[petalas]

Summary

Complete the emitted constant-overhead packed TM backend left open by Dugongue / David Ganz's #4538. Claim type: scoped simulation proof with exact finite corroboration. The new dense fixture initializes 256 tape cells in 128 packed data words. No new kappa or selected-frontier change.

length-prefixed scale and tape words
  -> emitted packing setup and input initialization
  -> simultaneous reads, dispatch, writes and signed head updates
  -> exactly m raw output symbols
  -> terminal HALT

Only research/emitted-packed-tm/ is added. PROOF.md proves the all-input invariant under well-formed-input, initially blank-field and nonwrapping-width premises. It derives a complete successful-instruction envelope and a tape-word bound. The emitter returns ordinary primitive instructions; no host TM step or packed access remains in the generated program.

Credit #4538 for its representation, access kernels, unpacked compiler and open question, and its retained RamStd/Problem 1.8 and Szymon Torunczyk simulation lineage. #4883's older retained-read improvement is credited context, not integrated. #4541's stronger tabulated transfer and #4724's portfolio are distinct precedents. The new contribution was produced by Nick Petalas. Classical packing and simulation retain their credit.

Advance CLAIM.

Evidence

• Before: the source has a complete emitted unpacked compiler and separate packed GET/SET kernels; its complete packed backend is explicitly open. After: initialization, signed heads, dispatch, fixed raw output and halt are all emitted and executed.
• 294 new-emitter fixtures pass: 277 halting runs, 17 nonhalting prefixes, 1,907 TM transitions and 419,591 successful RAM instructions. Block sizes 1,2,4,8,16, both sign crossings, four tapes, supported alphabets, nonzero output-tape choices, simultaneous cross-copy and preserved unused high bits are exercised.
• Twelve additional paired fixtures agree with the pinned unpacked compiler. These support the new construction's conformance; no predecessor scientific test suite is audited or replayed as the deliverable.
• Six actual emitted-code mutants and eight invalid machine specifications reject. The separate dense fixture uses exactly 128 packed data words and 9,757 successful instructions for 256 initialized symbols and 128 raw outputs.
• CPython 3.12.15 warning-strict direct commands pass in 1.761 and 1.790 seconds, with identical normal/optimized receipts. These are timeout-budget observations, not performance claims. Both registered commands, metadata/pins and committed byte/source-history checks pass. Eleven package/input files are bound to the commit.
• Official export and all three declared input checks pass. Both Git-free replay modes pass; all twelve exported files, including the export manifest, retain their hashes. A real predecessor-source corruption rejects, and the source is restored afterward. No receipt was hand-written.

From the repository root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/emitted-packed-tm/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/emitted-packed-tm/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/emitted-packed-tm
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/emitted-packed-tm --check-source-history

Expected markers: PASS_EMITTED_PACKED_TM, PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES. Another host's CPython 3.12 path may replace the displayed interpreter. Standard library only.

Limitations

The supplied emitter accepts at most four tapes, alphabet size four, sixteen states and one million instructions. The scale parameter is explicitly presented; a particular caller must justify its relation to input length and provide the execution/address envelope needed for logarithmic word width. Output is exactly m raw symbols, not an integer codec. Final simulated tapes are preserved, but owned tape/control storage is not erased.

The written induction establishes the universal scoped claim; finite fixtures corroborate it. Lean/RamStd.step refinement, complete multiplication-machine materialization, physical/native integration, caller cleanup, rounded arithmetic, stock, precision and analytic recovery remain unrun or unsupplied. All five selected framework assumptions remain. Independent human and formal proof-kernel review are unclaimed.

Open next questions

• Integrate Reduce packed tape read/write access from 30 to 17 instructions (no new κ) #4883's retained-read slabs only after proving that the full dispatcher preserves every cache. Start with one distinct-tape transition; clobber control is the blocker.
• Instantiate the backend with a complete multiplication caller, actual scale/width and charged IO/cleanup. Start with its finite machine and polynomial execution envelope; that full caller remains absent.

Related open work

The completion refresh inspected this account's open PRs created since the advance CLAIM at 2026-10-30T11:26:07Z. There are sixteen, including this PR; none of the other fifteen studies this complete emitted packed TM backend or computes its instruction/storage fixture. No additional same-object comparison or numerical disagreement was found, and no predecessor computations were rerun for this refresh. The earlier live open-PR list and complete cached overlap corpus were also inspected. Coverage excludes unpublished work and arbitrary code diffs; absence of matches is not a novelty certificate.

CI notes

Both hosted checks passed for head 0866b9f620c3ad64a4f3c1c0aa332c8f80eeb435 in run 41049420009: plan and replay (research/emitted-packed-tm). The completed checks were read once and confirmed successful. Hosted replay certifies execution of both registered finite checks; the universal scoped simulation theorem rests on the written proof. Independent human and formal proof-kernel acceptance remain unclaimed.

Every registered scientific command and the publication/source-history checks also passed locally; nothing was deferred solely to hosted replay.

Merge Danger

Two-way door. Blast radius: isolated. The PR adds one scoped research package and changes no shared tool, predecessor source, selected result or frontier.