[petalas]

Summary

Scoped written proof with exact finite corroboration. Every Gaussian-rational matrix E of rank r admits a factorization with at most 2r terms and exact coefficient norm bounds:

E = sum_j g_j a_j,       ||g_j||_2 <= 1,
||a_j||_2 <= ||E||_2,    GG* = P_col(E),    A = G*E.

Jose Manuel / jmbarrancoml's merged #4198 supplies the orthogonal-residual and compensated Stein interface, with r terms and row norm below 2||E||. Nick Petalas's merged #6228 already approaches factor one with r terms. The new step splits each residual projector using two Gaussian-rational squared norms and attains exact factor one by allowing extra terms. The standard coordinate construction uses m terms; the new bound is independent of the ambient row dimension m. Lagrange's four-square theorem is a classical input.

This contribution was produced by Nick Petalas. Credit Jose Manuel, Vlado Vojdanovski, Cinna Davis and the retained Gaussian/compiler/phase lineage. No predecessor scientific result is audited or replayed. No new kappa or selected-frontier change is claimed.

Evidence

• Before: the credited rank-many rational normalization gives a strict factor above one. After: an exact rational Parseval splitting gives factor one with at most twice as many terms.
• 414 matrix fixtures have total rank 698 and 901 emitted terms; 123 fixtures use extra terms. Independent row elimination checks rank. Every matrix entry, complete Parseval projector and exact Hermitian PSD inequality EE-a_ja_j is checked.
• 2,048 positive integer square decompositions and seventeen rejecting controls pass. For E=(1,1,1)^T, the two emitted terms have squared column norms 1/3 and 2/3, and squared row norms 1 and 2, below ||E|| squared = 3.
• CPython 3.12.15 on macOS arm64 passes both registered commands with identical source-hash-bound receipts. The direct normal and optimized commands take 0.28 and 0.27 seconds locally. These timings document replay budget, not performance gains.
• Seven-file committed-byte/source-history checks, official export integrity and optimized read-only Git-free replay pass. All eight exported files remain unchanged.

From the repository root:

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

Any CPython 3.12 path can replace the local interpreter. Expected markers are PASS_EXACT_UNIT_STEIN_SPLITTING, PASS_REGISTERED_RESEARCH_PACKAGE and PASS_RESEARCH_COMMIT_BYTES. Standard library only. Optional --receipt /absolute/new/path.json writes a generated file-bound receipt without overwriting an existing file.

Limitations

The arbitrary-dimensional claim is the written proof. The executable enforces at most eight rows and columns, input component height at most 256, and primitive residual squared norm at most 65,536. Its exhaustive four-square search is not a polynomial bit-time algorithm. The 2r count is not claimed globally optimal.

Extra compensated macros can outweigh the smaller coefficients. No rounded child, physical coefficient preparation/delivery, complete dirty-state rounding ledger, native/compiler admission, stock/tape invoice, full caller or outer multiplication theorem is supplied. No precision, runtime or recursive-moment gain is inferred. Independent human and formal proof-kernel review are unclaimed; no Lean, Docker, historical suite or selected cold replay ran. All five framework assumptions remain.

Open next questions

• Can rational Parseval construction use fewer than 2r terms? Start with a rank-two rational Hermitian form embedded into three standard coordinates. Such an embedding and its preparation costs are not supplied here.
• Does one actual rounded child benefit after every extra macro is charged? Start with a complete emitted tuple and its coefficient preparation, delivery, rounding and caller invoice. AAAmirinu's merged Bind a near-unit Stein row to the rounded child at unchanged precision #6239 already shows that smaller row norms alone need not reduce child precision.

Related open work

No other open PR studying rational Stein normalization or this Parseval term-count contract was found in the fully paginated cached open-PR corpus and the final live Stein search. #4198, #6228 and #6239 are merged predecessors/background, with the different contracts described above. No extra computation checked their results.

The completion check read this account's nine other open PRs created since the advance CLAIM. None studies the same Stein factorization or computes a competing coefficient bound. Adjacent #7267 changes forward accuracy allocation in a normalized Gaussian convolution channel; it does not construct or price these Stein coefficients. No additional numerical comparison was run.

CI notes

CI certified nothing for this package at unchanged head d9219ca07e69ca08c6cc7ec9dc805955fe87d857. In run 43029399850, plan job 130552253363, Onboarding helper tests ran 760 tests with exactly one failure and 24 skips. The exact failing test was test_research_current_status.CurrentCiNavigationTests.test_current_ci_section_matches_selected_record. Its assertion failed because the literal `make frontier7000-verify` was absent from docs/ci-verification.md. The package replay job was skipped because plan failed.

This is inherited from canonical main e54523517d0f03e58352e647c403a5af3e525a57: certificates/selected-result.json names make frontier7000-verify, while docs/ci-verification.md still describes #6030 and make frontier6030-verify. The exact main files and failing test were inspected and are byte-identical in this PR. The PR changes only its seven package files.

The failed logs were also inspected for run 42903313790 and run 43029125610. Each reports the same sole failing test and missing make frontier7000-verify assertion, with 760 tests, one failure and 24 skips. No claim is made about other runs not inspected here.

Both registered scientific commands, direct normal/optimized replay, committed-byte/source-history checks and export checks passed locally at this exact head as recorded above. Hosted package replay remains unrun. No fix, retrigger commit or job rerun was made.

Merge Danger

Door: two-way. Blast radius: isolated. Seven new files in one opt-in package; no shared implementation, frozen source or selected record changes.