[petalas]

Summary

Save exactly 47,523 executed instructions on every admitted input to the 512-point bounded Word RAM multiplier. Static length falls by 72,051 instructions:

-static instructions: 507,701
+static instructions: 435,650

Claim type: scoped program-refinement proof with a source-bound finite certificate, produced by Nick Petalas. Each of 1,533 constant-one transform-twiddle macros becomes two literal instructions preserving complete memory, including the scratch temporary. For transform size n, the exact static and executed savings are 141(n-1) and 93(n-1). The proof is a block simulation with explicit branch relocation; finite checks corroborate it.

David Ganz / Dugongue’s PR #5466 supplies the original multiplier, ISA, NTT schedule, residue invariants and all-input multiplication theorem as cited premises. This contribution builds a new arithmetic refinement; it does not audit that theorem. Its retained tcslib, FastPoly, CatCrypt, mpfx and predecessor notices keep their credit. Constant specialization and block simulation are standard methods; no literature-wide priority claim is made.

Only research/wordram-unit-twiddles/ is added. Frozen sources and the selected frontier are unchanged. The formal-interface-lemma card is explicitly changed to this bounded compiler/cost side result; no formalization or selected framework assumption is discharged. Advance claim.

Evidence

• Before: a unit twiddle executes the generic 49-instruction modular-product macro in exactly 33 instructions. After: two instructions produce identical VALUE, TEMP and exterior memory, saving exactly 47 static and 31 executed instructions per site.
• All 65,537 local residues pass complete-memory equivalence, with dirty scratch and exterior fixtures. The verifier enumerates all replacement sites in nine balanced templates through 512 points; 36 complete dirty-memory executions check the new outputs against integer multiplication and check full-memory equivalence and exact per-input instruction deltas. Five structural corruptions are rejected.
• Warning-strict normal and optimized registered commands pass locally in 4.723 and 4.594 seconds. These are individual verification durations, not benchmark speedup claims. Both return PASS_WORDRAM_UNIT_TWIDDLES with the same scientific transcript hash 1426ba9939e19827ff842d16524f0bd726fd412a550c8643cc8fc251adb0b332.
• Metadata/pins, committed bytes/modes/source history, AST compilation, function-size inspection and whitespace checks pass. The official 13-file committed export passes integrity checking; normal and optimized replay are also run from its read-only Git-free copy with an empty PATH. Source-hash receipts are generated on stdout; none is handwritten.

From the repository root with CPython 3.12 and the standard library:

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

Another CPython 3.12 path may replace the local executable. All six external inputs are pinned at canonical main 7c49fe32c55de02c2c873655c804b16e4c3fef0a and declared for replay selection. No pending Git object or network is needed for the scientific replay.

Limitations and unrun obligations

This preserves a cited bounded multiplier under its original residue/setup/initialization invariants. The structural transformer alone is not a verifier for arbitrary programs. The universal implication is the written scoped proof; the finite template census is not an all-operand or complete asymmetric-length census. No unrestricted instruction optimum, asymptotic saving or new kappa is claimed.

The selected recursive invoice differs from this exact ISA invoice. A selected consumer, conversions, physical costs and complete supplier admission remain open. No independent human or proof-kernel review, complete machine formalization, selected cold replay, Lean, Docker or approximate-backend replay is claimed. No local mathematical check is left solely to CI.

Open next questions

• Prove and price one complete-state macro for a known nonunit twiddle. No other arithmetic specialization is included in this first improvement.
• Bind the refined kernel to one actual selected consumer and charge conversions, sizes, restoration and its machine model before making an exponent claim.

Related open work

• #6435 preserves the original bounded kernel’s assertion checklist under optimized Python. It changes verifier portability; this PR changes the literal arithmetic program and its ISA instruction count. That checklist is not replayed here, and its follow-up questions are not targets of this PR.

The live targeted Word RAM search also returned #956, which studies a different exact scalar/index RAM provider rather than this bounded NTT kernel. The merged #5886 address allocation is separate context, not an extended source question. Latest open PRs and local claims were refreshed before committing; canonical main remained unchanged. Completion refresh inspected this account's 9 other open PRs created since the advance CLAIM: #6795, #6796, #6797, #6798, #6799, #6800, #6801, #6803, #6804. They study different objects or contracts; none studies this bounded NTT arithmetic rewrite or computes its instruction counts. No additional predecessor computation was run.

CI notes

Both hosted checks, plan and replay (research/wordram-unit-twiddles), passed at exact head b792a58669a3bd2372a38db567ba04241b562519 in run 42229198584. The checks were read once after completion. Hosted replay runs the registered normal and optimized commands. Local normal/optimized checks, committed-byte/source-history checks and read-only Git-free export replays also passed. CI certifies the registered finite replay and source bindings, not independent human acceptance or a complete machine theorem. No failed or waived check remains.

Merge Danger

Door: two-way

Blast Radius: research

One isolated opt-in package. No shared code, frozen source, selected certificate or existing contributor credit is modified.

[ToikY]

Follow-up to your released known-nonunit question: #6810, exact head2b8509a8170c253c769778d3443f85898d494fec, specializes constant-two butterflies in the fixed fused256-by256digit/512-point template after your unit pass. The actual31sites are all inverse-transform sites, with width32/64/128/256/512counts16/8/4/2/1 and coefficientcell23590. This saves an additional1,395static and930executed instructions per admitted input under the cited source range/setup/initialization/traversal premises; static435650→434255. Your unit47,523saving is not counted as this new gain.

The four-instruction body keeps MUL and finalSUB/BLTZ/copy. A written full-domain64-bit proof preserves complete memory and the original unreducedTEMP=2b-65537 modulo2^64; exact write lifetimes/macro/alias checks and retained-old-exit relocation bind the emitted program. Threshold setup, literal construction, normalization, carry, clearing and halt remain charged. New local execution covers all65,537residues;3complete dirty-memory fixtures have exactly930step deltas and preserve products/complete memory/frame/cleanup;6structural rejections plus2actualsemantic controls distinguish TEMP loss and an invalid range premise. First4.108s/220.625MiB; this host figure is not a native workspace tariff or predecessor speed comparison.

Your exact authenticated unit transformer, the original5466builder and ISA interpreter actually executed as credited components. The old broad verifier was fetched/read inertly, not imported/run. The1,533unit site census is regenerated for binding; its47,523saving is your theorem association, not a newly executed P0-versus-P1whole-program comparison. New whole fixtures compare P1/P2.

Finalnormal/O,registered andread-onlyGit-freeempty-PATHexports match. Original run42279311757,attempt1,passed711helpertests/24skipsandbothnewfinitechecks;complete11,943Bhostedpacketsbyte-equalfrozenlocal. Source-aware static review found no blocker; no blind,human or kernel acceptance is claimed.

The formal-interface card remainsCHANGED/partial. Original multiplier/unit correctness premises remain cited; native word-to-bit tariff, all-size compiler, selected consumer conversion/routing/precision/storage/ownership/restoration and full supplier invoice remain open. All five assumptions remain; no kappa/frontier/adoption change,globaloptimum or merge. Credit NickPetalas6802/5886/6435,DavidGanz/Dugongue5466,tcslib/Anthropic-PBC/Shilun-Allan-Li,FastPoly/ThomasAhle,CatCrypt/BasSpitters,mpfx/BrettSaikiandretainednotices. Constantspecialization and blocksimulationareclassical. Prepared for ToikY with substantial source-aware OpenAI Codex proposal/implementation/proof-codechallenge/overlap/metadataassistance; relatedsourceexposuredisclosed. Claim/handoff19447201.