Bound complete RootPlan retained backing across call histories (no new κ)

research/rootplan-backing-envelope/PROOF.md

@@ -0,0 +1,190 @@
+# Complete encoded RootPlan backing envelope
+
+This result was produced by Nick Petalas. Apache-2.0.
+
+## Statement and boundary
+
+Use the unchanged `MinimumRootPlan` in Ali Romman's merged PR #5707,
+`research/encoded-minimum-root-prefix/planner.py`, pinned by SOURCES.json.
+Its constructor fixes `2 <= m <= 73`, `1 <= r < m`, `F > 1` and integer
+guard exponent `g >= 0`. Each successful `compute` borrows canonical,
+distinct Counts
+
+```
+(p, s, left, right, C, B, rho),
+p >= 2, C >= 1, B >= 1, 0 <= s <= d, 0 <= rho < K,
+d = floor(p^(997/1000)), K = floor(d^(1/500)).
+```
+
+The seven borrowed tapes are separate from all owned tapes. Calls obey the
+source's empty-scratch entry contract. We count `len(Tape.cells)`, including
+erased BLANK tails, for its 256 scratch tapes and 29 field tapes. This does
+not count Python heap memory, borrowed input backing, payload execution,
+tape actions, or storage elsewhere in `RootLayer`.
+
+For a call define
+
+```
+b = bitlength(p), u = bitlength(C), v = bitlength(B),
+c = ceil(log2 F), h = m - 1, z = left + s*K + right,
+E = 8 + max(1994*b, c*h*b, z + u + v + b + g).
+```
+
+For any finite history of successful calls, let `a_i` be physical tape i's
+initial extent. At every instant through call j and its field cleanup,
+
+```
+len(cells_i) <= max(a_i, E_1, ..., E_j).
+```
+
+The sum of those 285 maxima bounds the complete owned backing. A cold
+planner therefore needs at most `285*max_j E_j` cells throughout its history.
+These are sufficient bounds, with no optimality claim for their constants.
+The successful-call premise does not assert absence of pool exhaustion on
+every input or provide a complete multiplier implementation.
+
+## Primitive extent rule
+
+The retained Count implementation represents an L-digit natural by LEFT at
+index zero, digits at 1 through L, and RIGHT at L+1. Zero has one digit.
+Copies, literal construction, increment and multiplication by a compiled
+constant write only through the longest old or resulting digit interval.
+Addition copies its right operand, then writes at most the longer input or
+the sum's interval. `Count.product` copies both factors and scans multiplier
+prefixes. Its result and temporary sums never exceed the final product when
+both factors are positive. A zero factor still requires its input copy.
+
+`encoded.divide` copies the divisor and keeps quotient and remainder. Each
+pre-subtraction remainder is less than twice the divisor; quotient prefixes
+are bounded by the final quotient. `subtract` copies its left operand.
+Normalization and division may leave erased high digits, but never extend
+past an already bounded old interval. Counter copies and decrements do not
+increase the copied digit interval. `copy_symbols` writes the complete
+Count including RIGHT. Clear writes through an existing dense body only.
+Add two cells to a digit bound for the markers.
+
+These rules follow directly from the retained `cardinal_counts`, `counts`,
+`cardinality`, `encoded`, `compact_counts`, `stream`, `machine` and `records`
+implementations. Their exact transitive bytes are retained in PR5707's
+source archive. The new step is applying these rules to the complete caller,
+including expressions outside the standalone callee of JoyboyBrian's PR #6098.
+
+## Parameter calculations
+
+The largest uncapped power target is `p^997`, used by `floor_power` and
+`atom_width`. Exponentiation by squaring constructs powers with exponents
+no larger than the requested fixed exponent. Saturated powers return their
+cap when a nonzero operand is already at least the cap. Otherwise they
+first form the full product of two operands smaller than the cap. Thus
+saturation does not justify charging only the cap's length.
+
+Every target and cap is at most `p^997+1 < 2^(997*b)+1`. Every such full
+product has fewer than `1994*b+2` binary digits. Input copies, bisection
+sums, `cap=target+1` and the smaller root computations fit this same bound.
+The marker allowance in E exceeds the resulting `1994*b+4` extent bound.
+
+The other parameter fields obey
+
+```
+1 <= d <= p, 1 <= K <= p,
+G = 4 ceil(log2 p)+6 <= 4*b+6 < 2^(b+3),
+H = d*G < 2^(2*b+3), delta = d*2^g < 2^(b+g).
+```
+
+Hence `qF=ceil(2H/K) <= 2H`, `qB <= H`, and their sum, products by K,
+and addition of `q0 <= p` use fewer than `2*b+6` digits. The products
+`qF*K < 2H+K` and `qB*K < H+K` are bounded before their subtractions.
+`input_bits=p+2` and `work_bits=p+2*delta+3` use at most `b+g+3`
+digits. Intermediate additions are nonnegative prefixes of those sums.
+The fixed literals through m have at most seven digits. All these lengths
+fit E after markers.
+
+## Complete minimum-prefix call
+
+This part uses the standalone envelope proved in JoyboyBrian's PR #6098 as
+a cited input. Its proof gives, for `M=remaining <= p` and spacing `K<=p`,
+at most
+
+```
+2 + max(7, bitlength(M)+bitlength(K)+1,
+        c*h*bitlength(M)+2)
+```
+
+cells for every newly reached scratch extent. This is at most E. Other
+caller leases remain live during that call, but cannot be acquired again
+until closed. Their values are covered by the other rows of this proof.
+The callee's free slots are still physical members of the same 256-tape
+pool. No standalone aggregate or 14-live-lease bound is substituted for
+historical backing of the caller.
+
+The returned `q0` is at most M-1, every profile depth is at most h*b, and
+`stock=F^depth <= 2^(c*h*b)`. These are the cited callee contract. The direct
+branch returns constants zero and one instead.
+
+## Address and row expressions
+
+Put `a=s*K` and `t=q0*K`. Both are nonnegative, and on the fast branch
+`t <= a`, since `q0 < M <= s`. The remaining complete expression ledger is
+
+| Expression | Digit bound or nonnegative magnitude bound |
+| --- | --- |
+| `active_bits=s*K`, its input copies | a; numeric digit length <= z+1 |
+| `left+active_bits+right` | z; its digit length <= z+1 |
+| `addresses=2^z` and its Counter | z+1 digits; the counter is no longer |
+| `gaussians=addresses*C*B` | at most z+u+v+1 digits, including both partial products |
+| `core_width=s-Q0` | at most p |
+| `core_front=qF*K-2H` | less than K |
+| `core_back=qB*K-H+right` | less than K+right |
+| `row_axes=t`, `original_rows=2^t` | t<=a; at most a+1 digits for the power |
+| `prefixes=B*2^left` | at most left+v+1 digits |
+| `ceil(original_rows/stock)` | quotient <= original_rows; temporary remainder < 2*stock |
+| `padded_rows=ceil(original_rows/stock)*stock` | less than original_rows+stock, hence at most max(a,c*h*b)+2 digits |
+| `rectangle=active_bits-row_axes+right` | between zero and a+right, hence at most z |
+| `row_gaussians=2^rectangle*C` | at most z+u+1 digits |
+| `row_bits=2*row_gaussians*work_bits` | at most z+u+b+g+4 digits, including the partial product |
+
+The padded-row estimate uses only division arithmetic. It does not need
+strict factor-two feasibility or a replay of the predecessor's padding
+theorem. Product prefixes are bounded by the final value. Input copies,
+sums, subtractions, counters and saved field copies all occur in this
+ledger or the preceding parameter/callee ledgers. Borrowed left and right
+have digit lengths at most z+1, since each is at most z. C and B have u and
+v digits. Every row plus its two markers fits E. The direct branch replaces
+the fast-only fields by zero or one, while still constructing addresses
+and gaussians; it therefore fits as well.
+
+## History and consequences
+
+`Tape.write` extends a tape exactly to `head+1` when necessary. Nothing
+reached here truncates `cells`. Thus each tape's extent is exactly the
+maximum of its initial extent and every write index plus one so far. The
+ledgers show that computation cannot extend it beyond E. Cleanup can write
+through an older larger body, already in the prior maximum, and cannot
+extend it. Induction over writes and calls proves the history theorem,
+even with arbitrary finite initially erased tails.
+
+For the production law, `a=s*K <= d*K`. Since `K^500 <= d` and
+`d^1000 <= p^997`,
+
+```
+a^500000 <= p^499497.
+```
+
+For fixed construction constants the cold bound is therefore
+`O(left+right+p^(499497/500000)+bitlength(p)+u+v)` cells. In particular it is
+`O(p+left+right+u+v)`.
+
+A bound linear only in encoded input digit lengths is impossible with
+unrestricted side widths. Fix p=2, s=right=0 and C=B=1. For every integer
+N>=0 set left=N. This direct-branch family has saved `gaussians=2^N`, with
+exactly N+3 cells through RIGHT in its cold field. Borrowed left has only
+max(1,bitlength(N)) digits. Conditional on successful execution, this lower
+bound follows directly from the saved output. The usual Count primitives
+terminate and this direct branch uses a fixed number of leases, so this
+family also supplies actual successful calls. This explains why the complete
+planner cannot inherit the callee's logarithmic bound without a caller
+restriction on numeric side widths.
+
+The proof concerns numerical backing of successful planner calls. The
+enclosing root, its payload, precision accuracy, movement costs, arbitrary
+exceptional exits and the five framework assumptions remain outside scope.

