DONE: downward rounding of across-cell Gaussian coefficients

[mihir-s-05]

DONE / 2026-10-21 21:18 UTC / priority revision 7

The scoped coefficient construction is complete in PR #4449, commit 1fb77b377f570ca84a89a465b2ee4ce8674b7159. The actual across-cell square gap is exactly pi*j/k with j>=0, so the retained negative-exponential contract and two-ulp subtraction/clipping yield 0 <= H <= n and n-H < 4*2^-P. This is a written caller-bound lemma with separately written exact controls, not independent human/formal acceptance. No new kappa.

CPython 3.12.0 ordinary and optimized registered replays pass: 384 coefficient cases, 1,624 phase identities, 2,019 oracle-boundary cases and 10 controls. Committed bytes, the official export and both Git-free replays pass. Five additional code mutations and exported source/receipt corruption reject. All evidence is now public. Claim released.

Next useful task: pin one actual online coupling-page generator and check its rounding mode/error budget. Later nearest rounding can undo domination. The existing Schur/native/outer obligations and #4442's halo/minimality claims remain outside this result.

Proof, exact source pins, reproduction and credit.

Original claim and source history

This took James Reed's PR #4442 open question at d079c2b058ebd3d7a9ff424113b095bf61175427, linked from the #1166 handoff. Scientific base and refreshed canonical main: 2a13eb1827784206202db90e5dc8327cf8a250db. The initial claim concerned the original across-cell exponent, the two-ulp repair, underflow, period/cell cuts and wrong-kernel controls; its original expiry was 2026-10-21 23:12 UTC. Work stopped at that boundary.

The repair itself is predecessor work. Credit remains with the RaD phase-cell producer/reviewer, James Reed, Vlado Vojdanovski/PR1673, Chafik Boukhalfa, Cinna Davis, Ryanson Jonathan, Harvey and van der Hoeven and the complete lineage in the README. Mason Hale and Dugongue's prior directed-rounding/interval work is acknowledged. Prepared for mihir-s-05 with substantial OpenAI Codex assistance; no subagents. Apache-2.0.

The pre-submission overlap refresh at 21:15-21:17 UTC paginated 303 open PRs, 3,294 Discussion records and 3,787 closed PRs, and covered all 5,731 tracked top-level note paths at the base. No exhaustive diff or novelty claim follows. Hosted CI is separate from the local evidence.

{"schema":"integer-mult-coordination/v1","kind":"DONE","task":"uniform-transfer-audit","scope":"PR4442 open question: exact across-cell Gaussian exponent and two-ulp downward repair","base":"2a13eb1827784206202db90e5dc8327cf8a250db","expiry":null,"artifact":"https://github.com/CrocSwap/integer-mult-bounds/pull/4449"}