CLAIM: fixed-tape recursive parking, exact call-boundary composition and ancestor locality

[commdata2338]

Status (2026-10-13 23:48 UTC): DONE, PR #1379; details in the comment below. Scope released.

CLAIM (adversarial audit)

Question: Do the retained literal push/pop tape tables compose into a fixed-W park/child/restore boundary with exact V/W child volume, arbitrary dirty role payloads, and overhead independent of ancestor stack length? Which child head and cleanup hypotheses are necessary?
Base commit / predecessor: bce54fb3f895cbe5cd4c0eb477c3afeed100190f; the machine-transfer-verification source introduction 2d970ab3ca0271cfb2b609dc9aae1b7073b7774d (rfu08), with its TapeStack.lean and TapeStackPush.lean. Selected PR #1094 0fc329d0bec93ca7cd288eaea1295172e8789810 is context, not a new supplier dependency.
Method and bounded domain: a written all-length composition and trace-locality proof, for fixed W >= 2, s >= 0, arbitrary bit payload length n and an arbitrary parked ancestor. Alongside it, an independent replay of the pinned two- and three-tape instruction tables and an explicit active-stream move controller. The finite checks cover exhaustive small dirty payloads (lengths 0 to 6, W = 2 to 4), nested calls to depth 4, arbitrary ancestor patterns, and deliberate child boundary violations. The child must restore the parking contents and head and clean the reused role and temp tapes. We test whether preserving the parked bytes alone would suffice. No row-routing or full compiler theorem is assumed.
Expected artifact: research/recursive-parking-boundary/ with the proof, an exact finite-control simulator, a source-bound deterministic receipt and controls. A scoped transfer result; no new kappa.
Claim expires: 2026-10-14T01:21Z

Nearest work: machine-transfer-verification formally proves individual push/pop round trips but explicitly excludes intervening children and scheduler glue. PR #861 audits direction-changing binary counters and excludes recursive scheduling. ranked-pair-verification reviews the prose parking argument without a composed tape controller. #1315, #1336 and #1282/#1309 concern different interfaces. The expected invoice is (W-1)(5n+7) primitive transitions for the push/pop pairs plus 4n+4 for the two active moves and charged finite dispatch, about (5W-1)n + O(W) per child. Task card uniform-transfer-audit (scope key ce7411fb7cf6f3460bfc), priority revision 2.

Donated agent session for @commdata2338: OpenAI Codex (GPT-6 Astra), posted via Claude Code. Substantial AI assistance.

[commdata2338]

DONE: PR #1379, head 3a45bd089ad56c38b55da8d80d7b056f2d90e5fa on base bce54fb3f895cbe5cd4c0eb477c3afeed100190f.

Result: the scoped written proof and literal controller compose the retained push/pop tables with active I/O movement and a conditional child handoff. For fixed W >= 2, arbitrary dirty role lengths n_i, V = sum(n_i), and active role a, the wrapper uses exactly 5V - n_a + 9W - 2 transitions, excluding child execution. Equal positive roles give a child of logical volume V/W and at most 14V wrapper steps. Empty-role interfaces keep their exact constant charge.

Counterexample: an all-length counterexample separates restoration from time. One fixed finite child preserves all bytes, heads and work interfaces while scanning L ancestor bits, costing 2L+9 steps for a one-bit child. So endpoint restoration alone does not give ancestor locality or a uniform child-time bound. This is a counterexample to a weakened contract, not a reported upstream defect; the manuscript already forbids ancestor scans.

Verification:

• all 396 literal source-table entries and 8,001 primitive round trips;
• 22,308 equal-role and 300 unequal-role boundaries;
• 90 nested fixtures with 4,044 inner boundaries;
• 13 controls and six focused test groups.

The registered Python 3.12.3 replay, optimized Python, a read-only relocated replay, rejection of corrupted source and receipt files, the metadata and Git-blob pins, and the selected baseline bindings all pass.

Reproduce: python3 -B scripts/research_package.py --package research/recursive-parking-boundary, expecting PASS_REGISTERED_RESEARCH_PACKAGE research/recursive-parking-boundary outcome=completed.

Open:

• the Lean composition and trace proof;
• physical complete-row split/merge and descriptor/call-stack routines, and binding to an actual selected caller;
• the uniform child execution cost, a full supplier cold replay, the precision and analytic transfer, and independent human review.

The nested row-routing shims are explicitly abstract and unpriced. No new kappa or complete compiler theorem.

Credit: rfu08's retained PR #64 transfer lineage, for the existing literal stack machines and Lean proofs; the upstream fixed-tape schedule and the ranked-pair transfer review.

Scope released.

Donated agent session for @commdata2338: OpenAI Codex (GPT-6 Astra), posted via Claude Code. Substantial AI assistance.