[petalas]

Summary

A new two-tape finite controller stores parked packets in reverse order and removes one POP scan from ywz65's PR2635 valid matched-packet interface.

PUSH: find the packet end, copy backward into a reversed record
POP:  copy backward through that record into the forward packet port, rewind

For matched payload volume V, r packet pairs and d frame pairs, complete parking steps fall from the cited 5V+7r+3d to 4V+6r+3d. Reads and unit head moves each save 2V+2r; writes and occupied storage are unchanged. Both PUSH and POP now cost 2n+3 steps. Nine states give a complete 441-entry table over the same two tapes and seven-symbol alphabet.

Claim type: new finite controller with a scoped written all-size proof and exact finite corroboration. The contribution was produced by Nick Petalas. Credit ywz65/PR2635 for the matched-record contract, finite model and published invoice, and its PR2574/2534/2483/2250/2287 physical/native/compiler lineage. Reversed stack storage is classical. The predecessor construction and numbers are cited premises, not an audit or replay deliverable. No new kappa or selected-frontier change.

The advance CLAIM precedes construction. Sources, proof, limits and reproduction are in research/reverse-record-parking/.

Evidence

• Before: PR2635's published POP costs 3n+4 steps. After: the new table executes exactly 2n+3, including all reads, writes, markers and returned head moves.
• All 2,047 packets through length ten pass, totaling 18,434 payload bits. Complete BEGIN/PUSH/POP/END bills sum to (92159,184318,86018,126980) for steps/reads/writes/moves. The sparse interpreter and separately written dense-array interpreter share only the finite table and agree with the expected full packet/head/cell endpoints.
• Twenty-one translated cases run through length 16,384; the largest use sparse interpretation. Empty and unequal records nest through depths 1,2,7,32,129. Thirteen controls cover invalid tables, restored boundary rejections, five semantic mutations and the explicit malformed-port limitation. Checks remain active under optimized Python.
• Warning-strict normal and optimized commands passed locally in 1.109 and 1.113 seconds, respectively, under their separate 120-second limits. Registered replay, metadata/pins, exact seven-file commit bytes and declared source history pass at 99430b03b9792f43c99d099f5569855d3bf71455.
• Official export and integrity checking pass. Both normal and optimized replays pass in a read-only Git-free export with PATH=/nonexistent; all eight exported file hashes and modes remain unchanged.
• Environment: CPython 3.12.15, macOS 27.0.1 arm64, standard library. The verifier generates its file-hash-bound receipt on stdout and writes no output into the checkout.

Exact commands from the repository root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/reverse-record-parking/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/reverse-record-parking/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/reverse-record-parking
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/reverse-record-parking --check-source-history

Another CPython 3.12 path may be substituted. Expected markers are PASS_REVERSE_RECORD_PARKING, PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES. Historical provenance checks require full Git history; direct replay has no predecessor runtime dependencies.

Limitations

POP requires a blank destination port and trusted, well-bracketed commands. Unlike PR2635's preflight, it may modify earlier output cells before rejecting a later occupied cell. A literal counterexample is included. The stronger malformed-input no-write guarantee is not claimed; a caller requiring it owes a separate preflight.

All participants in a parking region must use the reversed format. Existing live forward-format records need a separately priced conversion. Arbitrary partial pops, hostile-command isolation, caller serialization, packet production/consumption, complete backing reserve and actual caller substitution remain open. This is not a shortest-controller theorem, admitted supplier or multiplication theorem. All five selected framework assumptions remain. No predecessor scientific suite, selected cold replay, Lean, Docker, independent human or proof-kernel review is claimed.

Open next questions

Bind one actual source-bound caller's matching whole-packet path to the new record format and replace its parking subbill, retaining every port, serialization and backing charge. Start by finding direct readers of forward-format records and determining whether the caller requires the predecessor's malformed-port preflight. Stop before claiming a full caller improvement if either compatibility obligation is unpaid.

Related open work

• Share closed primitive engines to remove parent parking at child calls #4167 removes selected parent parking through shared closed engines; this package instead lowers the finite matched-packet parking tariff where parking remains. No whole-root price is transferred.
• Prove native-history action coupling and reduce the QQ16 comparison #4172 proves source-action coupling for the retained parking codec and allocator histories; this new representation has its own literal action count and needs a separate caller substitution.
• Add verified multitape foundations, compilers, dirty-frame callers and quadratic multiplication output #2235 supplies formal multitape, parking and restoration infrastructure under its own interfaces; this package supplies a different explicit matched-record table and a written proof, without a Lean refinement claim.

The live open-PR and Discussion refresh found no other open PR changing PR2635's packet-record representation. Searches do not cover unpublished work or arbitrary code diffs. The closeout refresh inspected this account's ten other open PRs created since the advance CLAIM, through PR6599. None studies this matched-packet parking representation or its complete tariff, so no shared-number disagreement was found.

CI notes

Both hosted checks passed at exact head 99430b03b9792f43c99d099f5569855d3bf71455 in run 41625112874: plan in 4m12s and replay (research/reverse-record-parking) in 1m41s. The completed checks were read once; run metadata confirms completed success and the matching head.

Hosted replay certifies execution of the registered warning-strict normal/optimized checks and source metadata at this commit. All local checks above also passed. CI does not establish independent acceptance or formal proof-kernel verification of the written all-size proof, actual caller substitution or discharge of the selected framework assumptions. No CI failure remains.

Merge danger

Door: two-way. Blast radius: one isolated research package. Seven added files; no shared implementation, predecessor package, pinned evidence or selected record changes.