Skip to content

Prove local inverse-pair error cancellation and a sharper precision guard - #5322

Merged
Mister-Meeseeks merged 2 commits into
CrocSwap:mainfrom
aliromman:codex/physical-pair-error-transfer
Oct 23, 2026
Merged

Mister-Meeseeks merged 2 commits into
CrocSwap:mainfrom
aliromman:codex/physical-pair-error-transfer

Conversation

@aliromman

@aliromman aliromman commented Oct 23, 2026 •

Copy link
Copy Markdown
Contributor

This enabling proof gives exact error cancellation for the physical inverse-coded pair. The entrance inverse error cancels from the Y output. The actual mode-kernel error shape reduces the sufficient local precision guard by one bit. The complete κ calculation and selected frontier are unchanged.

Proof, exact receipt, source pins, and checker. Base: canonical main ff3cc58e370d0f678e529246f8c73e8094e18fcf, priority revision 7.

Delta X = -D Q C e0
Delta Y = Q^-1(C e1+e2)
For the source mode kernel and e2=0:
P = p + ceil(9f/2) + 5 suffices for inverse errors below 2^-p.

The result holds for every positive tensor width f, with errors measured in maximum real or imaginary component. Other operations and the exit code are exact in the sharper guard. The second inverse input range must include the perturbed input. The proof does not commute C through Q alone.

Use CPython 3.12 and the standard library:

python3.12 -B scripts/research_package.py --package research/physical-pair-error-transfer
python3.12 -B scripts/check_research_commit.py --package research/physical-pair-error-transfer

Both registered modes passed under Python 3.12.13, with warnings as errors and with -O. Expected verifier marker: PASS_PHYSICAL_PAIR_ERROR_TRANSFER. The checks cover the full code identities and row norms, seven signed-normalizer Walsh fibers, 12 actual kernel calls, 12 Gaussian tensor rows, and 100 guard widths. Controls detect omitted X error, reversed thin order and a wrong exit-error site. The committed-byte check, export inventory check and both direct exported replay modes passed. git diff --check passed. Full-history validation was not run in the shallow checkout. No full physical caller, Lean, native/compiler or selected replay ran.

Native and Gaussian rounding, storage, movement, common-coordinate access and the complete error budget still require a funded caller.

This packages the completed Discussion result as the same contribution with a committed proof and replay. @JoyboyBrian’s PR #5069 supplies the pair and PR #5035 supplies the rounded kernel. @dillona’s PR #4933 supplies the actual normalizers. The consumed files are pinned at the base in SOURCES.json. @mdumitrean and the retained native, ownership, precision and compiler authors keep their source credit. New proof and checks: Ali Romman (@aliromman) with substantial OpenAI Codex assistance. Apache-2.0. This is author-checked evidence; independent acceptance is not claimed.

@Mister-Meeseeks
Mister-Meeseeks merged commit 3b785d5 into CrocSwap:main Oct 23, 2026
2 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants