Prove exact singular partial Pauli completion lengths

research/singular-rank-two-pauli/PROOF.md

@@ -0,0 +1,153 @@
+# Singular partial Pauli completion: the missing three/four-turn boundary
+
+Krzysztof Wojt, with substantial OpenAI Codex assistance. Apache-2.0.
+
+This is a scoped algebraic proof, not a physical supplier or a new kappa.
+Nick Petalas's [PR #5085](https://github.com/CrocSwap/integer-mult-bounds/pull/5085),
+head `d32b46c02387b3bc9dc0bea344b2c6271b08c5f9`, asks for the exact minimum
+at singular displacement rank two. It already supplies the induced form and
+the exact cutoff through two turns. JoyboyBrian's #5051 supplies the compatible
+partial signed-Pauli setting. The elementary residual-form machinery is
+classical (often called a Wall form); no literature-priority claim is made.
+This proof is self-contained and does not depend on a predecessor executable.
+
+## Statement and model
+
+Let V be any finite-dimensional nondegenerate symplectic space over F2 with
+pairing omega. Let h:U -> V be an injective linear isometry of a subspace U.
+Put d=h+I, D=d(U), r=dim D, and define the residual bilinear form
+
+    b(d(u),d(v)) = omega(u,d(v)).
+
+Let ell(h) be the least number of nonzero-axis transvections
+T_a(v)=v+omega(v,a)a whose product agrees with h on U. All axes lie in the
+original V; no clean ancilla or new dimension is allowed. The action outside
+U is unspecified. In particular, unprescribed spectators are not promised to
+be fixed; a required fixed spectator belongs in U with h(v)=v.
+
+**Theorem.** Every such partial map satisfies
+
+    r + nullity(b) <= ell(h) <= 2r.
+
+If b=0, the bound is sharp: **ell(h)=2r**, for every r, including r=0.
+If r=2 and b has rank one, **ell(h)=3**. Consequently every singular
+rank-two contract has the exact minimum **4-rank(b)**: three or four turns.
+The proof supplies attaining words inside V.
+
+Only the zero-form all-rank family and the singular rank-two family are
+classified exactly here. The general upper bound is not asserted to be
+optimal when b is nonzero. Transvection count is a formal tariff, not native
+Gaussian paid rank, recursive-child rank, physical cost or a supplier invoice.
+
+## The induced form
+
+Write K=ker d. For k in K and u in U, isometry and h(k)=k imply
+omega(k,d(u))=0. Thus K is orthogonal to D and b is well-defined. Expanding
+omega(h(u),h(v))=omega(u,v) gives
+
+    b(x,y)+b(y,x)=omega(x,y) for x,y in D.             (1)
+
+These are the predecessor's induced-form facts, repeated to make the argument
+checkable without importing that package.
+
+## A displacement-plus-nullity lower bound
+
+Take any full symplectic extension S of h, and put W=im(S-I). For every
+v,z in V,
+
+    omega(v,(S-I)z)=omega((S^-1-I)v,z).
+
+Hence W-perp=ker(S-I). The full residual form
+
+    B((S-I)v,w)=omega(v,w),  w in W,
+
+is well-defined. If its left row at (S-I)v is zero, v belongs to W-perp,
+so (S-I)v=0. Therefore B is nonsingular. Since D is contained in W and
+S agrees with h on U, B restricted to D times D is exactly b.
+
+Let R be the left radical of b. Each x in R defines a functional B(x,-)
+on W/D, because B(x,D)=0. The map R -> (W/D)* is injective by
+nonsingularity of B. Thus
+
+    nullity(b)=dim R <= dim W-r.
+
+Each transvection changes the identity by rank one, and
+AB-I=A(B-I)+(A-I) implies rank(S-I) <= the number of turns in any word
+for S. Combining the two inequalities proves ell(h)>=r+nullity(b).
+This lower bound permits any completion on unspecified coordinates.
+
+## Completing in at most two turns per displaced dimension
+
+The following reduction is uniform in dim V and preserves the whole currently
+fixed subspace, not merely a chosen list of previously treated vectors.
+
+If r>0 choose u in U outside K, and let p=h(u)+u, so p is nonzero and
+orthogonal to K. If omega(u,p)=1, T_p fixes K and exchanges u and h(u).
+
+Otherwise choose a in V solving
+
+    omega(k,a)=0 for every k in K,
+    omega(u,a)=1,       omega(p,a)=0.                 (2)
+
+These equations are consistent. Indeed u is not in K+<p>: membership in K
+contradicts its choice, while u=k+p would give h(u)=k=h(k), contradicting
+injectivity. Therefore the functional zero on K+<p> and one on u is
+well-defined, extends to V, and is represented by a through nondegeneracy.
+Also a and a+p are nonzero, since both have pairing one with u. They are
+orthogonal to K and to each other. Their commuting turns give
+
+    (T_(a+p) T_a)(u)=u+p=h(u).
+
+The product is an involution, so it also sends h(u) to u. Let F be this
+two-turn product, or the preceding single turn. Then h'=F h is again an
+injective partial isometry and fixes K+<u>. Its displacement rank is at most
+r-1. Repeat until it is the identity on U. There are at most r reductions,
+each with at most two turns. Reversing the collected correction word gives
+a full symplectic extension of h with at most 2r turns. Every step solves
+linear equations in the original V. No auxiliary dimension is introduced.
+
+When b=0 the lower bound is 2r, so this construction necessarily returns
+exactly 2r turns. This proves the entire zero-form family, including the
+four-turn rank-two case.
+
+## Rank-one singular form at displacement rank two
+
+Suppose dim D=2 and rank b=1. There is a in D with b(a,a)=1. Otherwise
+b would be alternating, hence in any two-dimensional basis would have
+matrix [[0,c],[c,0]], of rank zero or two, a contradiction.
+
+Apply T_a on the left and put h'=T_a h. By (1), its displacement is
+
+    d'(u) = d(u) + b(a,d(u)) a.                       (3)
+
+The map P:x -> x+b(a,x)a has kernel <a>, since b(a,a)=1. Its image is
+the line L=ker b(a,-), so d'(U)=L and has rank one. Choose its nonzero
+c; in basis (a,c) the form has matrix
+
+    [1 0]
+    [s t].
+
+Its rank is one, so t=0. For u_c with d(u_c)=c, formula (3) gives
+d'(u_c)=c, and the new residual form has value
+b'(c,c)=omega(u_c,c)=b(c,c)=0. Thus h' belongs to the rank-one zero-form
+family and has a two-turn completion. Appending T_a gives three turns for
+h. The lower bound r+nullity(b)=2+1=3 proves optimality.
+
+## Signed contracts, evidence and remaining boundary
+
+For compatible signed Hermitian Pauli constraints, each transvection has a
+literal Clifford lift. The sign discrepancies on independent prescribed
+generators define a binary functional on h(U); a Pauli conjugation implements
+it. Under #5085's tariff of free arbitrary Pauli corrections, this does not
+change the minimum. Compatibility of dependent central phase relations is a
+premise, and equality to an absolute-phase target still needs an anchor.
+These are cited predecessor implications; this contribution verifies unsigned
+labels, not a new literal Gaussian matrix or signed-phase implementation.
+
+The standalone verifier compares against complete symplectic-matrix Cayley
+distances in dimensions two and four. Larger zero-form and rank-one-form
+fixtures test the constructive algorithm and its fixed spectators; they are
+not exhaustive. The finite checks corroborate this written all-dimensional
+proof and do not replace it. No independent human or proof-kernel review,
+native/physical cost, profitable caller, arbitrary dirty-owner schedule,
+precision, stock, compiler/outer admission or new kappa is claimed.

