[petalas]

Summary

Scoped written proof with finite corroboration; no new κ. The complete unchanged PR5707 MinimumRootPlan.compute has an explicit numerical backing envelope across successful call histories, covering its 256 scratch tapes and 29 saved fields, including erased warm tails.

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 extent_i <= max(initial_i,E_1,...,E_j)

For fixed construction constants, the production law gives a cold bound of O(left+right+p^(499497/500000)+bitlength(p)+u+v). Numeric side widths are necessary: the direct p=2, s=right=0, C=B=1 family stores gaussians=2^left, requiring left+3 cells through RIGHT.

The new step transfers the standalone callee envelope to every other caller expression and physical tape history. It charges uncropped capped-product intermediates and large encoded row/address fields. Produced by Nick Petalas. Credit JoyboyBrian's PR6098 standalone theorem, Ali Romman's PR5707 planner and PR5688 prefix theorem, Jose Manuel's PR3385 physical Count/RootPlan cohort, and the retained source lineage. The standalone theorem is a cited mathematical premise, not a result re-audited here.

Evidence

• Before: PR6098 explicitly leaves the enclosing 256-tape caller history open. Its standalone bound does not account for the caller's other live values or saved powers.
• After: PROOF.md accounts for the complete expression ledger and proves a per-physical-tape history maximum. Seven complete source executions check all 1,961,741 owned writes, every borrowed input, all 29 canonical fields, pool closure and owned cleanup. One uses production parameters at p=2; six use the retained explicit reduced tuple to exercise both branches and warm/cold reuse. These are corroboration, not an exhaustive all-input computation.
• 256 parameter substitutions, seven address lower-bound fixtures, digit-only side-width rejection and erased-warm-backing controls pass. Both registered warning-strict normal/optimized commands pass locally in 1.751 and 1.763 seconds. Metadata, source compilation, staged whitespace, committed bytes and source-history preflight pass. The official 11-file export and its integrity check pass, as does an isolated optimized Git-free exported replay with empty PATH. The verifier generates a receipt bound to all six package files.

Exact reproduction from the worktree root, using the local CPython 3.12 interpreter and standard library:

/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

Scientific source base is canonical main 721c03822c421b7f7fcbb2598993b947c4d88419, refreshed before publication. Five live source files, including the complete authenticated transitive archive, are pinned in SOURCES.json. The cited standalone mathematical source is PR6098 at f8c31f448c633883b21c92a7b4bf3c4cf0d3c729.

Limitations and unrun obligations

Successful-call storage only; constants are sufficient and conservative. No general pool-sufficiency theorem, exceptional-exit proof, Python heap bound, surrounding RootLayer payload/storage bill, movement/time bound, numerical accuracy theorem or complete selected framework assumption is established. Production-law fast cases are covered by the written argument; finite fast fixtures use the explicitly reduced parameter law. No full selected replay, predecessor scientific suite, proof-kernel run or independent human review is claimed.

Open next questions

• Bind one actual root descriptor producer's restrictions on left, right, C and B, then add the nonplanner retained tapes to obtain an enclosing root storage bill.
• Sharpen the 1994*b parameter term or supply a physically charged capped multiplication implementation that avoids full temporary products.

Related open work

Live open-work search refreshed. No additional PR on this RootPlan backing object was found.

• PR #6098 proves the standalone minimum-prefix callee envelope; this contribution cites it and answers its first open question by covering the complete 256-tape caller and 29 fields. Its standalone quantities are not recomputed as this contribution.

CI notes

Uncertified by CI. For head 3f94b96e03ea482bb3d5127463001706d44faa3e, run 40725045913 failed plan in the shared onboarding helper tests. replay (research/rootplan-backing-envelope) was skipped, so the package replay did not run in CI. The local passing replays above remain separate evidence.

The failed tests are:

• test_research_current_status.CurrentStatusTests.test_current_section_matches_selected_record: expects the exact text **0.003125804** in docs/research/current-status.md; main instead puts the decimal and fraction together inside one bold span, **0.003125804 = 781451/250000000**.
• test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record: expects `make frontier6030-verify` in docs/ci-verification.md; that document still presents the PR5599 replay.

These mismatches are already present on base/main 721c03822c421b7f7fcbb2598993b947c4d88419, the PR6030 κ admission pushed with [skip ci]. That commit changed the selected record without bringing the two documentation contracts into agreement. This package changes neither document. I confirmed the same two failures in PR #6120's run 40691776027. Open PR #6050 targets the documentation fix.

A maintainer re-run is required after main is fixed. No CI certification or completed hosted package replay is claimed.

Merge Danger

Two-way door. Blast radius: this isolated research package and its opt-in replay only.