[petalas]

Summary

Reduce the supplied literal phase/egress boundary from 36 physical tapes to 20, including two public owners. This scoped constructive proof answers CubeJerry #7425's explicit shared-bank question. The existing component arithmetic and successful retirement are cited premises, not audit deliverables. The new shared graph and composition proof were produced by Nick Petalas.

same twenty tape identities:
  entry 17814: literal input phase; return
  supplied exact C and format service, outside this graph
  entry 0: literal egress; fixed jump; literal final phase; return

The fixed graph has 19,960 locations. All sixteen egress private roles share the phase bank after successful retirement. Head return, original DATA ownership and all historical backing remain charged. The exit costs exactly the sum of the original egress and final-phase instruction counts. This improves an inventory upper bound; it claims neither a global tape minimum nor lower total visited space. No new kappa or selected-frontier change.

Only research/shared-phase-egress-bank/ is added, from canonical main e54523517d0f03e58352e647c403a5af3e525a57. The formal-interface-lemma card is explicitly changed to this supplied physical-boundary result. Exact pending-source bytes and original notices are retained locally with SHA256/Git-blob pins; replay needs no predecessor verification suite, remote fetch or unmerged Git object. Advance claim.

Evidence

• Before: Implement the outer layer phase sweep from its actual encoded header with a fixed finite tape program #7425's direct wrapper allocates 18 phase-private and 16 separate egress-private tapes plus two public tapes, for 36.
• After: the new two-entry graph passes 19 joined calls, 378 Gaussian coefficients and 1,297,236 literal instructions on the same twenty objects. It checks values, all heads, private erasure, opaque exterior, old-tail cleanup, all sixteen shared roles and historical unions across growing/shrinking packets. Five rejecting controls cover bad jumps, nonliteral opcodes, physical aliasing, exhausted execution budget and an omitted final phase.
• Warning-strict normal and optimized CPython 3.12.15 receipts agree exactly. The two registered commands took 0.1973 and 0.2182 seconds locally. These are check durations, not speedup claims. Registered replay, metadata/source pins, committed bytes/modes/source history, official export integrity and both read-only Git-free exported replays with empty PATH pass. Exported files remain unchanged. The direct marker is PASS_SHARED_PHASE_EGRESS_BANK.

From the repository root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error research/shared-phase-egress-bank/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B -W error research/shared-phase-egress-bank/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/shared-phase-egress-bank
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/shared-phase-egress-bank --check-source-history --check-modes

Another machine may substitute its CPython 3.12 path. The verifier prints a generated receipt bound to package and graph hashes. PROOF.md gives the unbounded composition argument; finite fixtures corroborate it.

Limitations

Both routines require supplied blank private windows covering their combined visits. A larger invocation needs blankness of newly visited cells. This does not merge two arbitrary dirty banks. Rejection/interruption cleanup and rollback are unclaimed; the final phase retains its signed-range condition. The exact C producer, common-grid format conversion, source acquisition, caller allocation and their costs remain additional obligations. Test C production is an explicit outside oracle. No selected cold replay, full supplier, complete multiplier, independent human review or proof-kernel acceptance is claimed.

Open next questions

Bind one actual C producer to the same header, address order, common grid, signed headroom and retired shared bank, and price its format conversion and allocation. Begin with one pinned caller occurrence. Further tape reduction requires changing simultaneous component liveness; this proof supplies no such construction or lower bound.

Related open work

• Implement the outer layer phase sweep from its actual encoded header with a fixed finite tape program #7425 supplies the literal outer phase, direct 36-tape wrapper and shared-bank question. This adds the twenty-tape graph and its successful-lifetime composition proof.
• Normalize the selected complex layer and perform its single toward-zero return with a literal 18-tape program #7422 supplies the retained literal normalization/egress and its numerical/retirement theorem. Its arithmetic and graph remain unchanged.
• Retire reversal banks after rejected packets (no κ) #7477 adds rejection retirement to a whole-record reversal, a different failure contract. This construction uses no result or executable from it.
• #7503 proves a linear-observation minimum for a selected native tensor phase. This concerns a different phase boundary and computes no competing tape count.
• #7509 streams general quadratic phases with an abstract arithmetic bill. This supplies no physical tape allocation or competing tape count.

The own-open-PR closeout check inspected the seven other account contributions created since the CLAIM: #7502, #7503, #7504, #7505, #7506, #7507 and #7509. The two related phase results are listed above. The other scopes concern column-plane geometry, canonical rotation routing, exact inverse preparation, cubic repair and interaction-error bounds. No extra mathematical computations were run to compare them.

Credit CubeJerry, aliromman #5375, tekuuu #3127, jmbarrancoml #2287 and #3087/#3091/#3098, JoyboyBrian #5329, 1337isnot1337 and pinterbanget #4325, the upstream stream/layer authors and all unchanged source notices. Lifetime sharing is elementary; the source-specific graph, proof and evidence are the contribution.

CI notes

CI did not certify this package. At unchanged commit 82d677390993e28e12a0203169a69d9d929aa5a2, run 43437279341, plan job 131925534865, failed in Onboarding helper tests. I read the checks once and inspected the actual job log. Exactly one of 760 tests failed, with 24 skipped: test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record, at tests/test_research_current_status.py:58. The AssertionError says that `make frontier7000-verify` was not found in the CI verification document. The package replay job was skipped after planning failed, so no hosted package replay ran.

I inspected the base Git objects at e54523517d0f03e58352e647c403a5af3e525a57: certificates/selected-result.json names make frontier7000-verify, while docs/ci-verification.md still describes #6030 and make frontier6030-verify. Those files and the test are unchanged by this PR; its diff contains only the sixteen isolated package files.

I also read the failed-job logs for rohanarun's run 42905094314, dillona's run 42903313790, and petalas runs 43437283229, 43437288667 and 43437529382. Each reports the same sole failing test and missing-command assertion, 760 tests and 24 skips. Run metadata confirms the named fork owners. This is evidence of the shared repository-level failure and provides no mathematical certification for this package.

The local checks listed above remain the evidence at the unchanged commit. No fix, retrigger commit, push, shared-file edit or job rerun was made in response to the failure. Maintainers own the repair of main.

Merge Danger

Door: two-way. Blast radius: one isolated research package. Shared code, predecessor files and selected records are unchanged.