DONE: exact singular partial Pauli completion lengths (#5097)

[krzysztofwojt]

DONE / 2026-10-23 09:18 UTC / priority revision 7 / claim released

PR #5097, exact head 882cfb2894918ecfd3987fc05d70c91fd4bbd463, publishes the scoped proof and standalone verifier. Singular rank-two partial symplectic contracts have exact transvection minimum three when rank(b)=1, and four when b=0. The same proof gives r+nullity(b) <= ell(h) <= 2r, hence the sharp all-rank zero-form minimum 2r, with axes in the original V.

Registered normal/optimized checks, all 10,112 bounded partial maps, 268 larger fixtures, rejecting controls, source-history/committed-byte checks and Git-free export replays pass. Both hosted CI checks passed at the published head. Evidence is author-checked with AI assistance, not human/formal acceptance. No physical invoice or new kappa. Higher-rank nonzero forms and one fully priced actual caller are the next questions; no follow-up is reserved. Nick Petalas, JoyboyBrian and the retained lineage keep predecessor credit.

Original advance claim, retained for provenance

CLAIM / 2026-10-23 08:58 UTC / priority revision 7

Question: resolve Open next question 1 of Nick Petalas's PR #5085: the exact minimum symplectic-transvection length of an injective partial binary symplectic isometry h:U -> V when D=(h-I)U has dimension two and its induced residual bilinear form is singular. The target is a dimension-uniform criterion and attaining words inside the original V, distinguishing the zero and rank-one forms. This changes the missing ambient-completion problem, not the already classified two-turn cutoff.

Base: fresh canonical main 81e9bd69e4a5b00ba9c713a1620e36d576d5522e; predecessor #5085 at d32b46c02387b3bc9dc0bea344b2c6271b08c5f9, with JoyboyBrian #5051's signed-compatibility setting and the retained native/compiler lineage. Selected conditional kappa remains 60403/20000000.

Method and bounded domain: derive lower bounds from full displacement/residual-form completion, construct short extensions using binary linear algebra, and independently corroborate all restricted symplectic maps through ambient dimension four. Larger explicit fixtures will test any geometric boundary; they will not be represented as an exhaustive proof. Stop or narrow to a precise missing lemma if a uniform argument does not close within two hours. No predecessor census is being offered as a new contribution.

Value and overlap: #5085 explicitly leaves this exact minimum open in its README and #1166 handoff. The repository overlap snapshot at 08:54Z covered all 313 open PRs, 4,215 Discussion records and 6,824 local records without pagination warnings. A live PR/Discussion refresh immediately before this claim found no reservation of the singular rank-two completion question. The recent krzysztofwojt claims on four-event negative association, two-row dirty fanout, three-cycle cuts, intact-region retiming and the fixed seven-call twisted pattern are excluded.

Expected artifact: a focused proof and standalone exact verifier, or a precise scoped counterexample/handoff. Formal transvection count assumes free Pauli sign corrections and is not native Gaussian rank, a physical supplier invoice or a new multiplication exponent. Current evidence is LOCAL-ONLY; no result yet.

Claim expires: 2026-10-23T11:00:00Z.

Prepared by Krzysztof Wojt with substantial OpenAI Codex assistance; Apache-2.0. Nick Petalas, JoyboyBrian, David Ganz / Dugongue, Cao Yifan / intqwq, Cinna Davis, zxv, Jacob Alan Sussman and the retained native/owner/compiler and classical symplectic lineage retain credit.

[krzysztofwojt]

DONE — PR #5097, exact head 882cfb2894918ecfd3987fc05d70c91fd4bbd463.

The missing singular rank-two cases of Nick Petalas's #5085 have exact minima three for rank(b)=1 and four for b=0. The written proof also gives r+nullity(b) <= ell(h) <= 2r for every compatible partial binary symplectic map, hence the sharp all-rank zero-form minimum 2r. Attaining words use the original ambient space and preserve every prescribed fixed spectator.

All 10,112 small partial maps, including all 1,920 singular rank-two cases, agree with an independent literal-matrix Cayley oracle. There are 268 larger fixtures, 6,510 rejected omissions and 12 rejection controls. Normal/optimized registered checks, committed-byte/source-history checks, official export integrity and both Git-free direct modes pass. Hosted planning and package replay also passed at the exact head.

Reproduce with python3.12 -B scripts/research_package.py --package research/singular-rank-two-pauli (standard library; a few seconds). This is an unsigned formal-turn theorem. Higher-rank nonzero-form optima, signed phase/actual caller implementation and complete native/physical costs remain open. No new kappa, selected-frontier change, independent human review or formal proof-kernel acceptance is claimed. The reservation is released.

Krzysztof Wojt with substantial OpenAI Codex assistance, including a Luna supporting census/review; Apache-2.0. Nick Petalas #5085, JoyboyBrian #5051, David Ganz / Dugongue #4841, Cao Yifan / intqwq, Cinna Davis, zxv, Jacob Alan Sussman and the retained native/owner/compiler and classical symplectic lineage retain credit.