Prove exact 2r-1 completion for rank-one residual forms (no κ)

research/rank-one-residual-completion/PROOF.md

@@ -0,0 +1,104 @@
+# Rank-one residual forms at every displacement rank
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped algebraic proof. The new cases have displacement rank
+at least three. Krzysztof Wojt's [PR5097](https://github.com/CrocSwap/integer-mult-bounds/pull/5097)
+provides the lower bound, zero-form construction and rank-two predecessor.
+Nick Petalas's PR5085 provides the residual-form and low-length framework.
+The present step is the dimension-independent rank-one pivot below.
+
+Let V be a finite-dimensional nondegenerate symplectic space over F2, with
+pairing omega. Let h:U -> V be an injective linear map preserving omega on U.
+Set d=h+I, D=d(U), r=dim D, and define
+
+    b(d(u), d(v)) = omega(u, d(v)).
+
+This is well defined. If k is fixed by h, preservation of its pairing with
+u implies omega(k,d(u))=0. Expanding the isometry identity also gives
+
+    b(x,y) + b(y,x) = omega(x,y), for x,y in D.             (1)
+
+Suppose b has rank exactly one. Then the least length ell(h) of a product
+of nonzero-axis symplectic transvections extending h is
+
+    ell(h) = 2r - 1.                                    (2)
+
+Every axis lies in V. No ancillary dimension is adjoined. The extension is
+free outside U. Required fixed spectators must therefore be included in U.
+
+## Lower bound, credited predecessor argument
+
+For any full symplectic extension S, put W=im(S+I). Its residual form B,
+defined by B((S+I)v,w)=omega(v,w), is nonsingular and restricts to b on D.
+Indeed W-perp=ker(S+I); this proves both well-definedness and nonsingularity.
+The left radical of b injects into (W/D)* through B. Thus
+
+    dim W >= r + nullity(b) = 2r-1.
+
+Rank subadditivity applied to a transvection word gives length at least
+rank(S+I)=dim W. This is PR5097's displacement-plus-nullity lower bound,
+restated to make the present proof self-contained.
+
+## One pivot leaves a zero form
+
+A nonzero rank-one bilinear form factors as b(x,y)=lambda(x) mu(y), for
+nonzero binary functionals lambda and mu. There is an a with
+lambda(a)=mu(a)=1. If the functionals coincide, choose any vector on which
+they are one. If they differ, they are independent and the two equations
+are solvable. Therefore b(a,a)=1, and
+
+    b(x,y) = b(x,a) b(a,y).                             (3)
+
+Let T_a(v)=v+omega(v,a)a and h'=T_a h. Equations (1) give
+
+    d'(u) = d(u) + b(a,d(u))a.
+
+The map P:x -> x+b(a,x)a on D has kernel <a> and image
+L=ker b(a,-). Hence dim d'(U)=r-1.
+
+For x,y in L, choose u,v with d(u)=x and d(v)=y. Since P fixes L,
+d'(u)=x and d'(v)=y. The residual form of h' is consequently
+
+    b'(x,y)=omega(u,y)=b(x,y)=0,
+
+where the final equality uses (3) and b(a,y)=0. Thus the new residual form
+is identically zero on all r-1 displacement dimensions. This argument
+uses rank one, without a restriction to a two-dimensional D.
+
+PR5097 proves that a zero residual form of displacement rank s has an
+attaining 2s-turn completion in the original V. Apply it with s=r-1 and
+undo T_a. This yields at most 1+2(r-1)=2r-1 turns. The lower bound proves
+equality. When r=1, h' is already the identity on U.
+
+## Explicit completion of the zero-form remainder
+
+For completeness, the constructor uses the predecessor's general at-most-2s
+reduction. At a current partial isometry let K be its fixed subspace. Pick
+u outside K and set p=h(u)+u. If omega(u,p)=1, the one turn T_p corrects u
+and fixes K. Otherwise solve
+
+    omega(K,a)=0, omega(u,a)=1, omega(p,a)=0.
+
+The equations are consistent because u is not in K+<p>. Otherwise either
+u is fixed, or h(u) is a member k of K with h(k)=k, contrary to injectivity.
+Nondegeneracy represents this consistent functional by a in V.
+The two nonzero orthogonal axes a and a+p give an involution correcting u
+and fixing K. The new displacement rank decreases by at least one.
+After at most s reductions the map is fixed on U. Reversing the correction
+word gives its extension. On a zero-form input the lower bound 2s forces
+this at-most-2s construction to attain exactly 2s.
+
+## Interface and limits
+
+The new theorem optimizes unsigned binary symplectic transvection count.
+Under PR5085/PR5051's compatible signed-Pauli contract and free arbitrary
+Pauli-correction tariff, the same minimum applies to the projective signed
+lift. That is a cited interface implication, not a new phase implementation.
+Absolute target phase needs an amplitude anchor. Every monomial pass and
+native Gaussian service still needs pricing by an actual physical caller.
+
+No improvement to native paid rank, recursive children, a complete supplier
+invoice or kappa follows from (2) alone. Arbitrary higher-rank residual forms
+remain open here. Finite checks corroborate the written proof; they do not
+constitute independent human review or formal proof-kernel verification.

