[petalas]

Summary

Scoped written mathematical proof with finite corroboration. Under the unchanged physical Gaussian production guards, and conditional on the cited kernel and coefficient estimates, the original-coordinate rounded matrix H and every nonempty principal restriction satisfy

- Historical inverse infinity-norm bound: 8p
+ New inverse infinity-norm bound: 2 + 2p/u²
+ New rounded row gap: greater than u²/(2(p+u²))

The new step retains u*theta > u²/(4p) from u*d <= p and theta > 1/(4d). On the published p=16384, u=32 metadata example, the new upper bound is 34, instead of 131072. These are analytic bounds, not measured norms. This answers the row-gap part of PR6099's Open next questions. No new κ or selected-frontier change.

The bilateral majorant is cited from PR1673. PR6099's retained-band perturbation theorem, at 38ce77a4925c18eb66f94634b1b11a1242af8a87, is a mathematical premise conditional on PR6085. Their re-verification is not the deliverable. The six new files are confined to research/production-gaussian-rowgap/.

Evidence

• Before: the physical producer states an 8p inverse bound, while PR6099 leaves uniform row dominance open under its coefficient theorem.
• After: PROOF.md proves the stronger universal implication. Each registered check passes on 139850 exact rational parameter fixtures, 2976 geometry pairs, 1024 rounding-budget fixtures, five rejected parameter cases and one removed-similarity counterexample. The parameter fixtures are a relaxation, not complete production plans.
• CPython 3.12, standard library. Registered normal and optimized checks took 0.570s and 0.583s locally, each below its 60s timeout. The direct warnings-as-errors/development-mode check also passed.
• Package metadata, exact committed bytes, source ancestry and executable modes passed. The official export and input-coverage check passed for 11 package/input files. Both normal and optimized direct checks passed in a read-only Git-free export with all 12 exported files unchanged, including the generated export manifest.

Exact reproduction from the repository root:

/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/production-gaussian-rowgap
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/production-gaussian-rowgap --check-source-history --check-modes
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -B research/production-gaussian-rowgap/verify.py
/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -B research/production-gaussian-rowgap/verify.py

Use another CPython 3.12 executable in other environments. The verifier prints PASS_PRODUCTION_GAUSSIAN_ROWGAP; finite fixtures corroborate the written proof rather than establishing its universal quantifiers.

Limitations

Conditional on the existing bilateral row majorant and PR6099/PR6085 coefficient estimates. No independent human or formal proof-kernel acceptance is claimed. The infinite-periodized comparison and tail, column/spectral norms, LU growth, full production pages, physical setup/tape cost, tensor/CRT assembly and the complete multiplier remain unproved here. No predecessor scientific replay, selected cold replay, Lean or Docker run was performed. The five selected framework assumptions remain.

Open next questions

• Reprice one actual caller's inverse-error term using the retained u² factor, preserving its separate column, Schur and tape obligations.
• Prove the separate retained-band-to-infinite-periodized comparison and tail left in PR6099, starting with the exact omitted offsets across the physical seam.

Related open work

• Prove production Gaussian positivity and retained matrix perturbation #6099 supplies the conditional retained-band perturbation theorem and asks the row-gap question answered here; its infinite-tail question remains open.

• Audit uniform directed bounds for actual encoded Gaussian coefficients #6085 supplies the scalar enclosure theorem cited by Prove production Gaussian positivity and retained matrix perturbation #6099; this contribution adds a matrix-conditioning consequence without replaying that scalar result.

• Prove the sharp Gaussian concentration threshold (no new κ) #6131 studies the same ideal nearest-grid Gaussian kernel while varying concentration, and proves a sharp dominance/failure threshold. This contribution instead retains the unchanged production guard and bounds the rounded inverse; no common numerical inverse value is compared.

Credit Jose Manuel / jmbarrancoml for PR3851, JoyboyBrian for PR6099/PR6085, Vlado Vojdanovski and the credited PR1673 phase-cell contributors, RaD/hipotures, Chafik Boukhalfa and the retained source-specific lineage. This contribution was produced by Nick Petalas.

CI notes

CI is uncertified for commit 5e09c60005dd6ae454eef8271c0c2d2dba62c12e. In run 40692647641, plan failed during Onboarding helper tests and replay (research/production-gaussian-rowgap) was skipped. The package replay did not run in CI.

The exact failures are inherited from canonical main 721c03822c421b7f7fcbb2598993b947c4d88419, the PR6030 κ-admission commit pushed with [skip ci]. Its selected-record/documentation mismatch is unrelated to this isolated package:

• test_research_current_status.CurrentStatusTests.test_current_section_matches_selected_record expects the exact marker **0.003125804** in docs/research/current-status.md. The document instead bolds 0.003125804 = 781451/250000000 together, so that marker is absent.
• test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record expects make frontier6030-verify in docs/ci.md, which still describes Raise conditional kappa to 0.00310045 with independent helper splits #5599 and make frontier5599-verify.

The failed-job log reports 678 onboarding tests, two failures and 23 skips. PR6120's run 40691776027 fails the same two tests, confirmed from its failed-job log.

All package checks reported above passed locally; none was certified by this hosted run. The PR needs a maintainer re-run after main's documentation is fixed. No branch push, main-documentation edit or CI re-run was performed for this blocker.

Merge Danger

Door: two-way. The package is isolated and can be reverted.

Blast Radius: research. No shared implementation, frozen evidence or selected record changes.