[petalas]

Summary

Scoped written proof with exact finite corroboration: the complete once-rounded MOVE of CubeJerry's #6996 admits a smaller sufficient lifted-record allocation. Write g=r*f and k=ceil(g/2).

- lift g bits; width h+g+ceil((g+1)/2)+1
+ lift k bits; width h+2k+1

The new source-interface substitution preserves every exact Gaussian prefix, both serial monomials, the original absolute phase, final nearest-up rounding and true final-overflow contract. It saves s+1 component bits at g=2s and s bits at g=2s+1. At g=8 the saving is five bits per real component. The example h=2, f=1, r=8, 4096 complete records and one complex coefficient reduces the widened coded field from 417792 to 294912 bits. This is an exact record-size calculation, not a physical run or total runtime claim.

The source domain is #6996's retained #6030 raw catalogue. Its placement in the currently selected #7000 caller remains open. Only seven files under research/sharp-rounded-move-allocation/ are added. No frozen provider, selected record or rank invoice changes.

The allocation proof and new reference were produced by Nick Petalas. Credit CubeJerry #6996/#6989 for the complete source contract and variable lift/drop codec; Alejandro Zarzuelo Urdiales #45, Jose Manuel / jmbarrancoml #3091 and Nick Petalas #2772/#3089 for the cited sharp Gaussian denominator/row-norm and prefix facts; and the monomial, cutoff, native and tape lineage retained in those sources. The Gaussian facts are cited inputs, not claimed as new or re-audited. Independent human and formal proof-kernel review are unclaimed.

Advance CLAIM. Canonical base and refreshed main: e54523517d0f03e58352e647c403a5af3e525a57, priority revision 8. The card is explicitly changed to a local precision/storage side result.

Evidence

• Before, Research: Rounded selected MOVE #6996 uses a g-bit lift and general unitary headroom. After, the cited sharp Gaussian prefix facts prove integrality at a k-bit lift and stored-component magnitude at most 2^(w-2), including arbitrary signed inputs and every entrance/exit phase.
• The new verifier checks 32768 allocation cases; 131584 complete small input cases and all 1050624 output components; 320 larger boundary cases; 4064 signed codec round trips; 31320 drop/range cases; and the documented invalid-allocation, insufficient-reserve and rounding-order controls. A dense literal tensor engine checks the independently implemented butterflies. The all-source/unbounded claim rests on the written proof.
• Both registered warning-strict normal/optimized checks pass locally on CPython 3.12.15, macOS arm64. The final separately timed direct checks took 3.30 and 2.77 seconds, below their 120-second limits. Computed normal/optimized hash-bound receipts agree.
• Metadata/source pins, in-memory source compilation, staged whitespace and committed-byte/mode/source-history checks pass at 2b882fd2834303655f82d084e25dc551f67e9784. The publication preflight authenticates eleven package/input files and the declared canonical ancestry.
• Official committed export and integrity check pass. Both direct replays from a read-only Git-free export with an empty PATH match the local receipt. No predecessor scientific verifier or selected cold replay ran.

Exact reproduction from the repository root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/sharp-rounded-move-allocation/verify.py --emit
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/sharp-rounded-move-allocation/verify.py --emit
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/sharp-rounded-move-allocation
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/sharp-rounded-move-allocation --check-source-history --check-modes

Other machines may substitute their CPython 3.12 interpreter path. Scientific marker: PASS_SHARP_ROUNDED_MOVE_ALLOCATION; registered marker: PASS_REGISTERED_RESEARCH_PACKAGE; publication marker: PASS_RESEARCH_COMMIT_BYTES. --emit computes the receipt from current file hashes and checks, without writing a checkout artifact.

Limitations

This is a sufficient allocation substitution theorem under the retained provider premises. The literal Count/Tape substitution is unimplemented, and no physical whole-MOVE execution is claimed. Finite endpoint checks use two explicit abstract monomial pairs, not actual selected source recipes; they do not replace the proof or inherited contracts. The containing error fibre still includes all 9f native axes.

All fixed roles, protected stages, both serial repetitions, constructor/source/control work, restoration and historical backing remain charged. The complete bill must be recomputed at the smaller physical widths. No paid/productive rank saving, new kappa, supplier admission, actual #7000 caller mapping or complete multiplication theorem follows. All five selected framework assumptions remain. Physical execution, selected cold replay, Lean, Docker, independent human and formal proof-kernel acceptance are unrun or unclaimed.

Open next questions

• Implement the literal preparation substitution and execute one full admitted nine-block MOVE, including both protected stages and every fixed role. An adequate numerical budget and source-bound implementation are missing.
• Bind one actual caller to the new record length and recompute its full long-record, control and historical-backing bounds. Source placement, ownership and the complete caller invoice remain open.

Related open work

• Prove rounded inverse injectivity from eight owner residues (no κ) #7192 concerns recovery from coordinate residues for a 112-owner rounded inverse. It studies a distinct map and recovery interface; this result supplies a lifted-record bound for Research: Rounded selected MOVE #6996's tensor/monomial provider. No common numerical quantity is compared.

Targeted open searches found no other PR on the retained #6996/#6030 lifted-record allocation. Main README searches included the general tensor/prefix formula and exact width shape; merged searches, recent account contributions, current handoffs and local reservations were checked. Cached coverage included 502 open PRs and 7176 Discussion records with complete reported pagination; sparse local notes, arbitrary diffs and unpublished work remain limitations. No extra scientific computations checked another contributor's result.

The completion refresh read this account's nine other open PRs created since the CLAIM: #7203 through #7208, #7210, #7212 and #7213. Their titles and relevant body text concern distinct feedback, connector, Schur, idle-coalescing, fixed-line crossing, mode-shadow, recovery-cycle and formal-group questions. None targets this lifted-record allocation or computes a conflicting shared quantity. No extra scientific comparison computation was run.

CI notes

CI did not certify this package. At unchanged head 2b882fd2834303655f82d084e25dc551f67e9784, run 43013361819 failed in plan job 130498228533, step Onboarding helper tests. The package replay job was skipped because planning failed. Automated evidence for this package remains local.

I read the checks once and confirmed the job log. Exactly one of 760 tests failed, with 24 skipped: test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record. The AssertionError says that `make frontier7000-verify` was not found in the CI verification document. Direct inspection of canonical main e54523517d0f03e58352e647c403a5af3e525a57 confirms that certificates/selected-result.json names make frontier7000-verify, while docs/ci-verification.md still describes #6030 and make frontier6030-verify. The selected record, CI document and test are unchanged by this PR. This is a base-repository navigation failure.

I also read the failed logs of all six comparison runs below. Each has the same failing test and missing command, the same 760-test total, one failure and 24 skips, in Onboarding helper tests:

• 42905094314
• 42903313790
• 43012497455, PR Prove the unique pair of active feedback operators (no κ) #7203
• 43012524632, PR Prove the exact four-source uniform clean-row tariff (no κ) #7204
• 43013294091, PR Prove the sharp fixed-line Whitehead crossing floor (no κ) #7208
• 43013336222, PR Certify a filled three-dimensional mode shadow with 103,333 points (no κ) #7210

No repair, retrigger commit, push or job rerun was made for this repository-level failure. The local registered and exported evidence described above remains unchanged; no hosted scientific pass is claimed.

Merge Danger

Door: two-way. Blast radius: isolated. This adds one research package and its opt-in replay, without changing a shared implementation or the selected frontier.