From 882cfb2894918ecfd3987fc05d70c91fd4bbd463 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Krzysztof=20W=C3=B3jt?=
<97155365+krzysztofwojt@users.noreply.github.com>
Date: Fri, 23 Oct 2026 11:09:05 +0200
Subject: [PATCH] Prove exact singular partial Pauli completion lengths
---
research/singular-rank-two-pauli/PROOF.md | 153 ++++++++++
research/singular-rank-two-pauli/README.md | 153 ++++++++++
research/singular-rank-two-pauli/RESULT.json | 34 +++
research/singular-rank-two-pauli/SOURCES.json | 44 +++
research/singular-rank-two-pauli/TASK.json | 102 +++++++
research/singular-rank-two-pauli/VERIFY.json | 32 +++
research/singular-rank-two-pauli/algebra.py | 182 ++++++++++++
research/singular-rank-two-pauli/verify.py | 265 ++++++++++++++++++
8 files changed, 965 insertions(+)
create mode 100644 research/singular-rank-two-pauli/PROOF.md
create mode 100644 research/singular-rank-two-pauli/README.md
create mode 100644 research/singular-rank-two-pauli/RESULT.json
create mode 100644 research/singular-rank-two-pauli/SOURCES.json
create mode 100644 research/singular-rank-two-pauli/TASK.json
create mode 100644 research/singular-rank-two-pauli/VERIFY.json
create mode 100644 research/singular-rank-two-pauli/algebra.py
create mode 100644 research/singular-rank-two-pauli/verify.py
diff --git a/research/singular-rank-two-pauli/PROOF.md b/research/singular-rank-two-pauli/PROOF.md
new file mode 100644
index 0000000000..c8ffbe676f
--- /dev/null
+++ b/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+: 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+
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+. 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 , 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.
diff --git a/research/singular-rank-two-pauli/README.md b/research/singular-rank-two-pauli/README.md
new file mode 100644
index 0000000000..340e9004be
--- /dev/null
+++ b/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.
diff --git a/research/singular-rank-two-pauli/RESULT.json b/research/singular-rank-two-pauli/RESULT.json
new file mode 100644
index 0000000000..deb5c342c2
--- /dev/null
+++ b/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"
+}
diff --git a/research/singular-rank-two-pauli/SOURCES.json b/research/singular-rank-two-pauli/SOURCES.json
new file mode 100644
index 0000000000..0b163b390d
--- /dev/null
+++ b/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."
+ }
+ ]
+}
diff --git a/research/singular-rank-two-pauli/TASK.json b/research/singular-rank-two-pauli/TASK.json
new file mode 100644
index 0000000000..53735c04b7
--- /dev/null
+++ b/research/singular-rank-two-pauli/TASK.json
@@ -0,0 +1,102 @@
+{
+ "schema_version": 1,
+ "task_id": "formal-interface-lemma",
+ "priority_revision": 7,
+ "base_commit": "81e9bd69e4a5b00ba9c713a1620e36d576d5522e",
+ "original_card": {
+ "id": "formal-interface-lemma",
+ "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+ "starting_points": [
+ "docs/research/research-family-status.md",
+ "certificates/selected-result.json",
+ "research/gate-operand-parity-lean/README.md",
+ "research/staged544-certified-endpoint/README.md",
+ "research/unconditional-batched-crt/README.md"
+ ],
+ "methods": [
+ "Formalize a missing boundary lemma identified by the selected review.",
+ "Audit a formal theorem-to-certificate binding independently."
+ ],
+ "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+ "first_step": {
+ "command": [
+ "python3",
+ "-B",
+ "scripts/research_baseline.py"
+ ],
+ "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+ "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.",
+ "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+ },
+ "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+ "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+ "allowed_variations": [
+ "Narrow to one formal lemma or one theorem-to-certificate binding."
+ ],
+ "scope_change_triggers": [
+ "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+ ],
+ "overlap_terms": [
+ "hyperplane end",
+ "formal interface",
+ "Lean binding",
+ "3807",
+ "3857",
+ "4100",
+ "gate-operand-parity-lean",
+ "staged544-certified-endpoint",
+ "unconditional-batched-crt"
+ ],
+ "existing_checks": [
+ {
+ "scope": "PR #3807: scoped gate-operand parity formalization.",
+ "evidence": "research/gate-operand-parity-lean/README.md",
+ "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+ "status": "author-checked",
+ "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+ "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+ },
+ {
+ "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+ "evidence": "research/staged544-certified-endpoint/README.md",
+ "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+ "status": "author-checked",
+ "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+ "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+ },
+ {
+ "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+ "evidence": "research/unconditional-batched-crt/README.md",
+ "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+ "status": "author-checked",
+ "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+ "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+ }
+ ]
+ },
+ "scope_status": "changed",
+ "actual_scope": "Dimension-uniform exact singular rank-two partial symplectic completion lengths (3 or 4), with r+nullity(b) lower bound, 2r upper bound and sharp all-rank zero-form corollary.",
+ "scope_change_reason": "Take PR5085 Open next question 1 from handoffs #1166. This is a written algebraic interface proof with exact finite corroboration, not a Lean formalization or a selected-caller proof. The same completion argument yields the general zero-form corollary without an expanded search.",
+ "bottleneck_link": "Resolve an explicit missing partial native-chart completion tariff. Physical Gaussian rank and actual-caller savings remain unknown; this is a scoped side lemma, not supplier admission.",
+ "budget_minutes": 240,
+ "stop_rule": "Stop at a proof/counterexample within two hours; reserve final time for exact verification and overlap refresh. No larger census or physical supplier campaign.",
+ "outcome": "completed",
+ "evidence": "PROOF.md, algebra.py and independently implemented literal-matrix verify.py; normal/optimized checks and source-bound RESULT.json.",
+ "author": "Krzysztof Wojt",
+ "ai_assistance": "Substantial OpenAI Codex assistance, with a Luna supporting finite census and read-only review; no human or proof-kernel review claimed.",
+ "open_questions": [
+ {
+ "question": "What is the exact length for higher-rank nonzero residual forms?",
+ "why_it_matters": "Separates residual-nullity cost from alternating or other completion obstructions.",
+ "first_step": "Analyze pivot choices that prevent an alternating residual obstruction, starting with higher-rank forms.",
+ "blocked_by": "A general normal-form/attainment proof; the lower bound need not be sharp."
+ },
+ {
+ "question": "Can one fully specified native caller exploit a short singular completion?",
+ "why_it_matters": "Formal word savings only matter if the complete physical bill improves.",
+ "first_step": "Fix signed constraints, required fixed spectator subspace and absolute phase; price all turns and corrections.",
+ "blocked_by": "No caller, native Gaussian tariff, owner/precision or complete recursive invoice is supplied."
+ }
+ ],
+ "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5094"
+}
diff --git a/research/singular-rank-two-pauli/VERIFY.json b/research/singular-rank-two-pauli/VERIFY.json
new file mode 100644
index 0000000000..6ae5fc3fd3
--- /dev/null
+++ b/research/singular-rank-two-pauli/VERIFY.json
@@ -0,0 +1,32 @@
+{
+ "schema_version": 1,
+ "status": "ready",
+ "python": "3.12",
+ "requirements": [],
+ "inputs": [],
+ "commands": [
+ {
+ "argv": [
+ "{python}",
+ "-W",
+ "error",
+ "-B",
+ "{package}/verify.py"
+ ],
+ "timeout_seconds": 120,
+ "checks": "Complete small symplectic Cayley census, general lower/upper bounds, exact singular words, larger fixtures, omission/input controls and source-bound receipt."
+ },
+ {
+ "argv": [
+ "{python}",
+ "-O",
+ "-W",
+ "error",
+ "-B",
+ "{package}/verify.py"
+ ],
+ "timeout_seconds": 120,
+ "checks": "Same finite certificate with Python assertions disabled."
+ }
+ ]
+}
diff --git a/research/singular-rank-two-pauli/algebra.py b/research/singular-rank-two-pauli/algebra.py
new file mode 100644
index 0000000000..4fe5fae8ca
--- /dev/null
+++ b/research/singular-rank-two-pauli/algebra.py
@@ -0,0 +1,182 @@
+"""Binary partial symplectic completion, with explicit bounded linear algebra.
+
+Krzysztof Wojt with OpenAI Codex assistance. Apache-2.0.
+Vectors pack (x_0,...,x_{n-1},z_0,...,z_{n-1}) into low-to-high bits.
+Words list axes in chronological application order. No predecessor code imported.
+"""
+
+MAX_QUBITS = 9
+
+
+def require(condition, message):
+ if not condition:
+ raise ValueError(message)
+
+
+def pairing(left, right, n):
+ mask = (1 << n) - 1
+ return (((left & mask) & (right >> n)).bit_count()
+ + ((right & mask) & (left >> n)).bit_count()) & 1
+
+
+def turn(vector, axis, n):
+ return vector ^ (axis if pairing(vector, axis, n) else 0)
+
+
+def apply_word(vector, axes, n):
+ for axis in axes:
+ vector = turn(vector, axis, n)
+ return vector
+
+
+def linear_combination(columns, mask):
+ result = 0
+ for index, column in enumerate(columns):
+ if (mask >> index) & 1:
+ result ^= column
+ return result
+
+
+def echelon(columns):
+ """Return pivot -> (value, original-column mask), and kernel masks."""
+ pivots = {}
+ kernel = []
+ for index, column in enumerate(columns):
+ value, coefficients = column, 1 << index
+ while value:
+ pivot = value.bit_length() - 1
+ if pivot not in pivots:
+ pivots[pivot] = (value, coefficients)
+ break
+ old, old_coefficients = pivots[pivot]
+ value ^= old
+ coefficients ^= old_coefficients
+ if not value:
+ kernel.append(coefficients)
+ return pivots, tuple(kernel)
+
+
+def rank(columns):
+ return len(echelon(columns)[0])
+
+
+def validate(n, source, target):
+ require(type(n) is int and 1 <= n <= MAX_QUBITS, "invalid dimension")
+ require(isinstance(source, (tuple, list)), "source must be a sequence")
+ require(isinstance(target, (tuple, list)), "target must be a sequence")
+ require(len(source) == len(target) <= 2 * n, "invalid basis length")
+ for vector in tuple(source) + tuple(target):
+ require(type(vector) is int and 0 < vector < (1 << (2 * n)),
+ "invalid basis vector")
+ require(rank(source) == len(source), "dependent source basis")
+ require(rank(target) == len(target), "noninjective target")
+ for i, left in enumerate(source):
+ for j, right in enumerate(source):
+ require(pairing(left, right, n) == pairing(target[i], target[j], n),
+ "map does not preserve the symplectic pairing")
+
+
+def residual_data(n, source, target):
+ validate(n, source, target)
+ difference = tuple(u ^ v for u, v in zip(source, target))
+ pivots, kernel = echelon(difference)
+ records = tuple(pivots[key] for key in sorted(pivots))
+ displacement = tuple(value for value, _ in records)
+ lifts = tuple(linear_combination(source, mask) for _, mask in records)
+ form = tuple(sum(pairing(u, d, n) << j for j, d in enumerate(displacement))
+ for u in lifts)
+ fixed = tuple(linear_combination(source, mask) for mask in kernel)
+ return displacement, lifts, form, fixed
+
+
+def solve_pairings(n, equations):
+ """Solve omega(vector, a)=rhs; free variables are set to zero."""
+ pivots = {}
+ mask = (1 << n) - 1
+ for vector, rhs in equations:
+ row = (vector >> n) | ((vector & mask) << n)
+ value = rhs
+ while row:
+ pivot = row.bit_length() - 1
+ if pivot not in pivots:
+ pivots[pivot] = (row, value)
+ break
+ old, old_value = pivots[pivot]
+ row ^= old
+ value ^= old_value
+ require(row != 0 or value == 0, "inconsistent pairing equations")
+ answer = 0
+ for pivot in sorted(pivots):
+ row, rhs = pivots[pivot]
+ if ((row & answer).bit_count() & 1) != rhs:
+ answer ^= 1 << pivot
+ require(all(pairing(v, answer, n) == rhs for v, rhs in equations),
+ "pairing solution check failed")
+ return answer
+
+
+def reduction_word(n, source, target):
+ """Complete any valid partial map in at most twice its displacement rank."""
+ validate(n, source, target)
+ current = tuple(target)
+ initial_rank = rank(tuple(u ^ v for u, v in zip(source, current)))
+ corrections = []
+ for _ in range(initial_rank):
+ difference = tuple(u ^ v for u, v in zip(source, current))
+ old_rank = rank(difference)
+ if old_rank == 0:
+ break
+ _, kernel = echelon(difference)
+ fixed = tuple(linear_combination(source, mask) for mask in kernel)
+ index = next(i for i, value in enumerate(difference) if value)
+ u, delta = source[index], difference[index]
+ if pairing(u, delta, n):
+ axes = (delta,)
+ else:
+ equations = tuple((k, 0) for k in fixed) + ((u, 1), (delta, 0))
+ axis = solve_pairings(n, equations)
+ axes = (axis, axis ^ delta)
+ require(all(0 < a < (1 << (2 * n)) for a in axes), "invalid axis")
+ require(all(apply_word(k, axes, n) == k for k in fixed), "fixed-space loss")
+ current = tuple(apply_word(v, axes, n) for v in current)
+ new_rank = rank(tuple(u ^ v for u, v in zip(source, current)))
+ require(new_rank < old_rank, "rank did not decrease")
+ corrections.extend(axes)
+ require(current == tuple(source), "incomplete reduction")
+ word = tuple(reversed(corrections))
+ require(len(word) <= 2 * initial_rank, "completion bound exceeded")
+ require(tuple(apply_word(u, word, n) for u in source) == tuple(target),
+ "completion endpoint mismatch")
+ return word
+
+
+def exact_completion(n, source, target):
+ """Solve zero residual forms at any rank, and rank-two rank-one forms.
+
+ Other nonzero forms are deliberately outside this successor's exact API.
+ The lower bound r + nullity(b) itself applies to every partial isometry.
+ """
+ displacement, _, form, _ = residual_data(n, source, target)
+ r, form_rank = len(displacement), rank(form)
+ minimum = 2 * r - form_rank
+ if form_rank == 0:
+ word = reduction_word(n, source, target)
+ else:
+ require(r == 2 and form_rank == 1, "outside exact classification")
+ axis = 0
+ for coefficients in (1, 2, 3):
+ quadratic = (coefficients & linear_combination(form, coefficients)).bit_count() & 1
+ if quadratic:
+ axis = linear_combination(displacement, coefficients)
+ break
+ require(axis != 0, "missing anisotropic residual vector")
+ reduced = tuple(turn(v, axis, n) for v in target)
+ new_displacement, _, new_form, _ = residual_data(n, source, reduced)
+ require(len(new_displacement) == 1 and rank(new_form) == 0,
+ "singular Schur complement mismatch")
+ word = reduction_word(n, source, reduced) + (axis,)
+ require(len(word) == minimum, "sharp length mismatch")
+ require(tuple(apply_word(u, word, n) for u in source) == tuple(target),
+ "sharp endpoint mismatch")
+ return {"displacement_rank": r, "form_rank": form_rank,
+ "minimum": minimum, "axes": word}
diff --git a/research/singular-rank-two-pauli/verify.py b/research/singular-rank-two-pauli/verify.py
new file mode 100644
index 0000000000..5f209d7e22
--- /dev/null
+++ b/research/singular-rank-two-pauli/verify.py
@@ -0,0 +1,265 @@
+#!/usr/bin/env python3
+"""Exact independent matrix oracle and bounded constructive checks.
+
+Krzysztof Wojt with OpenAI Codex assistance. Apache-2.0.
+No predecessor code, files, network, external solver or package dependencies.
+"""
+
+import argparse
+from collections import Counter, deque
+from hashlib import sha256
+from itertools import product
+import json
+from pathlib import Path
+
+import algebra
+
+
+def check(condition, message):
+ if not condition:
+ raise RuntimeError(message)
+
+
+def omega(u, v, n):
+ # Deliberately literal, separate from the constructor's packed formula.
+ answer = 0
+ for i in range(n):
+ answer ^= ((u >> i) & 1) * ((v >> (i + n)) & 1)
+ answer ^= ((v >> i) & 1) * ((u >> (i + n)) & 1)
+ return answer
+
+
+def act(matrix, vector):
+ return sum(((row & vector).bit_count() % 2) << i
+ for i, row in enumerate(matrix))
+
+
+def multiply(left, right):
+ rows = []
+ for mask in left:
+ row = 0
+ for j, value in enumerate(right):
+ if mask & (1 << j):
+ row ^= value
+ rows.append(row)
+ return tuple(rows)
+
+
+def literal_turn(n, axis):
+ m = 2 * n
+ functional = sum(omega(1 << j, axis, n) << j for j in range(m))
+ return tuple((1 << i) ^ (functional if axis & (1 << i) else 0)
+ for i in range(m))
+
+
+def word_matrix(n, axes):
+ result = tuple(1 << i for i in range(2 * n))
+ for axis in axes:
+ check(type(axis) is int and 0 < axis < (1 << (2 * n)), "invalid word axis")
+ result = multiply(literal_turn(n, axis), result)
+ return result
+
+
+def symplectic(matrix, n):
+ return all(omega(act(matrix, 1 << i), act(matrix, 1 << j), n)
+ == omega(1 << i, 1 << j, n)
+ for i in range(2 * n) for j in range(2 * n))
+
+
+def cayley(n):
+ # Complete matrix enumeration is separate from the word BFS.
+ m = 2 * n
+ matrices = {rows for rows in product(range(1, 1 << m), repeat=m)
+ if all(omega(rows[i], rows[j], n) == omega(1 << i, 1 << j, n)
+ for i in range(m) for j in range(m))}
+ identity = tuple(1 << i for i in range(m))
+ distance = {identity: 0}
+ queue = deque([identity])
+ turns = tuple(literal_turn(n, a) for a in range(1, 1 << m))
+ while queue:
+ current = queue.popleft()
+ for generator in turns:
+ following = multiply(generator, current)
+ if following not in distance:
+ distance[following] = distance[current] + 1
+ queue.append(following)
+ check(set(distance) == matrices, "matrix enumeration and BFS disagree")
+ check(len(distance) == (6 if n == 1 else 720), "group order mismatch")
+ expected = {0: 1, 1: 3, 2: 2} if n == 1 else {
+ 0: 1, 1: 15, 2: 85, 3: 225, 4: 274, 5: 120}
+ check(dict(Counter(distance.values())) == expected, "Cayley distance census mismatch")
+ return distance
+
+
+def span(basis):
+ values = {0}
+ for vector in basis:
+ values |= {value ^ vector for value in values}
+ return frozenset(values)
+
+
+def basis_of(values):
+ basis = []
+ generated = frozenset({0})
+ for vector in sorted(values):
+ if vector not in generated:
+ basis.append(vector)
+ generated = span(basis)
+ return tuple(basis)
+
+
+def subspaces(m):
+ spaces = {frozenset({0})}
+ for _ in range(m):
+ enlarged = set(spaces)
+ for space in spaces:
+ for vector in range(1, 1 << m):
+ enlarged.add(frozenset(set(space) | {u ^ vector for u in space}))
+ spaces = enlarged
+ check(len(spaces) == (5 if m == 2 else 67), "subspace census mismatch")
+ return sorted(spaces, key=lambda s: (len(s), tuple(sorted(s))))
+
+
+def independent_form(n, source, target):
+ # Enumerate the complete small U; no constructor elimination is used.
+ pairs = {0: 0}
+ for u, v in zip(source, target):
+ pairs.update({old ^ u: image ^ v for old, image in tuple(pairs.items())})
+ lifts = {u ^ v: u for u, v in pairs.items()}
+ displacement = basis_of(lifts)
+ rows = tuple(sum(omega(lifts[x], y, n) << j for j, y in enumerate(displacement))
+ for x in displacement)
+ return len(displacement), len(basis_of(rows))
+
+
+def verify_endpoint(n, source, target, axes):
+ matrix = word_matrix(n, axes)
+ check(symplectic(matrix, n), "word is not symplectic")
+ check(tuple(act(matrix, u) for u in source) == tuple(target), "literal endpoint mismatch")
+ return matrix
+
+
+def finite_census(n):
+ distances = cayley(n)
+ counts = Counter()
+ for space in subspaces(2 * n):
+ source = basis_of(space)
+ restrictions = {}
+ for matrix, distance in distances.items():
+ target = tuple(act(matrix, u) for u in source)
+ restrictions[target] = min(restrictions.get(target, 99), distance)
+ for target, minimum in restrictions.items():
+ r, br = independent_form(n, source, target)
+ counts["all_restrictions"] += 1
+ check(minimum >= 2 * r - br, "residual-nullity floor failed")
+ generic = algebra.reduction_word(n, source, target)
+ verify_endpoint(n, source, target, generic)
+ check(len(generic) <= 2 * r, "generic two-per-rank bound failed")
+ if br != 0 and (r, br) != (2, 1):
+ continue
+ solved = algebra.exact_completion(n, source, target)
+ check(solved["minimum"] == minimum, "exact Cayley minimum mismatch")
+ check((solved["displacement_rank"], solved["form_rank"]) == (r, br),
+ "independent residual data mismatch")
+ verify_endpoint(n, source, target, solved["axes"])
+ counts[f"exact_r{r}_b{br}"] += 1
+ for i in range(len(solved["axes"])):
+ short = solved["axes"][:i] + solved["axes"][i + 1:]
+ matrix = word_matrix(n, short)
+ check(tuple(act(matrix, u) for u in source) != target,
+ "omitted turn survived")
+ counts["rejected_omissions"] += 1
+ expected = 16 if n == 1 else 10096
+ check(counts["all_restrictions"] == expected, "restriction count mismatch")
+ if n == 2:
+ check(counts["exact_r2_b0"] == 30 and counts["exact_r2_b1"] == 1890,
+ "singular rank-two census mismatch")
+ return dict(sorted(counts.items()))
+
+
+def larger_fixtures():
+ counts = Counter()
+ for n in range(2, algebra.MAX_QUBITS + 1):
+ for r in range(1, n // 2 + 1):
+ source = tuple(1 << j for j in range(n)) + tuple(
+ 1 << (n + j) for j in range(2 * r, n))
+ target = tuple((1 << j) ^ ((1 << (r + j)) if j < r else 0)
+ for j in range(n)) + source[n:]
+ counts["zero_form_nilpotent_with_fixed_spectators"] += gauged_checks(n, source, target, 2 * r)
+ counts["zero_form_disjoint_source_and_displacement"] += gauged_checks(
+ n, source[:r], target[:r], 2 * r)
+ for pairs in range(1, n // 2 + 1):
+ source = tuple(1 << j for j in range(n))
+ target = list(source)
+ for i in range(pairs):
+ a, b = source[2 * i:2 * i + 2]
+ target[2 * i], target[2 * i + 1] = b, a ^ b
+ counts["zero_form_order_three"] += gauged_checks(n, source, tuple(target), 4 * pairs)
+ if n >= 3:
+ source = (1, 1 << n, 1 << (n + 2))
+ target = (1 ^ (1 << 1), 1 << n, (1 << (n + 2)) ^ (1 << 2))
+ counts["rank_one_form"] += gauged_checks(n, source, target, 3)
+ return dict(sorted(counts.items()))
+
+
+def gauged_checks(n, source, target, minimum):
+ count = 0
+ for seed in range(4):
+ axes = tuple(1 + ((19 * seed + 13 * j + j * j) % ((1 << (2 * n)) - 1))
+ for j in range(2 * n + seed))
+ gauge = word_matrix(n, axes)
+ left = tuple(act(gauge, u) for u in source)
+ right = tuple(act(gauge, v) for v in target)
+ solved = algebra.exact_completion(n, left, right)
+ check(solved["minimum"] == minimum, "larger expected minimum failed")
+ verify_endpoint(n, left, right, solved["axes"])
+ count += 1
+ return count
+
+
+def controls():
+ invalid = (
+ (True, (), ()), (0, (), ()), (10, (), ()),
+ (2, (True,), (1,)), (2, (0,), (1,)), (2, (16,), (1,)),
+ (2, (1,), ()), (2, (1, 1), (1, 2)),
+ (2, (1, 2), (1, 1)), (2, (1, 4), (1, 2)),
+ (1, (1,), (2,)),
+ )
+ for args in invalid:
+ try:
+ algebra.exact_completion(*args)
+ except ValueError:
+ continue
+ raise RuntimeError("invalid or out-of-scope input accepted")
+ try:
+ word_matrix(2, (0,))
+ except RuntimeError:
+ return len(invalid) + 1
+ raise RuntimeError("zero axis accepted")
+
+
+def main():
+ parser = argparse.ArgumentParser(description=__doc__)
+ parser.add_argument("--write-report", action="store_true")
+ args = parser.parse_args()
+ counts = {"dimension_2": finite_census(1), "dimension_4": finite_census(2),
+ "larger_fixtures": larger_fixtures(), "rejection_controls": controls()}
+ names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json",
+ "algebra.py", "verify.py")
+ root = Path(__file__).resolve().parent
+ hashes = {name: sha256((root / name).read_bytes()).hexdigest() for name in names}
+ report = {"status": "PASS_SINGULAR_PARTIAL_PAULI_COMPLETION", "counts": counts,
+ "source_sha256": hashes,
+ "scope": "Unsigned finite corroboration and witnesses; uniform theorem in PROOF.md. No physical cost or new kappa."}
+ rendered = json.dumps(report, indent=2, sort_keys=True) + "\n"
+ if args.write_report:
+ (root / "RESULT.json").write_text(rendered, encoding="utf-8")
+ else:
+ stored = (root / "RESULT.json").read_bytes()
+ check(len(stored) <= 1048576, "oversized receipt")
+ check(json.loads(stored) == report, "stored report differs from recomputation")
+ print(rendered, end="")
+
+
+if __name__ == "__main__":
+ main()