research/singular-rank-two-pauli/README.md

@@ -0,0 +1,153 @@
+# Exact singular partial Pauli completion lengths
+
+**Scoped algebraic proof with exact finite corroboration; no new kappa.**
+This answers Open next question 1 of Nick Petalas's
+[PR #5085](https://github.com/CrocSwap/integer-mult-bounds/pull/5085), head
+`d32b46c02387b3bc9dc0bea344b2c6271b08c5f9`:
+
+| Rank-two displacement, singular residual form b | Exact transvection minimum |
+|---|---:|
+| rank(b)=1 | 3 |
+| b=0 | 4 |
+
+The predecessor only gave a lower bound of three for these cases. The new
+[proof](PROOF.md) closes the ambient-completion gap and constructs attaining
+words in the original binary symplectic space. The same argument proves, for
+every injective partial isometry with displacement rank r,
+
+    r + nullity(b) <= ell(h) <= 2r,
+
+and therefore **ell(h)=2r whenever b=0**, at every rank. This is a symbolic
+extension, not a larger parameter census. The induced form is
+b((h-I)u,(h-I)v)=omega(u,(h-I)v). Its nullity measures necessary extra
+displacement in every full completion. A constructive reduction preserves
+the current fixed subspace and fixes one more source direction per step.
+
+## Scope, examples and value
+
+The contract specifies h only on U. Any spectator required to remain fixed
+must be included in U and mapped to itself. There is no guarantee of identity
+on unspecified coordinates, and no clean ancilla or ambient enlargement.
+With free Pauli sign corrections the unsigned length has the same meaning as
+in #5085; dependent signed compatibility and absolute-phase anchors remain
+separate obligations. This implementation returns unsigned labels only.
+
+In bit order (x0,x1,z0,z1), both examples have source basis (1,2):
+
+| Target basis | rank(b) | Chronological attaining axes |
+|---|---:|---|
+| (2,3) | 0 | (9,8,15,12) |
+| (4,6) | 1 | (9,8,5) |
+
+[algebra.py](algebra.py) implements the constructive rank reduction and exact
+classification; [verify.py](verify.py) uses separately implemented literal
+row matrices and complete Cayley distances. No predecessor executable or
+certificate is imported or rerun. The transvection tariff is not native
+Gaussian rank, recursive-child rank, physical execution cost or a supplier
+invoice. This is a boundary lemma for partial native-chart contracts, not a
+profitable actual caller or a change to the selected frontier.
+
+The task uses the live #1166 handoff in preference to a random card, under
+priority revision 7. It changes `formal-interface-lemma` to a written proof,
+without claiming Lean formalization or selected-caller admission. The exact
+base is `81e9bd69e4a5b00ba9c713a1620e36d576d5522e`.
+[Discussion #5094](https://github.com/CrocSwap/integer-mult-bounds/discussions/5094)
+is the canonical claim. The 08:54Z overlap snapshot covered 313 open PRs,
+4,215 Discussion records and 6,824 local records; the direct pre-claim refresh
+found no claim on the singular completion gap. The broader zero-form conclusion
+was also searched against the residual-form corpus before publication.
+
+## Exact evidence
+
+The registered checker enumerates all 6 and 720 symplectic matrices in ambient
+dimensions two and four independently of its Cayley BFS, then all 5 and 67
+source subspaces. It checks all **10,112 distinct partial maps** against the
+general lower bound and constructive upper bound. The exactly classified
+subset includes all **1,920 singular rank-two maps**: 1,890 with rank-one b
+and 30 with zero b. It also covers 360 rank-one zero-form maps and 72 identity
+restrictions. Every returned exact word is checked as a full literal matrix;
+all 6,510 single-turn omissions fail its required endpoint.
+
+Another **268 fixed fixtures** through ambient dimension 18 cover zero-form
+maps with disjoint source/displacement, fixed nondegenerate spectators,
+nilpotent displacement and order-three action on isotropic subspaces, plus
+rank-one residual forms. Four explicit symplectic conjugations per underlying
+fixture test different coordinates. Twelve invalid/out-of-scope input and
+zero-axis controls reject. These fixtures are not exhaustive.
+
+The generated [RESULT.json](RESULT.json) binds the counts to SHA256 hashes of
+the seven package sources. Ordinary replay recomputes and compares that report;
+it does not update it. Normal and optimized Python use explicit exceptions,
+so correctness checks do not depend on assertions. Source hashes authenticate
+the stated bytes, not mathematical correctness. A separate AI-assisted
+column-matrix census agreed on the 4D singular counts during development; it
+is local-only corroboration, not an additional published or human review.
+
+## Reproduce
+
+CPython 3.12, standard library only. From the repository root:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/singular-rank-two-pauli
+```
+
+The registered normal and optimized commands each take about one second on
+the development Mac (Python 3.12.12). Standalone, including from a Git-free
+package export:
+
+```sh
+python3.12 -W error -B research/singular-rank-two-pauli/verify.py
+python3.12 -O -W error -B research/singular-rank-two-pauli/verify.py
+```
+
+After an intentional source change, `verify.py --write-report` regenerates the
+receipt only after recomputing every check. Review the changed report before
+committing it. The generic runner needs Git history for scaffold provenance;
+the standalone mathematical checker has no repository or external inputs.
+
+## Limits
+
+The written theorem is uniform in finite dimension. The API deliberately caps
+the ambient space at 18 binary dimensions, accepts only an independent source
+basis, and requires injectivity and preserved pairings. The exact API rejects
+nonzero forms outside the singular rank-two case. `reduction_word` returns a
+valid upper-bound word for other compatible maps, without claiming minimality.
+Linear algebra is polynomial in the API dimension; exhaustive matrix and
+subspace enumeration is restricted to dimensions two and four. Python uses
+dynamic allocation; this is an offline research implementation.
+
+## Open next questions
+
+1. **What is the exact length for higher-rank nonzero residual forms?** The
+   new interval separates residual nullity from the remaining obstruction.
+   First test whether a diagonal pivot can always be chosen to avoid an
+   alternating residual obstruction. A general normal-form/attainment argument
+   is missing; the lower endpoint must not be assumed attainable (the known
+   nonsingular alternating rank-two form already needs three rather than two).
+2. **Can a specified native caller exploit one of these short completions?**
+   Fix its partial signed constraints, required fixed spectator subspace and
+   absolute phase, then price every turn and correction in its actual native
+   alphabet. No such caller or physical/recursive invoice is supplied here.
+
+Native Gaussian costs, physical movement, arbitrary dirty-owner restoration,
+precision, stock, compiler and outer admission remain open. Lean, Docker and
+the selected scientific cold replay were not run. No independent human or
+formal proof-kernel review is claimed. The selected conditional kappa remains
+`60403/20000000`.
+
+## Credit and source boundary
+
+Prepared by **Krzysztof Wojt with substantial OpenAI Codex assistance**, including
+a Luna supporting census and read-only review. New work is Apache-2.0.
+Nick Petalas's #5085 supplies the low-length cutoff, residual-form problem and
+explicit open question. JoyboyBrian's #5051 supplies signed partial-contract
+compatibility. David Ganz / Dugongue's #4841 supplies native compiler context;
+Cao Yifan / intqwq, Cinna Davis, zxv, Jacob Alan Sussman and the retained
+native/owner/compiler lineage keep their predecessor credit. Classical binary
+symplectic transvections and Wall forms are not claimed as new concepts.
+
+[SOURCES.json](SOURCES.json) pins base provenance and separately records exact
+bibliographic predecessor heads and document hashes. The latter are credited
+problem statements, not live inputs, vendored sources, audited predecessor
+results or unmerged Git dependencies. The complete proof and implementation
+needed for this package are local. No frozen predecessor files are changed.

research/singular-rank-two-pauli/RESULT.json

@@ -0,0 +1,34 @@
+{
+  "counts": {
+    "dimension_2": {
+      "all_restrictions": 16,
+      "exact_r0_b0": 5
+    },
+    "dimension_4": {
+      "all_restrictions": 10096,
+      "exact_r0_b0": 67,
+      "exact_r1_b0": 360,
+      "exact_r2_b0": 30,
+      "exact_r2_b1": 1890,
+      "rejected_omissions": 6510
+    },
+    "larger_fixtures": {
+      "rank_one_form": 28,
+      "zero_form_disjoint_source_and_displacement": 80,
+      "zero_form_nilpotent_with_fixed_spectators": 80,
+      "zero_form_order_three": 80
+    },
+    "rejection_controls": 12
+  },
+  "scope": "Unsigned finite corroboration and witnesses; uniform theorem in PROOF.md. No physical cost or new kappa.",
+  "source_sha256": {
+    "PROOF.md": "bc43da28cf432e370532cdeb1622ce8efb175d497fe83b632d8560fd27c20a5b",
+    "README.md": "2be2b460c1ce24261e3f887cb583163e86233217a6ccaa61c9a6a8b8d1ec7cb0",
+    "SOURCES.json": "d97ae2f0b5a440b9d076ac4599718eb10a76a216ce8d32bcb76abc2a70f05ae2",
+    "TASK.json": "a3e877f265643fb47fd1e5fabbd61f965c6e8ec0e4cadf6a012c1f902b65b637",
+    "VERIFY.json": "ead160df0e0b9862fc1184096589a1ac855dc2c23bc26cd4e4dfccac81d9406c",
+    "algebra.py": "13cf6e512d93e7f9a75d63e8bfd615c6235931e0c0aba3a59582256c75a74427",
+    "verify.py": "0788354998ae813531524c1095d603e040417677e1eb62a282a54875c1aa3ef9"
+  },
+  "status": "PASS_SINGULAR_PARTIAL_PAULI_COMPLETION"
+}

research/singular-rank-two-pauli/SOURCES.json

@@ -0,0 +1,44 @@
+{
+  "schema_version": 1,
+  "base_commit": "81e9bd69e4a5b00ba9c713a1620e36d576d5522e",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395",
+      "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    }
+  ],
+  "bibliographic_predecessors": [
+    {
+      "pr": 5085,
+      "author": "Nick Petalas",
+      "head": "d32b46c02387b3bc9dc0bea344b2c6271b08c5f9",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5085",
+      "usage": "Cited problem, cutoff and signed-lift setting only; not a live input or audited executable.",
+      "documents": [
+        {
+          "path": "research/partial-pauli-two-transvection/PROOF.md",
+          "sha256": "667e87bb24bfc34b1b488bf7dae87cd870b02156b13214bbcfce5d8c687fe9f6"
+        },
+        {
+          "path": "research/partial-pauli-two-transvection/README.md",
+          "sha256": "06b3084c46bea30e06519385258a355c4b6d9b622281e1fda9a5b794b233a2c5"
+        }
+      ]
+    },
+    {
+      "pr": 5051,
+      "author": "JoyboyBrian",
+      "head": "0960807a68ff46acbe6510c8867912ef2324ee71",
+      "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5051",
+      "usage": "Cited compatible signed-contract setting; not a live input or audited executable."
+    }
+  ]
+}