diff --git a/research/qq16-root-cutoff-parking/PROOF.md b/research/qq16-root-cutoff-parking/PROOF.md new file mode 100644 index 0000000000..fa69dec13a --- /dev/null +++ b/research/qq16-root-cutoff-parking/PROOF.md @@ -0,0 +1,262 @@ +# A global-root cutoff in the QQ16 parking recurrence + +## Domain and inherited premises + +Fix the historical original selected-C backend retained by QQ16 #4166, +as identified in [#4753](../qq16-nonterminal-c8-tree/README.md). Its dimension +is 73. Write **d for the positive integer global root-width descriptor**; +this is not the fixed dimension. At each selected-C node of integer width w, +the source tests `w < 73 or w**1000 < d` before stripping a remainder. +Only widths `0 <= w <= d` have a source interpretation. The recurrence below +also makes sense outside that range, without claiming source admission. + +The inherited histogram and full-bank relation are + +| r | 1 | 2 | 3 | 4 | 5 | 7 | 8 | 48 | +| --- | ---: | ---: | ---: | ---: | ---: | ---: | ---: | ---: | +| n_r | 349604 | 60192 | 62585 | 20448 | 11808 | 7 | 1152 | 4866 | + +Put `N = sum n_r = 510662`, `F = 14336 Gamma`, `c_r = n_r/14336`, and +`C = sum c_r = 255331/7168`. Gamma is the same positive integer owner +multiplier throughout this fixed backend. A nonterminal node has `n_r Gamma` +children of width `r floor(w/73)`. Each child's incoming rows and complete +bank volume are the parent's divided by F. Calls are sequential; their row +quotients are reused, not consumed additively. These are cited source premises, +not a new full literal-word census or physical correctness proof. + +The only priced subtrace is one current-bank volume per selected-child +park/restore pair. Ordinary/native internals, remainder leaves, other parked +roles, restore actions and candidate work are outside that quantity. In +particular the source-action floor `(2,5,5)` per parked bank bit is inherited +from #4753, not a complete park/restore invoice proved here. + +## Exact cutoff and recurrence + +For every integer d >= 1 define + +\[ +T_d=\max(73,\lceil d^{1/1000}\rceil),\qquad +H_d(w)=\begin{cases} +0,&w 1`, `M(1)=1041408/1046528 < 1`. +This is exactly #4865's existing exponent, not a new root search. Its +published bracket is `0.9983245373 < s < 0.9983245374`; the present proof +needs only the defining equation and `0= 1`. For every w >= T_d, + +\[ +\boxed{\quad +\frac{((w+a)/(T_d-1+a))^s-1}{C-1} +\le H_d(w)\le +\frac{(w/q_T)^s-1}{C-1}. +\quad} +\] + +The proof uses Nick Petalas's #4865 weighted-leaf argument with the cutoff +kept as a parameter. To make the extension's dependence explicit, let L be +the total terminal-leaf weight in the finite rank tree. Replacing one +frontier vertex by its children multiplies that vertex's weight by C. +Telescoping gives `L=1+(C-1)H_d(w)`. Every terminal leaf below a nonterminal +root has width in `[floor(T_d/73), T_d-1]`. + +For phi(x)=x^s, at an internal width w=73q+delta, +`sum c_r phi(rq)=(73q)^s <= phi(w)`. Telescoping implies +`q_T^s L <= w^s`, giving the upper bound. For psi(x)=(x+a)^s, + +\[ +a\ge\max_{r,0\le\delta\le72}\frac{r\delta}{73-r} + =\frac{48\cdot72}{25},\qquad +rq+a\ge(r/73)(w+a). +\] + +Thus `sum c_r psi(rq) >= psi(w)`. Terminal widths are at most T_d-1, +so `(T_d-1+a)^s L >= (w+a)^s`, giving the lower bound. The potential +functions and sharp per-edge affine shift are predecessor work; retaining +the moving cutoff and applying the result to changing d is the new scope. + +The constants can also be made uniform simultaneously in both parameters. +Put `A=1+a/73=5281/1825` and `X=(w/T_d)^s`. Since +`T_d-1+a <= A*T_d` and `floor(T_d/73) >= T_d/146`, the envelope and H>=1 give + +\[ +\frac{X}{C A^s}\le H_d(w)\le\frac{146^s}{C-1}X +\quad (w\ge T_d). +\] + +For the lower bound combine `H>=1` with +`H>=(X/A^s-1)/(C-1)`: the first suffices when X<=C A^s and the second when +X>=C A^s. Thus `H_d(w)=Theta((w/T_d)^s)` uniformly over the whole nonterminal +domain, with constants independent of d and w. There is no positive estimate +of this form for terminal widths, where H=0. + +## The diagonal recurrence and a growing root descriptor + +At w=d, let t=d^(1/1000). For t>=a, `T_d=ceil(t)`, +`T_d-1+a <= 2t`, and `floor(T_d/73) >= T_d/146 >= t/146`. +The latter inequality follows from `floor(x)>=x/2` for x>=1. Therefore + +\[ +\frac{(d^{999/1000}/2)^s-1}{C-1} +\le H_d(d)\le +\frac{(146d^{999/1000})^s-1}{C-1}, +\qquad H_d(d)=\Theta(d^{999s/1000}). +\] + +The implicit constants are independent of d. The same exponent applies +conditionally to any family with `epsilon*d <= w(d) <= d`, for fixed +epsilon>0. For other width families use the explicit envelope. Multiplying +the predecessor's bracket by 999/1000 gives the inherited numerical interval +`0.9973262127627 < 999s/1000 < 0.9973262128626`; it is not newly certified +numerical root information. + +This is a diagonal statement about a two-parameter recurrence. It neither +constructs an admitted RootPlan with w=d nor treats physical volume v as +constant while d grows. The full physical term has the extra factor +`N Gamma v(d)`. It does not follow that total runtime has this exponent. +The earlier fixed-cutoff `Theta(w^s)` remains correct on its stated domain. + +## Exact selected-C row-division depth + +Define + +\[ +D_d(w)=0\ (w=j` if and only if `w>=B_j`. The base case is the source cutoff. +Inductively, another internal level requires +`48 floor(w/73)>=B_j`, exactly equivalent to the displayed ceiling threshold. +These thresholds increase strictly. The source's pre-remainder test is why +`B_1` is T_d, not the next multiple of 73. For T_d=356, the first three +thresholds are 356, 584 and 949. The verifier checks this inverse oracle +against all finite DP depths and the giant historical maximum path. + +For a positive integer incoming row count R, every selected-C row division +in this reached tree is positive and exact **if and only if** + +\[ +F^{D_d(w)}\mid R. +\] + +Sufficiency follows since a depth-j node receives R/F^j and no path has more +than D internal nodes. Necessity follows on an attained longest path: its D +successive exact divisions imply divisibility by F^D. In particular the +smallest positive row count for this arithmetic contract is F^D. This is +not a minimum for all supplier stock or native/Ordinary internals. Sequential +sibling invocations reuse the same quotient; the total child count does not +create an additional stock power. + +There are explicit depth estimates. With rho=48/73 and a=3456/25, for w>=T_d, + +\[ +\left\lceil\frac{\log((w+a)/(T_d-1+a))}{\log(73/48)}\right\rceil +\le D_d(w)\le +1+\left\lfloor\frac{\log(w/T_d)}{\log(73/48)}\right\rfloor. +\] + +Along the maximum path, `w_j <= rho^j w` and +`w_j+a >= rho^j(w+a)`. The first terminal width is at most T_d-1; +the last internal width is at least T_d. Substituting these two facts gives +the displayed inequalities, with the strict threshold explaining the upper +`1+floor`. The checker verifies their integral equivalents, using powers +of 48 and 73, without floating-point logs. + +Consequently + +\[ +D_d(d)=\frac{999}{1000}\frac{\log d}{\log(73/48)}+O(1). +\] + +For fixed F, the arithmetic row minimum therefore satisfies +`F**D_d(d) = Theta_F(d**((999/1000)*log(F)/log(73/48)))`. +For variable F use the exact power; the constants in `Theta_F` are not +asserted uniform in F. This is a row-divisibility statement, not an installed +storage improvement. + +In #4753's historical descriptor `d=isqrt(2**16949)`, exact integer iteration +gives T_d=356 and D_d(d)=13997, ending at width 240. The cutoff-free +recurrence with T=73 gives 13999, ending at 48. The original conservative +RootPlan and its stock remain unchanged. Replacing its depth needs its own +root-layout, padding, all-caller and admission argument. + +## Boundary of the result + +No matched D* versus B* sign is established. All retained later calls, +candidate-only nonchild/shell/control work and the exact return credits must +still appear in that comparison. Lower bounds on both sides do not compare +their difference. No new recursive invoice is proposed, so the signed +invoice preflight is not an admission substitute or a claimed improvement. + +Source histogram/physical correctness, actual RootPlan admissibility, stock +construction, numerical precision, restoration, native/Ordinary implementations +and the selected framework assumptions remain inherited or unchecked. The +finite checker corroborates the written proof and its source descriptor +boundary; it is not a proof-assistant derivation or production execution. diff --git a/research/qq16-root-cutoff-parking/README.md b/research/qq16-root-cutoff-parking/README.md new file mode 100644 index 0000000000..ca14cf60fd --- /dev/null +++ b/research/qq16-root-cutoff-parking/README.md @@ -0,0 +1,131 @@ +# QQ16 parking with its global-root cutoff + +**Scoped proof with exact finite corroboration; no new kappa.** The literal +historical QQ16 child backend stops at `w < 73 or w**1000 < d`, where d is +the global root-width descriptor. This package extends Nick Petalas's +[#4865 fixed-cutoff parking law](../qq16-parking-power-law/README.md) to that +varying cutoff and determines the exact selected-C row-division depth. +It answers part of that package's second open question. The complete +matched QQ16 cost comparison remains open. + +Put `T_d=max(73,ceil(d**(1/1000)))`, `C=255331/7168`, `a=3456/25`, and let s +be #4865's existing moment root. For w>=T_d, the normalized parking mass is +bounded uniformly by + +\[ +\frac{((w+a)/(T_d-1+a))^s-1}{C-1} +\le H_d(w)\le +\frac{(w/\lfloor T_d/73\rfloor)^s-1}{C-1}. +\] + +In fact `H_d(w)=Theta((w/T_d)**s)` uniformly for w>=T_d. Thus the diagonal +recurrence has `H_d(d)=Theta(d**(999*s/1000))`, with constants independent of d. +This concerns normalized current-bank parking volume; +physical volume, admission and the complete cost are additional obligations. +The fixed-cutoff theorem remains unchanged and correctly scoped. + +The maximum-rank path +`w -> 48 floor(w/73)`, stopped at T_d, gives the exact division depth D_d(w). +Equivalently, the smallest widths reaching j divisions are `B_1=T_d` and +`B_(j+1)=73 ceil(B_j/48)`; this supplies a separate exact depth oracle. +Every selected-C row division is positive and exact precisely when +`(14336 Gamma)**D_d(w)` divides the positive incoming row count. At the +historical `d=isqrt(2**16949)`, the depth is **13997**, versus the existing +cutoff-free sufficient depth **13999**. This does not install smaller root +stock. [PROOF.md](PROOF.md) proves the envelope, its changing-root consequence, +the exact divisibility statement and logarithmic depth bounds. + +## Evidence and reproduction + +```sh +python3 -B scripts/research_package.py --package research/qq16-root-cutoff-parking --check-only +python3 -B scripts/research_package.py --package research/qq16-root-cutoff-parking +``` + +Expected scientific status: `PASS_QQ16_ROOT_CUTOFF_PARKING`. Python 3.12 and +the standard library suffice. The registered normal and optimized runs are +read-only and compare the full deterministic [RESULT.json](RESULT.json). +Only `verify.py --write` regenerates that receipt. + +The checker uses exact rational dynamic programming at ten cutoffs and every +width 0..8192, an independent breadth census on 70 boundary/large-width cases, +30 exact 1000th-power boundaries, and all 584 rank/residue inequalities. +It checks the full-volume cancellation and exact stock powers at three +integer Gamma calibrations. The giant historical root is checked by a single +maximum path and independent inverse thresholds, without constructing its +bank, row count or full tree. + +The source probe extracts the unchanged `Machine.node` and `prepare_child` +methods from authenticated bytes and runs them over exact integer descriptor +operations. It checks cutoff equality, no repeated post-remainder test, +child width/rows, unchanged global d and the complete spectator rectangle. +Its Tape/Count primitives are explicitly test interpreters: this is **not** +physical payload execution or an audit of primitive implementations. Executed +source mutations change equality, global-root forwarding, rows and spectator +tails; arithmetic discriminators cover a frozen cutoff, a repeated test and +an insufficient affine shift. One-short stock is rejected on every tested +nonterminal maximum path, and a row-count size bound is distinguished from +exact divisibility. Dropping rank 48 underestimates the tested tree depth. +Receipt controls reject duplicate keys and boolean/float substitutions for +integer fields. + +The finite checks corroborate the written universal proof. They do not +numerically certify a new moment root or rerun #4753's literal-word census. +The existing root bracket is cited only for orientation. No full supplier, +selected cold replay, Lean, Docker, native payload, hosted CI or independent +human review is claimed. + +Resource limits: fixed ten-cutoff arrays of 8193 entries, breadth width at most +65536, at most 4096 states/64 levels per census, and a 40000-step maximum-path +cap. The largest checked root has fewer than 21000 bits. No proof-relevant +subprocess or third-party package is used. Source pins cover every external +input; package-local files are the remaining execution closure. + +## Scope and coordination + +Base: `32890bc5de034ab8fc93ac88ead7279a6a416d04`, priority revision 7, +card `joint-query-controller`, refined scope in [TASK.json](TASK.json). +The [claim is in Discussion #4744](https://github.com/CrocSwap/integer-mult-bounds/discussions/4744#discussioncomment-19173694), +following [#4865's released result](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133932). +[SOURCES.json](SOURCES.json) freezes current-base bytes and the historical +provenance. This is the original backend retained by #4166/#4753, not a new +analysis of the currently selected #5413 supplier. + +No family expansion is justified by this result. The exact current-bank +parking term is only one removed expense. Candidate-only work, other parked +roles, restores, all retained later calls and finite control remain charged +or explicitly unresolved. Root-dependent bounds alone cannot decide the +complete D* versus B* inequality. + +## Open next questions + +1. Can the exact depth replace the conservative RootPlan stock exponent? + First bind padding, root-prefix geometry and every consumer of the original + depth to one admitted root family. The arithmetic divisibility result does + not check those contracts, and no stock replacement is installed here. +2. What bounds every candidate-only positive interval in the nonterminal + D* versus B* comparison? Start from the actual unmatched Compact/native + interval and its full geometry in the #4744 handoff. The missing upper + invoice remains the decision blocker; another descendant census is not + sufficient. See the structured obligations in TASK.json. + +## Credit + +Prepared for commdata2338 (@commdata2338), with substantial OpenAI Codex assistance. + +Nick Petalas's #4865 (`8f8f518bd1a40baa30434ab18e86fd851d122b28`) supplies +the weighted-leaf identity, two potential functions, sharp affine shift and +fixed-cutoff exponent law. Brian/JoyboyBrian's #4753 +(`44e2c79344e0090d4e829e0dde4f533d8d0273ec`) supplies the complete histogram, +global cutoff, fresh-row/full-bank interpretation and physical parking floor. +Chris R/Clear1nsight's #4166/#4167/#4172/#4177 and recursive-binding work +supply the installed caller and comparison boundaries. Jose Manuel supplies +the original physical machinery; ywz65, Sagar Thakrar, Tekalign, Ali Romman, +Arham Tahir and the retained source notices keep their predecessor credit. + +The new contribution is the cutoff-uniform theorem, changing-root consequence, +exact selected-tree stock-depth characterization and source-bound checks. +No literature-priority claim is made for finite-tree potentials or monotone +path arguments. Apache-2.0. Substantial AI assistance covers derivation, +implementation, checking and writing; no independent human or formal-kernel +acceptance is asserted. diff --git a/research/qq16-root-cutoff-parking/RESULT.json b/research/qq16-root-cutoff-parking/RESULT.json new file mode 100644 index 0000000000..fe10ff69d3 --- /dev/null +++ b/research/qq16-root-cutoff-parking/RESULT.json @@ -0,0 +1,627 @@ +{ + "affine_residue_cases": 584, + "breadth_censuses": [ + { + "cutoff": 73, + "depth": 0, + "mass": "0", + "width": 72 + }, + { + "cutoff": 73, + "depth": 1, + "mass": "1", + "width": 73 + }, + { + "cutoff": 73, + "depth": 1, + "mass": "1", + "width": 74 + }, + { + "cutoff": 73, + "depth": 4, + "mass": "550134544513/368293445632", + "width": 583 + }, + { + "cutoff": 73, + "depth": 4, + "mass": "550134544513/368293445632", + "width": 584 + }, + { + "cutoff": 73, + "depth": 10, + "mass": "2811672498409443148688787704860733825/49955345834886796458831223579475968", + "width": 8192 + }, + { + "cutoff": 73, + "depth": 15, + "mass": "175373450828157966851428377237092156347603044702917976321/945304995960626361667446543235370633114440189370957824", + "width": 65536 + }, + { + "cutoff": 74, + "depth": 0, + "mass": "0", + "width": 73 + }, + { + "cutoff": 74, + "depth": 1, + "mass": "1", + "width": 74 + }, + { + "cutoff": 74, + "depth": 1, + "mass": "1", + "width": 75 + }, + { + "cutoff": 74, + "depth": 4, + "mass": "550134544513/368293445632", + "width": 583 + }, + { + "cutoff": 74, + "depth": 4, + "mass": "550134544513/368293445632", + "width": 584 + }, + { + "cutoff": 74, + "depth": 10, + "mass": "2398173480104686392348963931050570113/49955345834886796458831223579475968", + "width": 8192 + }, + { + "cutoff": 74, + "depth": 15, + "mass": "175373450828157966851428377237092156347603044702917976321/945304995960626361667446543235370633114440189370957824", + "width": 65536 + }, + { + "cutoff": 145, + "depth": 0, + "mass": "0", + "width": 144 + }, + { + "cutoff": 145, + "depth": 1, + "mass": "1", + "width": 145 + }, + { + "cutoff": 145, + "depth": 1, + "mass": "1", + "width": 146 + }, + { + "cutoff": 145, + "depth": 3, + "mass": "74739457/51380224", + "width": 583 + }, + { + "cutoff": 145, + "depth": 3, + "mass": "74739457/51380224", + "width": 584 + }, + { + "cutoff": 145, + "depth": 9, + "mass": "132882182138938129851545843755009/6969216773840233880975338110976", + "width": 8192 + }, + { + "cutoff": 145, + "depth": 14, + "mass": "13639928442587386730548880190030757989676132407449473/131878487159685597330837966411184519128688642490368", + "width": 65536 + }, + { + "cutoff": 146, + "depth": 0, + "mass": "0", + "width": 145 + }, + { + "cutoff": 146, + "depth": 1, + "mass": "1", + "width": 146 + }, + { + "cutoff": 146, + "depth": 1, + "mass": "1", + "width": 147 + }, + { + "cutoff": 146, + "depth": 3, + "mass": "74739457/51380224", + "width": 583 + }, + { + "cutoff": 146, + "depth": 3, + "mass": "74739457/51380224", + "width": 584 + }, + { + "cutoff": 146, + "depth": 9, + "mass": "132882182138938129851545843755009/6969216773840233880975338110976", + "width": 8192 + }, + { + "cutoff": 146, + "depth": 14, + "mass": "13639928442587386730548880190030757989676132407449473/131878487159685597330837966411184519128688642490368", + "width": 65536 + }, + { + "cutoff": 355, + "depth": 0, + "mass": "0", + "width": 354 + }, + { + "cutoff": 355, + "depth": 1, + "mass": "1", + "width": 355 + }, + { + "cutoff": 355, + "depth": 1, + "mass": "1", + "width": 356 + }, + { + "cutoff": 355, + "depth": 1, + "mass": "1", + "width": 583 + }, + { + "cutoff": 355, + "depth": 2, + "mass": "9601/7168", + "width": 584 + }, + { + "cutoff": 355, + "depth": 8, + "mass": "4080978947771510752575463041/972267965100479057055711232", + "width": 8192 + }, + { + "cutoff": 355, + "depth": 12, + "mass": "186652659848756610913763294440157978239190145/2566716858993950616697155045707557038456832", + "width": 65536 + }, + { + "cutoff": 356, + "depth": 0, + "mass": "0", + "width": 355 + }, + { + "cutoff": 356, + "depth": 1, + "mass": "1", + "width": 356 + }, + { + "cutoff": 356, + "depth": 1, + "mass": "1", + "width": 357 + }, + { + "cutoff": 356, + "depth": 1, + "mass": "1", + "width": 583 + }, + { + "cutoff": 356, + "depth": 2, + "mass": "9601/7168", + "width": 584 + }, + { + "cutoff": 356, + "depth": 8, + "mass": "4080978947771510752575463041/972267965100479057055711232", + "width": 8192 + }, + { + "cutoff": 356, + "depth": 12, + "mass": "186649426958301437866100648392630399212733569/2566716858993950616697155045707557038456832", + "width": 65536 + }, + { + "cutoff": 357, + "depth": 0, + "mass": "0", + "width": 356 + }, + { + "cutoff": 357, + "depth": 1, + "mass": "1", + "width": 357 + }, + { + "cutoff": 357, + "depth": 1, + "mass": "1", + "width": 358 + }, + { + "cutoff": 357, + "depth": 1, + "mass": "1", + "width": 583 + }, + { + "cutoff": 357, + "depth": 2, + "mass": "9601/7168", + "width": 584 + }, + { + "cutoff": 357, + "depth": 8, + "mass": "4080978947771510752575463041/972267965100479057055711232", + "width": 8192 + }, + { + "cutoff": 357, + "depth": 12, + "mass": "186649426958301437866100648392630399212733569/2566716858993950616697155045707557038456832", + "width": 65536 + }, + { + "cutoff": 511, + "depth": 0, + "mass": "0", + "width": 510 + }, + { + "cutoff": 511, + "depth": 1, + "mass": "1", + "width": 511 + }, + { + "cutoff": 511, + "depth": 1, + "mass": "1", + "width": 512 + }, + { + "cutoff": 511, + "depth": 1, + "mass": "1", + "width": 583 + }, + { + "cutoff": 511, + "depth": 1, + "mass": "1", + "width": 584 + }, + { + "cutoff": 511, + "depth": 7, + "mass": "335338823579664883913985/135640062095490939879424", + "width": 8192 + }, + { + "cutoff": 511, + "depth": 12, + "mass": "168762320640236294545679795647782943381275777/2566716858993950616697155045707557038456832", + "width": 65536 + }, + { + "cutoff": 512, + "depth": 0, + "mass": "0", + "width": 511 + }, + { + "cutoff": 512, + "depth": 1, + "mass": "1", + "width": 512 + }, + { + "cutoff": 512, + "depth": 1, + "mass": "1", + "width": 513 + }, + { + "cutoff": 512, + "depth": 1, + "mass": "1", + "width": 583 + }, + { + "cutoff": 512, + "depth": 1, + "mass": "1", + "width": 584 + }, + { + "cutoff": 512, + "depth": 7, + "mass": "335316343277734433920257/135640062095490939879424", + "width": 8192 + }, + { + "cutoff": 512, + "depth": 12, + "mass": "168762320640236294545679795647782943381275777/2566716858993950616697155045707557038456832", + "width": 65536 + }, + { + "cutoff": 1024, + "depth": 0, + "mass": "0", + "width": 583 + }, + { + "cutoff": 1024, + "depth": 0, + "mass": "0", + "width": 584 + }, + { + "cutoff": 1024, + "depth": 0, + "mass": "0", + "width": 1023 + }, + { + "cutoff": 1024, + "depth": 1, + "mass": "1", + "width": 1024 + }, + { + "cutoff": 1024, + "depth": 1, + "mass": "1", + "width": 1025 + }, + { + "cutoff": 1024, + "depth": 5, + "mass": "3978404765090305/2639927418290176", + "width": 8192 + }, + { + "cutoff": 1024, + "depth": 10, + "mass": "1112323335042233158354699966049513857/49955345834886796458831223579475968", + "width": 65536 + } + ], + "claim_kind": "scoped proof with exact finite corroboration", + "dp_cutoffs": [ + 73, + 74, + 145, + 146, + 355, + 356, + 357, + 511, + 512, + 1024 + ], + "dp_widths_per_cutoff": 8193, + "full_cost_sign": "unresolved", + "histogram_census_replayed": false, + "historical_root": { + "coarse_division_depth": 13999, + "cutoff": 356, + "definition": "isqrt(2**16949)", + "exact_division_depth": 13997, + "last_internal_threshold_hex_sha256": "04ff801bdac539776ca0fee44303cef905a2603dcf76a21705bd9b73e6d67e2b", + "next_threshold_hex_sha256": "6a4a6a9f79e1bd18b07a13cc23a023029002c2ce6da01b4854754276aab45589" + }, + "new_kappa": false, + "physical_execution": false, + "rejected_controls": [ + "height equality made terminal", + "child resets global cutoff", + "child omits row division", + "child omits spectator tail", + "frozen 356 used for every root", + "height retested after remainder stripping", + "affine floor shift reduced below its allowed residue", + "rank-48 child omitted from maximum depth", + "inverse depth threshold rounded downward", + "boolean/integer receipt confusion", + "floating/integer receipt confusion", + "duplicate receipt key" + ], + "root_boundaries": [ + [ + 2, + -1, + 73 + ], + [ + 2, + 0, + 73 + ], + [ + 2, + 1, + 73 + ], + [ + 72, + -1, + 73 + ], + [ + 72, + 0, + 73 + ], + [ + 72, + 1, + 73 + ], + [ + 73, + -1, + 73 + ], + [ + 73, + 0, + 73 + ], + [ + 73, + 1, + 74 + ], + [ + 74, + -1, + 74 + ], + [ + 74, + 0, + 74 + ], + [ + 74, + 1, + 75 + ], + [ + 145, + -1, + 145 + ], + [ + 145, + 0, + 145 + ], + [ + 145, + 1, + 146 + ], + [ + 356, + -1, + 356 + ], + [ + 356, + 0, + 356 + ], + [ + 356, + 1, + 357 + ], + [ + 357, + -1, + 357 + ], + [ + 357, + 0, + 357 + ], + [ + 357, + 1, + 358 + ], + [ + 1024, + -1, + 1024 + ], + [ + 1024, + 0, + 1024 + ], + [ + 1024, + 1, + 1025 + ], + [ + 4096, + -1, + 4096 + ], + [ + 4096, + 0, + 4096 + ], + [ + 4096, + 1, + 4097 + ], + [ + 1000000, + -1, + 1000000 + ], + [ + 1000000, + 0, + 1000000 + ], + [ + 1000000, + 1, + 1000001 + ] + ], + "source_descriptor_probe": { + "child_cases": 304, + "node_cases": 85 + }, + "status": "PASS_QQ16_ROOT_CUTOFF_PARKING", + "stock_gamma_calibrations": [ + 1, + 2, + 7 + ] +} diff --git a/research/qq16-root-cutoff-parking/SOURCES.json b/research/qq16-root-cutoff-parking/SOURCES.json new file mode 100644 index 0000000000..a37c7762c0 --- /dev/null +++ b/research/qq16-root-cutoff-parking/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/physical-complex-controller/machine.py", + "usage": "input", + "git_blob": "92f9467ffd3346d672a0e2c56f2508e33ed21689", + "sha256": "b648792a361fdf98597a2f56c634767508be8e818b82e482fbfc60b5c63cc855" + }, + { + "path": "research/qq16-nonterminal-c8-tree/README.md", + "usage": "input", + "git_blob": "55bd5ce66846b5ddf124c655c617a8b47b52d9b7", + "sha256": "e57f9c84275c5cf0baf914322392a8ba0b39e014490c396ed1da85fb005337a2" + }, + { + "path": "research/qq16-nonterminal-c8-tree/RESULT.json", + "usage": "input", + "git_blob": "8c11adabc19648de3ebcfb20cbad1cd47ee63e5d", + "sha256": "0e3fbddf58103dd04c2bdf2912b30c218e3e68a974aac868bd07b2cc1280230b" + }, + { + "path": "research/qq16-parking-power-law/README.md", + "usage": "input", + "git_blob": "e9eff8b9d0e7ae95cd0c0c8245ec96826b264235", + "sha256": "be44dd95fb7d66f39f02943f1e5377bb028f7b28f8ac990a6e5c89e808a64fdd" + }, + { + "path": "research/qq16-recursive-binding/PROOF.md", + "usage": "input", + "git_blob": "5de56af0213bf710ae3e832f21de74cf0ac9c7b0", + "sha256": "b547277ab5380b218893908a3e8e8874efc0cf3f9717b582f8972698d87418a2" + } + ] +} diff --git a/research/qq16-root-cutoff-parking/TASK.json b/research/qq16-root-cutoff-parking/TASK.json new file mode 100644 index 0000000000..7d5a61d534 --- /dev/null +++ b/research/qq16-root-cutoff-parking/TASK.json @@ -0,0 +1,144 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "joint-query-controller", + "question": "Can the installed QQ16 caller win a complete matched protocol bill, or can a changed demand eliminate actual paid work?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/qq16-caller-install/README.md" + ], + "methods": [ + "Derive the matched whole-caller physical bill for installed and baseline protocols.", + "Change the actual demanded observations and prove a cheaper legal producer/consumer contract." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #4166 COST.md and ADMISSION.json. An actual caller connection is now proposed. Its native-component profile loses; parent park/restore versus external-call costs remain unresolved. Retain the producer and recovery lineage rather than rebuild it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "At the actual installed cut, compare matched complete parent park/restore and external input/return protocols at the same bank/packet geometry, including every later root call and service cost. Alternatively pin both bridge observations and derive a genuinely smaller source-compatible demand. Stop if the complete necessary inequality fails or an essential cost is unknown; no larger decoder scan from a local tape-action saving.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair.", + "One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations.", + "Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise.", + "Treating a completed-output defect inequality as a producer-interior, dirty-range or physical-cost certificate.", + "Recreating completed-output recovery or caller wiring already supplied by #4166 without new independent coverage.", + "Dropping retained later root calls or claiming native-profile dominance from the isolated publication saving." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969", + "2540", + "early record", + "output-bank retention", + "complete native decoder", + "2965", + "producer defect", + "dirty-helper range", + "F17 consumer", + "4166", + "qq16-caller-install" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Uniform global-root-cutoff parking envelope and exact selected-C fresh-row division depth for the frozen original QQ16 backend.", + "scope_change_reason": "Take PR4865 Open next question 2: its fixed-cutoff asymptotic explicitly does not establish a growing-root descriptor or stock law. This closes the recurrence/row-divisibility part while preserving actual RootPlan admission as an open obligation.", + "bottleneck_link": "The whole-caller bill contains removed original C8 bodies. A root-dependent bound prevents applying a fixed-cutoff asymptotic to a growing root without its changed stopping rule and stock obligations.", + "budget_minutes": 60, + "stop_rule": "Stop after the quantified recurrence and row-divisibility result plus bounded checks; do not expand the construction or infer a total sign from one removed expense.", + "outcome": "partial", + "evidence": "PROOF.md; RESULT.json exact rational DP, independent breadth and inverse-depth oracles, authenticated descriptor-method interpreter and rejection controls.", + "author": "commdata2338", + "ai_assistance": "Substantial OpenAI Codex assistance in derivation, implementation, checking and writing; no independent human or formal-kernel review.", + "open_questions": [ + { + "question": "Can the exact selected-C depth replace the conservative RootPlan stock exponent?", + "why_it_matters": "The two-division difference in the historical descriptor is arithmetic only until every stock consumer and root geometry is checked.", + "first_step": "Bind padding, root-prefix geometry and each use of the original coarse depth to one admitted root family.", + "blocked_by": "No RootPlan modification, complete stock or admission argument is provided." + }, + { + "question": "Can every candidate-only positive interval in the nonterminal D* versus B* comparison be upper-priced at its actual full geometry?", + "why_it_matters": "A removed parking term alone does not determine the signed complete cost.", + "first_step": "Use Discussion4744 comment19140234 and bind the first unmatched Compact/native interval including spectators and all descendants.", + "blocked_by": "The constructive full candidate upper invoice remains missing; further descendant counting alone cannot close it." + } + ], + "scope_key": "73442cf25caf1ed45f11", + "predecessor_heads": { + "PR4865": "8f8f518bd1a40baa30434ab18e86fd851d122b28", + "PR4753": "44e2c79344e0090d4e829e0dde4f533d8d0273ec", + "PR4166": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "PR4177": "4cdda81c2ad99ffe5add0ac5d894094c3cca101a" + }, + "selection": { + "mode": "released-handoff refinement", + "seed": "45a2393c7289f16f036f033bc27ae9e7", + "track": "recursive-interfaces", + "handoff": "https://github.com/CrocSwap/integer-mult-bounds/pull/4865", + "canonical_thread": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4744", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4744#discussioncomment-19173694" + }, + "family_expansion_decision": "Narrow and stop. This prices one subtrace and characterizes selected-tree arithmetic divisibility; candidate costs and full admission remain unknown.", + "remaining_obligations": [ + "The inherited source histogram and physical/primitive correctness are cited premises, not independently replayed.", + "RootPlan geometry, padding, all-caller stock and actual positive-volume admission are unproved by this package.", + "Complete unmatched nonchild/shell/native/control costs, all later calls, restoration and exact return credits are needed for D* versus B*.", + "No selected supplier, precision, outer or complete multiplication theorem is changed." + ], + "freshness": { + "checked_at": "2026-10-25T05:35:03+00:00", + "canonical_main": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "priority_revision": 7, + "changes_since_base": "none", + "selected_result": "PR5413; historical QQ16 backend and source pins intentionally retained", + "overlap": { + "open_prs_fetched_at": "2026-10-25T05:31:21.052548+00:00", + "open_prs": 371, + "discussions_fetched_at": "2026-10-25T05:33:05.370314+00:00", + "discussions": 4779, + "complete_pagination": true, + "complete_base_local_notes": 7402, + "scope_query": [ + "parking-power-law", + "parked current-bank volume", + "fresh-row depth", + "root-dependent" + ], + "nearest_matches": [ + "PR4865 fixed-cutoff package", + "this investigation in Discussion4744" + ], + "limitations": "Text and declared local-note coverage; arbitrary diffs and unpublished work are not exhaustive." + } + } +} diff --git a/research/qq16-root-cutoff-parking/VERIFY.json b/research/qq16-root-cutoff-parking/VERIFY.json new file mode 100644 index 0000000000..4c05515a48 --- /dev/null +++ b/research/qq16-root-cutoff-parking/VERIFY.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/physical-complex-controller/machine.py", + "research/qq16-nonterminal-c8-tree/README.md", + "research/qq16-nonterminal-c8-tree/RESULT.json", + "research/qq16-parking-power-law/README.md", + "research/qq16-recursive-binding/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "root-dependent-cutoff-envelope-depth-source-controls" + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "root-dependent-cutoff-envelope-depth-source-controls-optimized" + } + ] +} diff --git a/research/qq16-root-cutoff-parking/source_probe.py b/research/qq16-root-cutoff-parking/source_probe.py new file mode 100644 index 0000000000..70fe4dd066 --- /dev/null +++ b/research/qq16-root-cutoff-parking/source_probe.py @@ -0,0 +1,133 @@ +# SPDX-License-Identifier: Apache-2.0 +"""Execute two unchanged source methods over exact descriptor integers. + +This is a Count/record test interpreter, not physical execution or a new +implementation of the source primitives. Physical correctness is inherited. +Prepared for commdata2338 with substantial OpenAI Codex assistance. +""" +import ast +from types import SimpleNamespace + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +class Count: + def __init__(self, value): + self.value = value.value if isinstance(value, Count) else value + need(type(self.value) is int and self.value >= 0, "natural descriptor") + self.tape = self + + literal = classmethod(lambda cls, value: cls(value)) + product = classmethod(lambda cls, a, b: cls(a.value * b.value)) + + def zero(self): + return self.value == 0 + + def add(self, other): + self.value += other.value + + def multiply_small(self, factor): + self.value *= factor + + def divide_small(self, divisor): + self.value, remainder = divmod(self.value, divisor) + return remainder + + def close(self): + pass # Lifetimes, record cells and their costs are outside this probe. + + +def methods(source): + tree = ast.parse(source) + machine = next(n for n in tree.body if isinstance(n, ast.ClassDef) + and n.name == "Machine") + inputs = next(ast.literal_eval(n.value) for n in tree.body + if isinstance(n, ast.Assign) and any( + isinstance(t, ast.Name) and t.id == "INPUTS" for t in n.targets)) + functions = [n for n in machine.body if isinstance(n, ast.FunctionDef) + and n.name in ("node", "prepare_child")] + need(len(functions) == 2, "both original descriptor methods") + env = { + "Count": Count, "INPUTS": inputs, "BLANK": -1, "need": need, + "positive": lambda x: need(x.value > 0, "positive descriptor"), + "compare": lambda a, b: (a.value > b.value) - (a.value < b.value), + "subtract": lambda a, b: Count(a.value - b.value), + "divide": lambda a, b: tuple(Count(x) for x in divmod(a.value, b.value)), + "fixed_power": lambda a, k, cap: Count(min(a.value ** k, cap.value)), + "skip": lambda tape, extent: None, + "copy_symbols": lambda source, target: setattr(target, "value", source.value), + } + # No imported predecessor module or constructor executes here. + exec(compile(ast.Module(body=functions, type_ignores=[]), + "", "exec"), env) + return inputs, env["node"], env["prepare_child"] + + +def fixture(inputs, width, root_width, rows, gamma): + values = dict.fromkeys(inputs, 0) + values.update(width=width, root_width=root_width, rows=rows, prefixes=3, + spacing=7, guard=1, component_bits=2, coefficients=5, + front=11, compact_bits=2, before=13, after=17, back=19) + state = SimpleNamespace(values=values, leaves=[], mode="node", group=None, + binding=SimpleNamespace(dimension=73, families=14336, + cover=SimpleNamespace(size=gamma))) + state.roles = {"current": SimpleNamespace(rewind=lambda: None, read=lambda: -1), + "header": SimpleNamespace()} + state.c = lambda key: Count(state.values[key]) + state.save = lambda value, key: state.values.__setitem__(key, value.value) + state.shape = lambda: state.values.__setitem__("row_bits", 20) + state.complete_extent = lambda: Count(0) + state.apply_leaf = lambda w, before, after: state.leaves.append( + (w.value, before.value, after.value)) + state.capsule = {name: Count(0) for name in ("current", *inputs)} + state.packet = lambda index: Count(23) + state.header = SimpleNamespace(write=lambda tape, fields: None) + state.bank = SimpleNamespace(state="gathered") + state.root = True + return state + + +def rectangle(values): + return (3 * values["compact_bits"] + values["front"] + values["before"] + + values["width"] * values["spacing"] + values["after"] + values["back"]) + + +def check_source(source, ranks, cutoffs): + inputs, node, child = methods(source) + counts = {"node_cases": 0, "child_cases": 0} + for threshold in cutoffs: + root = threshold ** 1000 + for width in sorted({0, 1, 72, 73, threshold-1, threshold, threshold+1, + 73*(threshold//48), 8192}): + gamma, rows = 3, (14336*3)**4 + state = fixture(inputs, width, root, rows, gamma) + before = rectangle(state.values) + node(state) + terminal = width < 73 or width ** 1000 < root + need((state.mode == "return") == terminal, "literal cutoff decision") + counts["node_cases"] += 1 + if terminal: + need(state.leaves == [(width, 13, 17)], "terminal source leaf") + continue + q, remainder = divmod(width, 73) + need(state.values["columns"] == q and state.values["width"] == 73*q, + "source quotient and reached program width") + need(state.values["unused"] == rows//(14336*gamma), "source fresh rows") + need(rectangle(state.values) == before, "remainder spectators preserved") + need(len(state.leaves) == bool(remainder), "one optional remainder leaf") + state.group = object() + for rank in ranks: + child(state, 0, rank) + result = {name: value.value for name, value in state.capsule.items() + if name != "current"} + need(result["width"] == rank*q, "literal child width") + need(result["rows"] == rows//(14336*gamma), "literal child row division") + need(result["root_width"] == root, "unchanged global cutoff") + need(rectangle(result) == before, "complete address extent preserved") + for key in set(inputs)-{"rows", "width", "after", "before"}: + need(result[key] == state.values[key], "unchanged spectator descriptor") + counts["child_cases"] += 1 + return counts diff --git a/research/qq16-root-cutoff-parking/verify.py b/research/qq16-root-cutoff-parking/verify.py new file mode 100644 index 0000000000..972e922efc --- /dev/null +++ b/research/qq16-root-cutoff-parking/verify.py @@ -0,0 +1,290 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Exact corroboration of the root-dependent QQ16 parking/row-depth proof. + +No floating point, numerical root search, native payload or predecessor replay. +Prepared for commdata2338 with substantial OpenAI Codex assistance. +""" +import argparse +from bisect import bisect_right +from collections import Counter +from fractions import Fraction as Q +from hashlib import sha256 +from math import isqrt +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +from source_probe import check_source, need + +DIMENSION = 73 +ROW_FACTOR = 14336 +SHIFT = Q(3456, 25) +CUTOFFS = (73, 74, 145, 146, 355, 356, 357, 511, 512, 1024) +WIDTH_LIMIT = 8192 + + +def receipt_matches(raw, expected): + def unique(items): + result = {} + for key, value in items: + need(key not in result, "duplicate receipt key") + result[key] = value + return result + + def no_float(value): + raise ValueError("receipt numbers must be exact integers: "+value) + + saved = json.loads(raw, object_pairs_hook=unique, parse_float=no_float, + parse_constant=no_float) + need(json.dumps(saved, sort_keys=True) == json.dumps(expected, sort_keys=True), + "complete typed committed receipt") + + +def authenticate(): + manifest = json.loads((HERE/"SOURCES.json").read_text()) + raw = {} + for row in manifest["files"]: + if row["usage"] == "input": + value = (ROOT/row["path"]).read_bytes() + need(sha256(value).hexdigest() == row["sha256"], "source digest: "+row["path"]) + raw[row["path"]] = value + result = json.loads(raw["research/qq16-nonterminal-c8-tree/RESULT.json"]) + ranks = {int(r): n for r, n in result["rank_histogram"].items()} + need(ranks == {1:349604, 2:60192, 3:62585, 4:20448, + 5:11808, 7:7, 8:1152, 48:4866}, "inherited complete histogram") + return ranks, raw["research/physical-complex-controller/machine.py"].decode() + + +def cutoff(root): + """Exact ceil(root**(1/1000)), with the source's width-73 floor.""" + need(type(root) is int and root >= 1 and root.bit_length() <= 21000, + "bounded positive global root") + lo, hi = 0, 1 << ((root.bit_length()+999)//1000) + while hi-lo > 1: + middle = (lo+hi)//2 + if middle**1000 >= root: + hi = middle + else: + lo = middle + return max(73, hi) + + +def longest(width, threshold): + path = [] + while width >= threshold: + need(len(path) < 40000, "depth resource cap") + path.append(width) + width = 48*(width//73) + return path, width + + +def inverse_thresholds(width, threshold): + """Smallest widths reaching successive division depths; includes sentinel.""" + levels = [threshold] + while levels[-1] <= width: + need(len(levels) < 40000, "inverse-depth resource cap") + levels.append(73*((levels[-1]+47)//48)) + return levels + + +def depth_bounds(width, threshold, depth): + if width < threshold: + need(depth == 0, "terminal depth") + return + # Equivalent to the displayed logarithmic bounds, entirely integral. + need((25*width+3456)*48**depth <= (25*(threshold-1)+3456)*73**depth, + "affine lower bound on depth") + need(width*48**(depth-1) >= threshold*73**(depth-1), + "multiplicative upper bound on depth") + + +def tables(ranks, threshold): + mass = [Q(0)]*(WIDTH_LIMIT+1) + leaves = [Q(1)]*(WIDTH_LIMIT+1) + depths = [0]*(WIDTH_LIMIT+1) + thresholds = inverse_thresholds(WIDTH_LIMIT, threshold) + c = Q(sum(ranks.values()), ROW_FACTOR) + for width in range(threshold, WIDTH_LIMIT+1): + children = [(r*(width//73), n) for r, n in ranks.items()] + mass[width] = 1+sum((Q(n, ROW_FACTOR)*mass[v] for v, n in children), Q(0)) + leaves[width] = sum((Q(n, ROW_FACTOR)*leaves[v] for v, n in children), Q(0)) + depths[width] = 1+max(depths[v] for v, _ in children) + need(depths[width] == 1+depths[48*(width//73)], "maximum-rank path is attained") + need(leaves[width] == 1+(c-1)*mass[width], "weighted leaf/internal identity") + need(depths[width] >= depths[width-1], "depth monotonicity") + need(depths[width] == bisect_right(thresholds, width), "inverse threshold oracle") + depth_bounds(width, threshold, depths[width]) + return mass, leaves, depths + + +def census(ranks, width, threshold): + """Independent integer path counting by breadth, with Gamma symbolic.""" + frontier = Counter({width:1}) + internal, leaves, rows = Q(0), Q(0), [] + for depth in range(64): + if not frontier: + return internal, leaves, rows + need(len(frontier) <= 4096, "frontier resource cap") + active = sum(n for w, n in frontier.items() if w >= threshold) + terminal = sum(n for w, n in frontier.items() if w < threshold) + internal += Q(active, ROW_FACTOR**depth) + leaves += Q(terminal, ROW_FACTOR**depth) + rows.append((active, terminal)) + successor = Counter() + for w, paths in frontier.items(): + if w < threshold: + if depth: + need(threshold//73 <= w < threshold, "terminal width interval") + continue + for rank, n in ranks.items(): + successor[rank*(w//73)] += paths*n + frontier = successor + raise ValueError("census depth resource cap") + + +def stock_and_volume(ranks, width, threshold, mass, rows): + path, _ = longest(width, threshold) + depth = len(path) + total = sum(ranks.values()) + for gamma in (1, 2, 7): + f = ROW_FACTOR*gamma + incoming = f**depth + remaining = incoming + for _ in path: + remaining, remainder = divmod(remaining, f) + need(remainder == 0 and remaining > 0, "sufficient positive stock") + need(remaining == 1, "minimal stock reaches one at terminal depth") + if depth: + remaining = incoming//f + for _ in path[:-1]: + remaining //= f + need(remaining == 1 and remaining % f != 0, "one-short stock fails") + need(incoming+1 > incoming and (incoming+1) % f != 0, + "a size bound cannot replace exact divisibility") + # The proof allows any admitted complete-bank volume v. + paid = sum(active*gamma**j*(total*gamma)*Q(incoming, f**j) + for j, (active, _) in enumerate(rows)) + need(paid == total*gamma*incoming*mass, "full-volume Gamma cancellation") + + +def controls(ranks, source): + rejected = [] + for name, changed in ( + ("height equality made terminal", source.replace( + 'if compare(test, self.c("root_width")) < 0:', + 'if compare(test, self.c("root_width")) <= 0:')), + ("child resets global cutoff", source.replace( + 'else self.c(name)', 'else width if name == "root_width" else self.c(name)')), + ("child omits row division", source.replace( + 'self.c("unused") if name == "rows"', 'self.c("rows") if name == "rows"')), + ("child omits spectator tail", source.replace( + 'after.add(self.c("after"))', 'after = self.c("after")')), + ): + need(changed != source, "source mutation applied") + try: + check_source(changed, ranks, (73, 356)) + except ValueError: + rejected.append(name) + else: + raise ValueError("source mutation survived: "+name) + need(cutoff(356**1000+1) == 357, "moving cutoff distinguishes fixed-356 shortcut") + rejected.append("frozen 356 used for every root") + need(len(longest(356, 356)[0]) == 1 and len(longest(292, 356)[0]) == 0, + "retesting reached remainder-stripped program changes tree") + rejected.append("height retested after remainder stripping") + need((SHIFT-Q(1,25))*25 < 48*72, "too-small affine shift fails") + rejected.append("affine floor shift reduced below its allowed residue") + need(len(longest(584, 356)[0]) == 2 and 8*(584//73) < 356, + "dropping the positive rank-48 class underestimates depth") + rejected.append("rank-48 child omitted from maximum depth") + need(inverse_thresholds(584,356)[:2] == [356,584] + and len(longest(73*(356//48),356)[0]) == 1, + "inverse child threshold requires ceiling, not floor") + rejected.append("inverse depth threshold rounded downward") + for label, raw in (("boolean/integer receipt confusion", '{"x":[true]}'), + ("floating/integer receipt confusion", '{"x":[1.0]}'), + ("duplicate receipt key", '{"x":[1],"x":[1]}')): + try: + receipt_matches(raw, {"x":[1]}) + except ValueError: + rejected.append(label) + else: + raise ValueError("receipt mutation survived: "+label) + return rejected + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--write", action="store_true") + args = parser.parse_args() + ranks, source = authenticate() + total = sum(ranks.values()) + c = Q(total, ROW_FACTOR) + need(c > 1 and Q(sum(r*n for r,n in ranks.items()), 73*ROW_FACTOR) < 1, + "unique moment exponent in (0,1)") + shifts = [Q(r*delta, 73-r) for r in ranks for delta in range(73)] + need(max(shifts) == SHIFT, "sharp affine residue constant") + root_cases = [] + for k in (2, 72, 73, 74, 145, 356, 357, 1024, 4096, 10**6): + for offset in (-1, 0, 1): + d = k**1000+offset + expected = max(73, k+(offset == 1)) + need(cutoff(d) == expected, "exact 1000th-power boundary") + root_cases.append([k, offset, expected]) + sample_rows = [] + for t in CUTOFFS: + mass, leaves, depths = tables(ranks, t) + for w in sorted({t-1, t, t+1, 583, 584, 8192, 65536}): + h, leaf, rows = census(ranks, w, t) + need(leaf == 1+(c-1)*h, "breadth leaf identity") + if w <= WIDTH_LIMIT: + need(h == mass[w] and leaf == leaves[w], "independent breadth/DP agreement") + stock_and_volume(ranks, w, t, h, rows) + sample_rows.append({"cutoff": t, "width": w, "mass": str(h), + "depth": len(longest(w,t)[0])}) + d = isqrt(1 << 16949) + t = cutoff(d) + actual, last = longest(d,t) + coarse, coarse_last = longest(d,73) + reverse = inverse_thresholds(d,t) + need(len(reverse)-1 == len(actual) and reverse[-2] <= d < reverse[-1], + "independent giant-root inverse threshold") + need((t,len(actual),len(coarse),last,coarse_last) == (356,13997,13999,240,48), + "historical exact global-root depth") + depth_bounds(d,t,len(actual)) + receipt = { + "status": "PASS_QQ16_ROOT_CUTOFF_PARKING", + "claim_kind": "scoped proof with exact finite corroboration", + "dp_cutoffs": list(CUTOFFS), "dp_widths_per_cutoff": WIDTH_LIMIT+1, + "affine_residue_cases": len(shifts), "root_boundaries": root_cases, + "breadth_censuses": sample_rows, + "source_descriptor_probe": check_source(source, ranks, CUTOFFS), + "historical_root": {"definition": "isqrt(2**16949)", "cutoff": t, + "exact_division_depth": len(actual), + "coarse_division_depth": len(coarse), + "last_internal_threshold_hex_sha256": sha256( + hex(reverse[-2]).encode()).hexdigest(), + "next_threshold_hex_sha256": sha256( + hex(reverse[-1]).encode()).hexdigest()}, + "rejected_controls": controls(ranks,source), + "stock_gamma_calibrations": [1,2,7], + "histogram_census_replayed": False, "physical_execution": False, + "full_cost_sign": "unresolved", "new_kappa": False, + } + target = HERE/"RESULT.json" + if args.write: + target.write_text(json.dumps(receipt, indent=2, sort_keys=True)+"\n") + else: + receipt_matches(target.read_text(), receipt) + print(receipt["status"]) + print(json.dumps({k:receipt[k] for k in ("historical_root", "source_descriptor_probe", + "dp_widths_per_cutoff", "rejected_controls")}, + sort_keys=True)) + + +if __name__ == "__main__": + main()