research/rank-one-residual-completion/README.md

@@ -0,0 +1,130 @@
+# Exact all-rank completion for a rank-one residual form
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped algebraic proof with exact finite corroboration. For an
+injective binary symplectic partial map h:U -> V, let D=(h+I)U, r=dim D,
+and let b((h+I)u,(h+I)v)=omega(u,(h+I)v). If rank b=1, then
+
+    minimum transvection length = 2r-1.
+
+The new cases have r at least three. Krzysztof Wojt's
+[PR5097](https://github.com/CrocSwap/integer-mult-bounds/pull/5097) proves
+the lower bound r+nullity(b), the zero-form optimum 2r, and the rank-two
+rank-one case. Its Open next question 1 asks about higher-rank nonzero forms.
+This contribution supplies the attaining word for the rank-one slice at
+every r. At r=3 it closes the interval [5,6] at five. It does not classify
+other residual ranks or improve kappa.
+
+[PROOF.md](PROOF.md) shows that one anisotropic pivot leaves a zero residual
+form on r-1 displacement dimensions. The predecessor's two-turn reduction
+then finishes the word. [completion.py](completion.py) implements that
+construction locally. It validates independence, injectivity and preservation
+of pairings, and rejects residual forms whose rank differs from one.
+
+All axes lie in the original V. The action outside U is free. Required fixed
+spectators must be prescribed in U, and the implementation preserves them.
+Under the cited signed-Pauli contract, compatible sign corrections are free
+in this formal tariff. Absolute phase and physical costs are separate.
+
+## Exact evidence and reproduction
+
+From the repository root, with CPython 3.12 and the standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/rank-one-residual-completion/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/rank-one-residual-completion/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rank-one-residual-completion
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rank-one-residual-completion --check-source-history
+```
+
+Other machines may substitute their CPython 3.12 path. The standalone marker
+is `PASS_RANK_ONE_RESIDUAL_COMPLETION`; the launcher must also print
+`PASS_REGISTERED_RESEARCH_PACKAGE`. Receipts are generated on stdout and bind
+every regular package file by SHA256. No receipt is hand-written or stored in
+the checkout. The standalone commands are read-only and require no Git or
+external source inputs.
+
+The finite checks cover exactly:
+
+- Every nonzero rank-one binary form in dimensions 3, 4 and 5, represented
+  uniquely as p q-transpose for nonzero p,q. There are 1,235 forms. Each has
+  a literal symplectic realization and two prescribed fixed spectators.
+- All 242 of those forms with zero diagonal, where a sum of basis vectors
+  rather than a basis vector must supply the anisotropic pivot.
+- 52 larger or conjugated fixtures, through displacement rank 12, including
+  a rank-three contract in the original six-dimensional ambient space.
+- Independent dense-coordinate evaluation of every emitted full matrix,
+  every prescribed image, all symplectic pairings and full displacement rank
+  exactly 2r-1. The checker uses dense row elimination rather than the
+  constructor's packed binary elimination.
+- 182 rejecting one-turn omissions, plus malformed/out-of-scope contracts
+  and an inconsistent pairing system. The generated receipt gives the
+  control count.
+
+These are finite corroborations of the written dimension-uniform proof.
+They do not enumerate all partial maps in the tested dimensions. No
+predecessor scientific executable, receipt, census or compiler is replayed.
+
+## Scope and provenance
+
+Base: canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority
+revision 8, selected PR6030. [TASK.json](TASK.json) records the explicit change
+from the formal-interface-lemma card to this written interface side result.
+[SOURCES.json](SOURCES.json) pins the problem statements as provenance only.
+The selected source-binding orientation command passed. The advance
+[claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19363481)
+and scoped overlap checks precede the construction.
+
+The turn count is an abstract tariff. It is not native Gaussian rank, paid
+recursive rank, a favorable supplier invoice, physical tape cost or a new
+multiplication theorem. A compatible signed lift with charged monomial
+passes, phase anchor, actual caller, dirty-owner restoration, precision,
+stock and compiler/outer admission remains to be supplied. The selected
+frontier and five retained assumptions are unchanged. Selected cold replay,
+Lean and Docker were not run. Independent human and formal proof-kernel
+review are unclaimed. CI results belong in the PR body.
+
+## Implementation bounds
+
+The public `complete` entry point accepts at most 16 qubits, hence at most
+32 basis vectors and 32-bit ambient vectors. Every elimination loop is bounded
+by these dimensions. A correction has at most 2r-1 turns and each step
+strictly decreases displacement rank. Helpers operate on validated internal
+data. The mathematical theorem has no dimension cap.
+
+Power of Ten rule 3 has a managed-runtime deviation in `completion.py` and
+`verify.py`. Python allocates integers and collections during execution.
+The API cap above bounds the live algebraic data; the verifier has fixed
+finite census bounds and does not accumulate per-case matrices. Verification
+checks the accepted cap and rejects a dimension above it. A fixed-capacity
+native implementation would be needed before a steady-allocation claim.
+Rule 10 uses warning-strict normal/optimized replay and source compilation;
+availability of additional static diagnostics is recorded in the PR body.
+No function exceeds 60 physical lines. There is no recursion, dynamic code
+generation, network access or subprocess execution in either scientific file.
+The verifier loads the named local completion module through the standard
+import loader; that is its sole dynamic dispatch boundary.
+
+## Open next questions
+
+- Determine an attaining formula for residual rank two at displacement rank
+  at least three. First examine the residual form after an anisotropic pivot;
+  a nonzero alternating remainder is an unresolved obstruction here.
+- Price one actual signed native contact satisfying this partial contract.
+  Include fixed spectators and an absolute phase anchor, then charge every
+  turn, Pauli correction, monomial pass and owner/restoration operation.
+  A shorter formal word alone gives no recursive saving.
+
+## Credit
+
+Krzysztof Wojt / krzysztofwojt / PR5097 supplies the explicit higher-rank
+question, displacement-plus-nullity lower bound, zero-form construction and
+rank-two pivot proof. Nick Petalas / PR5085 supplies the residual form and
+low-length cutoff. Brian / JoyboyBrian / PR5051 supplies signed compatibility;
+David Ganz / Dugongue / PR4841 supplies native compiler context. Cao Yifan /
+intqwq, Cinna Davis, zxv, Jacob Alan Sussman and the retained native/compiler
+lineage retain their predecessor credit. Symplectic transvections, residual
+forms and binary elimination are classical. No literature-priority claim is
+made. The new step is the all-rank rank-one attainment proof and its local
+constructor; predecessor files and credit lines are unchanged.

research/rank-one-residual-completion/SOURCES.json

@@ -0,0 +1,43 @@
+{
+  "schema_version": 1,
+  "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a",
+      "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec",
+      "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81"
+    },
+    {
+      "path": "research/singular-rank-two-pauli/README.md",
+      "usage": "provenance",
+      "git_blob": "340e9004be1cbc28917adac5db6dfa8950c00dc5",
+      "sha256": "2be2b460c1ce24261e3f887cb583163e86233217a6ccaa61c9a6a8b8d1ec7cb0"
+    },
+    {
+      "path": "research/singular-rank-two-pauli/PROOF.md",
+      "usage": "provenance",
+      "git_blob": "c8ffbe676f33e14105c188959e47d8aafeaaae3e",
+      "sha256": "bc43da28cf432e370532cdeb1622ce8efb175d497fe83b632d8560fd27c20a5b"
+    },
+    {
+      "path": "research/partial-pauli-two-transvection/README.md",
+      "usage": "provenance",
+      "git_blob": "fa6116dfce698f9e51ed910d974c9707028ca3e6",
+      "sha256": "06b3084c46bea30e06519385258a355c4b6d9b622281e1fda9a5b794b233a2c5"
+    },
+    {
+      "path": "research/signed-pauli-partial-extension/README.md",
+      "usage": "provenance",
+      "git_blob": "b7f3c12b91656ce3ee1c1753a2799fd1861345a9",
+      "sha256": "8bde3fc092ef164f974d63350df97b95bcab3d490d71bc3d9100baaaf9693666"
+    }
+  ],
+  "credit": "PR5097 poses the higher-rank question and supplies the lower bound and zero-form construction; PR5085 and PR5051 supply residual and signed-contract context. No predecessor scientific replay is a deliverable."
+}