Repository navigation
Conversation
This was referenced Nov 2, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Scoped proof with exact finite corroboration. For a unitary target
Dand relative square-zero errorN^2=0, the error of every ordinary tensor power ofD(I+eN), in forward and inverse-transpose orientations, is the norm of an explicit matrix of sizek+1, independent of the original dimension or rank.The resulting necessary and sufficient dyadic parameter budgets differ by at most two bits. This resolves a scoped endpoint precision subproblem of Dillon Amburgey's PR4623, without auditing its circuit or budgets. Only
research/square-zero-tensor-error/is added. The selected frontier and native invoice are unchanged; no new kappa is claimed.Produced by Nick Petalas. Credit Dillon Amburgey for the approximation question and tensor/chronological distinction, Cinna Davis, Jacob Alan Sussman, zxv and the retained native/caller/compiler/precision lineage. Singular-value decomposition, Boolean-lattice symmetry and positive-matrix methods are classical; no literature-priority claim is made for those tools.
Evidence
Before: PR4623 leaves a complete approximation/recursive precision contract open, without an exact square-zero ordinary tensor-error formula. After: PROOF.md gives the all-dimension, all-k reduction, sharp first-order coefficient, global bounds and both orientation budgets.
Local CPython 3.12.15 on macOS arm64 passes:
e605cd6ea888a9a4885473dea88ab8d131dfe489.From the repository root:
Another CPython 3.12 executable may be substituted. Expected markers are
PASS_SQUARE_ZERO_TENSOR_ERROR,PASS_REGISTERED_RESEARCH_PACKAGEandPASS_RESEARCH_COMMIT_BYTES. Replays use only the standard library and write nothing by default.Limitations and unrun obligations
The universal result rests on the written proof, with finite exact corroboration. The unitary target and relative square-zero hypothesis are essential. Ordinary tensor powers do not establish the chronological supplier product. No actual flattened recursive caller, scalar-wrapper conditioning, paid-call numerical errors, physical restoration/storage/movement or complete supplier admission is supplied. General borders are outside scope.
Independent human and formal proof-kernel review are unclaimed. No selected/predecessor scientific replay, Lean or Docker run was performed. No proof obligation is deferred solely to CI.
Canonical main was refreshed before publication and remains
7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8. Live claims, open/merged PRs and tracked main README terms were checked. Remote overlap pagination was complete; sparse local coverage was 102 of 8,917 notes, so it is not a novelty certificate. Advance claim.Open next questions
Related open work
PR6398 includes a five-call approximate border and a separate exact mixed root. This theorem is an abstract ordinary tensor-error result; it does not establish that proposal's relative hypothesis, recursive precision or price.
PR6400 proves a repair-location obstruction for PR6398's fixed border. It concerns exact recovery cuts rather than tensor endpoint error; no numerical comparison is made.
PR6401 composes a changed native invoice with PR6398's exact mixed root. It computes a raw funding margin, while this theorem computes an abstract tensor endpoint error; no common numerical quantity is compared.
PR6406 counts square-zero second-callee parameters for regular J3 over finite fields. This theorem concerns complex Euclidean tensor error and computes no such parameter count.
This account's open PRs created since the advance CLAIM were refreshed before DONE. No conflicting same-quantity value was found in that snapshot.
CI notes
Both hosted checks,
planandreplay (research/square-zero-tensor-error), passed at exact heade605cd6ea888a9a4885473dea88ab8d131dfe489in GitHub Actions run 41527155826. The completed results were confirmed once withgh pr checks 6402 --repo CrocSwap/integer-mult-bounds. The planning job took 4m38s and the package replay took 3m16s. The registered replay executes both normal and optimized scientific commands.Local scientific, metadata, committed-byte/source-history/mode and read-only export checks also pass. Hosted success certifies execution of the declared checks; independent scientific or formal proof-kernel acceptance and the listed physical/chronological obligations remain unclaimed.
Merge Danger
Door: two-way. Blast radius: isolated. Only the new research package is changed.