Research: prove QQ16 parking bounds and exact row-division depth with the global-root cutoff

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<T_d,\\
+1+\sum_r c_r H_d(r\lfloor w/73\rfloor),&w\ge T_d.
+\end{cases}
+\]
+
+For integer w, `w**1000 < d` is equivalent to
+`w < ceil(d**(1/1000))`, including when d is a perfect 1000th power.
+The strict inequality matters at equality. If w=73q+delta is nonterminal,
+the source reaches its selected program at 73q without repeating the test.
+Thus the recurrence tests the original w, and recurses on rq. Every edge
+contracts by at most rho=48/73, so the recurrence is well defined.
+
+The actual `Machine.node` computes columns=q and unused rows=R/F.
+The actual `prepare_child` sets width=rq, rows=R/F, and
+`after'=after+(73-r)q*spacing`; it forwards root_width unchanged. The preceding
+remainder step replaces `before` by `before+delta*spacing`. Hence
+
+\[
+b=3\,\mathrm{compact\_bits}+\mathrm{front}+\mathrm{before}
+  +w\,\mathrm{spacing}+\mathrm{after}+\mathrm{back}
+\]
+
+is preserved by both steps. All prefix/component/coefficient descriptors are
+also preserved. Consequently the bank volume, including spectators, is
+divided by F, not by a width ratio. These source statements explain the
+recurrence's weights. `source_probe.py` executes these two unchanged methods
+over an exact descriptor-integer interpreter; it does not execute records,
+native payloads, Count arithmetic algorithms or their costs.
+
+If the incoming bank has complete volume v, summing current-bank volume over
+all selected-child parking pairs gives
+
+\[
+P_d(w,v)=N\Gamma v H_d(w).
+\]
+
+Indeed a depth-j rank path has multiplicity
+`Gamma**j product(n_r)` and volume `v/F**j`. Their Gamma factors cancel
+inside the path weight, but the `N Gamma` child invocations at that node
+remain. For sixteen removed C8 calls per outer cover, the corresponding
+quantity is `16 N Gamma**2 v H_d(8 lambda)`, when `8 lambda <= d` and all
+other source premises hold. It is already part of the removed complete C8
+bodies; it cannot be added a second time to a matched invoice.
+
+## Uniform envelope
+
+Let s be the unique number in (0,1) satisfying
+
+\[
+M(s)=\sum_r c_r(r/73)^s=1.
+\]
+
+Existence and uniqueness follow from strict decrease and
+`M(0)=255331/7168 > 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<s<1`.
+
+Set `a = 3456/25` and `q_T = floor(T_d/73) >= 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<T_d),\qquad
+D_d(w)=1+D_d(48\lfloor w/73\rfloor)\ (w\ge T_d).
+\]
+
+This is the exact maximum number of nonterminal selected-C nodes on a path,
+including the incoming node if nonterminal. Strong induction shows that D
+is nondecreasing in w: the threshold case is immediate and the child map is
+nondecreasing with argument strictly below w. Hence among all ranks the
+maximum descendant depth is attained by rank 48, which has positive
+multiplicity. This proves the recurrence from the complete tree.
+
+An equivalent inverse characterization checks the depth without expanding
+any tree. Let `B_1=T_d` and
+
+\[
+B_{j+1}=73\left\lceil B_j/48\right\rceil.
+\]
+
+Then `D_d(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.

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.