[petalas]

Summary

Add a scoped constructive proof and executable retirement graph for the failure-reuse question left open by Jerry Chen / CubeJerry #7427. After a finite rejected reversal, the new 26-tape, 2,145-location graph preserves all public contents, erases private work and restores every head. A valid call can then reuse the same banks. No new kappa or selected-frontier change is claimed.

simulate source and mark each tape's visited interval
on either terminal outcome:
    erase marked private cells, retaining each origin marker
    return every head to its origin and erase every monitor
    halt with the source's accepting or rejecting status

The written bound is 5T+16L+6n <= 21T+22n, where T is the finite source-run length and L its total visited span. Here n=13, so the bound is 21T+286. Added history is charged explicitly. The visited-interval method is classical; the explicit transformer and this supplied-interface application were produced by Nick Petalas. The successful reversal and its rejection-time public-preservation property are cited predecessor premises, not audit deliverables.

Base e54523517d0f03e58352e647c403a5af3e525a57, priority revision 8. Card formal-interface-lemma changes scope to #7427 Open next question 4. Advance CLAIM.

Evidence

• Before: Implement complete-record row reversal from encoded elementary descriptors with a fixed finite tape program #7427 preserves public contents on rejection but leaves private retirement and head return unclaimed.
• After: the emitted graph passes 518 valid packets, 25 malformed packets, a rejected-then-valid reuse chain on the same 26 objects, 16 generic left/right fixtures and eight rejection controls. Public contents, exteriors, owner identity, head return, erasure, retained history and instruction bounds are checked. The receipt is generated and bound to the proof, source manifest, compiler and verifier hashes.
• CPython 3.12.15 on macOS arm64: both registered warning-strict commands pass in 0.4320 and 0.4186 seconds. These are check runtimes, not speedup claims. Metadata/source pins, full registered replay, committed bytes/modes/source history, official export/check and a read-only Git-free exported replay pass.

From the repository root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B -W error research/row-reversal-rejection-cleanup/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B -W error research/row-reversal-rejection-cleanup/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/row-reversal-rejection-cleanup
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/row-reversal-rejection-cleanup --check-source-history --check-modes

Expected markers: PASS_ROW_REVERSAL_REJECTION_CLEANUP, PASS_REGISTERED_RESEARCH_PACKAGE outcome=completed, and PASS_RESEARCH_COMMIT_BYTES. Another machine may substitute its CPython 3.12 path. Exact #7427 source bytes at 7662d01d827c95d90032579c168cae78aa531f2f and original notices are retained locally, so no pending source object or network is required for the direct replay.

Limitations

Private visited cells and the additional thirteen monitor windows must be blank on entry and supplied by the caller. The theorem covers a finite source halt or rejection; it supplies no cleanup after interruption or nontermination and no rollback of earlier public writes. Runtime is linear in the actual rejected execution, which may exceed actual DATA length for oversized descriptors. Caller allocation, complete native/caller composition, common-grid admission and the selected cold replay are unrun. Independent human and formal proof-kernel review are unclaimed.

Open next questions

Can fewer monitor tapes retain the four-symbol alphabet and constant-factor time? Begin by proving a head-displacement relation on every malformed path. Can a concrete caller reject excessive descriptors before expensive unary expansion? Specify an encoded resource cap and a pre-write contract. Neither obligation is supplied here.

Related open work

• Implement complete-record row reversal from encoded elementary descriptors with a fixed finite tape program #7427 supplies the whole-record reversal and explicitly leaves failure retirement open; this package adds that contract.
• Generate the actual native translation descriptors from the five-field header and execute its complete same-owner pass #7428 constructs descriptors and applies the original reversal to one selected translation; its producer and caller are not transformed here.
• Implement the outer layer phase sweep from its actual encoded header with a fixed finite tape program #7425 supplies a related literal layer-phase graph with success-only retirement; no new cleanup or cost is claimed for it.
• Lower the current selected quadratic Gaussian phase to a fixed tape table with complete owner return #7426 supplies a related literal native-phase graph with success-only retirement; no new cleanup or cost is claimed for it.
• Implement both selected Gaussian linear maps as fixed tape programs with every column and complete owner return #7430 supplies the selected binary-matrix tape programs; this package changes no matrix word or complete MOVE bill.

Completion refresh checked the seven other account open PRs created since the advance CLAIM: #7469, #7470, #7471, #7472, #7473, #7474 and #7476. They concern a one-step threshold, integral shear biclique, rounded affine-lattice hull, partition optimum, field-extension certificate, rounded half-shear and Type A sign gauge. None studies reversal rejection retirement or computes this graph's instruction bound, so no additional same-object line or numerical comparison is needed.

CI notes

CI did not certify this package. At unchanged commit 4fffa69c79ead4eb92e862daec4015b05c12d622, run 43291152300, plan job 131437419998, failed in Onboarding helper tests. The job log reports exactly one failure out of 760 tests, 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 replay job was skipped, so no hosted replay ran this package.

This is a repository-level mismatch on main e54523517d0f03e58352e647c403a5af3e525a57: certificates/selected-result.json names make frontier7000-verify, while the current section of docs/ci-verification.md still describes #6030 and make frontier6030-verify. I read both main files and the failed job log; this PR changes neither file. I also read the failed logs of rohanarun run 42905094314, dillona run 42903313790 and petalas run 43289883200. Each reports the same sole failing test and missing-command assertion, 760 tests and 24 skipped. No fix, retrigger commit, push or workflow rerun was made.

The package checks in Evidence passed locally at this commit. git diff --check reports the pre-existing blank line at EOF of the exact retained inputs/reversal/reverse.py export. Those source bytes are preserved; the diff check passes when that frozen file is excluded.

Merge Danger

Door: two-way. Blast radius: one isolated research package. No selected record, shared runtime or predecessor file changes.