DONE: independent audit of #4462 cross-cell rounding and inverse bounds (#4501)

[mihir-s-05]

DONE / 2026-10-22 02:29 UTC / priority revision 7 / claim released

PR #4501, commit 5fad1d2e9ae4e1ac269a812b024c9c53024603ec, supplies the requested independent check of #4462 at 89548dc186c9c90d459085b6d1be4834977705b9. Both conditional lemmas hold. The audit makes the combined within/across-cell rounding budget explicit, derives the correctly ordered inverse-polynomial residual and section-agreement condition, and gives exact counterexamples showing why both row and column hypotheses matter. Registered replay, optimized replay, committed-byte checks and standalone export replay pass on Windows/Python 3.12. This is a separate implementation with AI assistance, not human or formal-kernel approval. Ideal Gaussian gaps and the production page generator remain unverified. No new kappa; the selected record stays 23/10000.

Evidence. Proof, source pins, exact receipt and verifier. There are 511 exact scalar cases, 24 mixed-cell matrices, 384 sign-vector responses, nonnormal polynomial checks and six failure controls. The predecessor's original README/verifier are preserved and authenticated, but never executed by this checker.

The mixed allowance includes both errors:

2delta + 2(p-1)/(64p^4) < 1/(32p^3),  p >= 2.

A six-by-six bandwidth-one matrix at p=2 satisfies the row condition but has ||H^-1||_2 > 40; its transpose fails under column-only control. This is a generic contract counterexample, not a Gaussian counterexample or an objection to #4462's stated two-sided hypotheses.

Reproduce:

python3.12 -B scripts/research_package.py --package research/delta-cross-cell-independent-audit

Next useful task / handoff. Pin the actual emitted page generator and verify its simultaneous row/column ledger, including within-cell ratios, across-cell rounding and an exact unit diagonal. A first finite block is useful calibration; an all-size conclusion also requires the certified ideal gaps and uniform generator argument. #4481's Schur follow-up is separate. Schur/tensor/core, native/stock/outer assumptions and the full theorem were not checked. Linux and the optional full-history preflight were not run; the selected baseline stopped at a sparse omitted package. No selected cold replay is claimed.

Freshness and attribution. Started and finished against canonical main 2a13eb1827784206202db90e5dc8327cf8a250db, priority revision 7. Final snapshots covered 352 open PRs and 3,378 discussion records; sparse local coverage is explicitly limited. Credit Ryanson Jonathan / pinterbanget, James Reed / jwr404, the #4449 rounding-contract and retained LOG-A/FINE-PRIME/rad20 contributors. Prepared by mihir-s-05 with substantial OpenAI Codex assistance; Apache-2.0. Original claim: this exact audit scope, posted before the checks; now completed and released.

{"schema":"integer-mult-coordination/v1","kind":"DONE","task":"uniform-transfer-audit","scope":"Independent conditional audit of #4462 cross-cell inverse bounds, combined rounding budget and Neumann error/locality, with six failure controls; generator and ideal gaps remain open","base":"2a13eb1827784206202db90e5dc8327cf8a250db","expiry":null,"artifact":"https://github.com/CrocSwap/integer-mult-bounds/pull/4501"}