research/rootplan-backing-envelope/README.md

@@ -0,0 +1,119 @@
+# Complete encoded RootPlan backing bound
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Scoped written proof with finite source-bound corroboration. The complete
+unchanged PR5707 `MinimumRootPlan.compute`, including its 256 scratch tapes
+and 29 retained field tapes, has a history-aware numerical backing envelope.
+This answers the caller-transfer question in JoyboyBrian's
+[PR #6098](https://github.com/CrocSwap/integer-mult-bounds/pull/6098).
+
+For successful calls with precision p, selected width s, spacing K,
+side widths left and right, coefficient count C, outer rows B, and fixed
+construction constants m, F, g, define
+
+```
+b=bitlength(p), u=bitlength(C), v=bitlength(B),
+c=ceil(log2 F), h=m-1, z=left+s*K+right,
+E=8+max(1994*b, c*h*b, z+u+v+b+g).
+```
+
+Physical tape i has extent at most `max(initial_i,E_1,...,E_j)` through
+call j and cleanup. The total is the sum over all 285 tapes. A cold planner
+therefore has the sufficient bound `285*max_j E_j`. The full domain and
+complete expression ledger are in [PROOF.md](PROOF.md).
+
+For the production parameter law, `(s*K)^500000 <= p^499497`. With fixed
+construction constants the cold bound is
+`O(left+right+p^(499497/500000)+bitlength(p)+u+v)`.
+The numeric side widths cannot simply be replaced by their bit lengths:
+the direct p=2, s=right=0, C=B=1 family stores `gaussians=2^left`, requiring
+left+3 cells through RIGHT.
+
+## What is new and what is assumed
+
+JoyboyBrian's PR6098 bounds the standalone minimum-prefix callee on a
+32-tape pool and explicitly excludes the enclosing planner. We cite that
+mathematical envelope as an input, without auditing or rerunning that
+package. The new step accounts for all other live caller expressions,
+parameter arithmetic, large saved powers, both caller branches, all 285
+physical histories and erased warm tails. Saturated multiplication is
+charged for its uncropped intermediate, before applying the cap.
+
+Ali Romman supplied PR5707's complete encoded planner and PR5688's minimum
+prefix theorem. Jose Manuel supplied the physical RootPlan and Count cohort
+in PR3385. The retained sources preserve their complete predecessor notices,
+including commdata2338's reached-depth result and the address/geometry lineage.
+The per-tape high-water identity is elementary and is also used by PR6098.
+The contribution is the complete caller envelope and its explicit dependence,
+with no priority claim for that general identity.
+
+## Reproduce
+
+From the repository root, using CPython 3.12 and its standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/rootplan-backing-envelope/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -W error -B research/rootplan-backing-envelope/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rootplan-backing-envelope
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rootplan-backing-envelope --check-source-history
+```
+
+Set TMPDIR to a scratch directory to choose where the unchanged source
+loaders extract their temporary trees. The verifier removes those trees on
+exit and writes its hash-bound receipt to stdout. It changes no source file.
+The marker is `PASS_ROOTPLAN_BACKING_ENVELOPE`.
+
+The checker runs seven complete planner calls and observes every owned
+write, checking the exact high-water identity and the new envelope. One
+call uses the production parameter law at p=2. Six use the predecessor's
+explicit reduced tuple `(d,K,G,H,delta)=(8,1,1,1,32)` to reach both branches,
+in cold and reused warm histories. These fast fixtures exercise the caller
+body; they are not production-law fast cases. All seven borrowed inputs,
+all 29 canonical fields, pool closure and owned cleanup are checked.
+
+Further controls check 256 parameter substitutions, seven address-power
+lower-bound fixtures, rejection of digit-only side-width accounting, and
+failure of a fresh-history bound on preexisting erased backing. The finite
+checks corroborate the proof. They do not quantify over all inputs.
+
+## Limits
+
+The sufficient constants are conservative. The theorem concerns successful
+planner calls with the stated ownership contract. It does not prove pool
+sufficiency on every input, exceptional-exit cleanup, Python heap bounds,
+RootLayer payload storage, movement/time costs, numerical accuracy, any
+selected framework assumption in full, or a new kappa. The standalone callee
+theorem is a cited mathematical premise. Independent human and proof-kernel
+review are unclaimed. No predecessor scientific suite or full selected
+supplier replay is required for this scoped addition.
+
+## Open next questions
+
+The structured questions are also in [TASK.json](TASK.json).
+
+- Bind actual root caller restrictions on left, right, C and B to this
+  envelope. Start with one descriptor producer and include retained backing
+  outside the planner. The remaining RootLayer storage ledger is a blocker.
+- Replace the conservative 1994*b parameter term by a sharper source-bound
+  bound, or change the capped multiply implementation to avoid full temporary
+  products. First identify its maximum reached product. A replacement needs
+  its own physical cost and ownership proof.
+
+## Verification design decisions
+
+The write observer delegates to actual complete source execution. Source
+binding, caller execution and publication checks are separate. Functions are
+under 60 lines. Fixture sets, the 285-slot state and five source-tree owners
+are fixed and bounded.
+
+Power of Ten deviations, rules 3 and 9: Python and the inherited interpreter
+allocate dynamically, and observation requires replacing one Tape.write call
+with a wrapper. Scope is this bounded checker only. The wrapper has one
+original target, delegates each write exactly once, checks the resulting
+physical extent, and is restored in finally. Fixed fixture sets bound live
+observer state; the finite parameter/word sizes bound the source run. Warning-
+strict normal and optimized replays verify this path. The five source loaders
+are explicitly cleaned up in finally. The proof does not infer a Python heap
+bound from numerical tape extents. A future runtime port must replace these
+managed allocations and callback with its own bounded observation mechanism.

research/rootplan-backing-envelope/SOURCES.json

@@ -0,0 +1,48 @@
+{
+  "schema_version": 1,
+  "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/encoded-minimum-root-prefix/SOURCE-INDEX.json",
+      "usage": "input",
+      "git_blob": "c899b4bda006b247a909751f8e9c51190c111032",
+      "sha256": "a82d9be25cc5457a0dea248d51558da5b5b68fbde0c342238bc500fab50da4ef"
+    },
+    {
+      "path": "research/encoded-minimum-root-prefix/SOURCES.json",
+      "usage": "input",
+      "git_blob": "edcab2a10cecf01396076b8947017a7f1ae25e46",
+      "sha256": "acc4f3e5d165b4ba62627fe4465c94dc748109424009b058e7b15bd9dbbd0391"
+    },
+    {
+      "path": "research/encoded-minimum-root-prefix/planner.py",
+      "usage": "input",
+      "git_blob": "7a94b98a8fe4dc6b34c749527a43866ab49b155e",
+      "sha256": "8a65edc901f95fc24082eea6503309fedef8eb2a0d66701d0daf9dd0e136383f"
+    },
+    {
+      "path": "research/encoded-minimum-root-prefix/retained.py",
+      "usage": "input",
+      "git_blob": "8149c0dbea1b09ccc4a93bccbe318e9cbc2ac5d4",
+      "sha256": "35f0070900a82164bcb3e570c155d95d0a84d54a62252e33d74dc4848176347c"
+    },
+    {
+      "path": "research/encoded-minimum-root-prefix/source-snapshot.tar",
+      "usage": "input",
+      "git_blob": "991cfca61a091e10168b1647e1ae55c644cdcd85",
+      "sha256": "3e901efd15eafce0d9b1f11d452a294229e08b0cc06ddb6fc0bef8157dc3c08f"
+    }
+  ]
+}