Prove the exact two-transvection cutoff for partial Pauli maps

research/partial-pauli-two-transvection/PROOF.md

@@ -0,0 +1,200 @@
+# Exact low-length completion of a partial Pauli contract
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+The claim is a scoped algebraic proof. Its new repository application is an
+exact low-length completion decision for the partial contracts in
+[JoyboyBrian's PR5051](https://github.com/CrocSwap/integer-mult-bounds/pull/5051),
+head `0960807a68ff46acbe6510c8867912ef2324ee71`. That predecessor supplies the
+compatibility problem and a general construction, rather than this optimum.
+Binary symplectic transvections and residual bilinear forms are classical.
+No literature-priority claim is made. No predecessor verifier is imported or run.
+
+## Model and statement
+
+Let V be a finite-dimensional nondegenerate symplectic space over F2, with
+alternating pairing omega. Let U be any subspace and let h:U -> V be an
+injective linear isometry. Its displacement is d(u)=h(u)+u, its displacement
+space is D=d(U), and r=dim D. A transvection with nonzero axis a is
+
+    T_a(v) = v + omega(v,a) a.
+
+Let ell(h) be the least number of such transvections in a symplectic map
+whose restriction to U equals h. Transvections may act on the full given V;
+no new dimensions are adjoined. This is an unsigned label-word length.
+
+The following bilinear form on D is well defined:
+
+    b(d(u),d(v)) = omega(u,d(v)).                         (1)
+
+Here "alternating" means b(x,x)=0 for every x, not merely that the ambient
+symplectic pairing is alternating. The exact cutoff is:
+
+| Displacement data | Conclusion |
+|---|---|
+| r=0 | ell(h)=0 |
+| r=1 and b is nonzero | ell(h)=1 |
+| r=1 and b=0 | ell(h)=2 |
+| r=2 and b is nonsingular and nonalternating | ell(h)=2 |
+| r=2 and b is nonsingular and alternating | ell(h)=3 |
+| r=2 and b is singular | ell(h)>=3 |
+| r>2 | ell(h)>=r |
+
+In particular, the first four rows are necessary and sufficient for ell(h)<=2.
+This statement classifies every partial isometry at that cutoff. The last two
+rows deliberately give only lower bounds, not an infeasibility conclusion or
+a classification of every longer word. The executable API uses `minimum=None`
+for those rows.
+
+For a compatible signed Hermitian-Pauli contract, use the same tariff when
+arbitrary Pauli conjugations are free and each literal quarter-turn is charged
+one unit. Signs do not change this tariff. This is a declared formal alphabet;
+turn count is not Gaussian paid rank, recursive-child rank or physical cost.
+
+## The induced form and the rank lower bound
+
+If z is in ker d, then h(z)=z. Isometry gives
+
+    omega(z,d(v)) = omega(h(z),h(v)) + omega(z,v) = 0.
+
+Changing the preimage u of d(u) in (1) therefore changes nothing. Bilinearity
+and well-definedness in the other argument are immediate. Expanding the
+isometry equation for u,v gives
+
+    b(x,y) + b(y,x) = omega(x,y),  for x,y in D.          (2)
+
+Each T_a-I has rank one on V. The identity AB-I=A(B-I)+(A-I) implies
+rank(S-I)<=t for a product S of t transvections. Since (S-I)|U=d for an
+extension, ell(h)>=r. In particular only r<=2 can pass the two-turn cutoff.
+
+## Rank-one displacement
+
+Write D=<d0> and d(u)=alpha(u)d0, with alpha a nonzero functional on U.
+Equation (1) says
+
+    omega(u,d0) = alpha(u)b(d0,d0).
+
+If b(d0,d0)=1, T_d0 agrees with h, and the rank bound proves ell(h)=1.
+Conversely, any single turn extending a nonidentity h must have axis d0,
+so this condition is necessary for length one.
+
+If b=0, then U is orthogonal to d0. Choose a in V satisfying
+
+    omega(u,a)=alpha(u) for every u in U,
+    omega(d0,a)=0.                                     (3)
+
+This is a consistent linear functional on U+<d0>. Indeed, if d0 belongs
+to U, injectivity of h forces alpha(d0)=0: otherwise h(d0)=0. If d0 is
+outside U there is no additional relation. Nondegeneracy of omega supplies a
+representing a, by solving a linear system. Since alpha is nonzero and
+omega(U,d0)=0, a is neither zero nor d0. Thus a and a+d0 are distinct
+nonzero orthogonal axes. Their commuting turns give, for u in U,
+
+    T_(a+d0) T_a(u) = u + alpha(u)d0 = h(u).
+
+The one-turn exclusion proves ell(h)=2. No clean ancilla or enlarged V was used.
+
+## Exactly two turns at rank two
+
+First consider two distinct nonzero axes a,c. They are linearly independent
+over F2. Put gamma=omega(a,c). The displacement of S=T_c T_a is
+
+    (S-I)v = omega(v,a)a + (omega(v,c)+gamma omega(v,a))c. (4)
+
+Nondegeneracy makes the two functionals omega(-,a), omega(-,c) independent.
+Consequently im(S-I)=<a,c> and rank(S-I)=2. In the ordered basis (a,c),
+the residual form defined as in (1), now on all of V, has matrix
+
+    [1 gamma]
+    [0   1  ].                                         (5)
+
+This follows directly by substituting (4) into b((S-I)v,a)=omega(v,a)
+and b((S-I)v,c)=omega(v,c). If S extends a partial map of displacement
+rank two, its full displacement space equals D, so its residual form is
+the form already fixed by the partial contract. Hence b must be nonsingular
+and nonalternating. Equal axes instead cancel and cannot have rank two.
+
+Conversely suppose r=2 and b is nonsingular and nonalternating. Choose
+a in D with b(a,a)=1. The kernel of the nonzero functional x -> b(x,a)
+is a line different from <a>; choose its nonzero element c. In this basis
+b(c,a)=0, and nonsingularity forces b(c,c)=1. Equation (2) gives
+b(a,c)=omega(a,c)=gamma. Thus b has exactly the form (5).
+
+For d(u)=lambda a+mu c, equation (1) now gives
+
+    omega(u,a)=lambda,
+    omega(u,c)=gamma lambda+mu.
+
+Formula (4) therefore equals d(u). The two turns extend h, and rank two
+excludes every shorter word. This also proves the singular-form obstruction.
+All choices require only linear algebra in the two-dimensional D.
+
+## The alternating three-turn boundary
+
+For a nonsingular alternating form on a binary two-space, every basis (a,c)
+has b(a,c)=b(c,a)=1 and zero diagonal. Equation (2) says omega(a,c)=0.
+Equation (1) gives
+
+    d(u)=omega(u,c)a+omega(u,a)c.
+
+The three distinct nonzero axes a,c,a+c are pairwise orthogonal. Multiplying
+their commuting turns gives on all of V
+
+    T_(a+c) T_c T_a(v) = v + omega(v,c)a + omega(v,a)c.
+
+This extends h. The preceding two-turn criterion excludes shorter words,
+so ell(h)=3. For an explicit full contract in any dimension at least four,
+take a,c independent isotropic basis vectors, fix them and every other
+standard basis vector except their duals, and send
+
+    f_a -> f_a+c,   f_c -> f_c+a.
+
+The new criterion proves its exact three-turn cost directly. This example is
+a boundary witness for the cutoff, not an additional supplier construction.
+
+## Signed Hermitian Paulis
+
+Write a label as (x,z), and H_v=i^(popcount(x & z)) X^x Z^z. It is Hermitian
+and squares to I. The literal unitary
+
+    C_a = (I-i H_a)/(1-i)
+
+has Gaussian-dyadic entries and conjugates labels by T_a. Direct multiplication
+gives C_a H_v C_a^-1=H_v when the labels commute, and -i H_a H_v otherwise.
+Thus each attaining label word above has an actual Clifford lift.
+
+For independent source generators, let U0 be that lift. Its output signs may
+differ from the desired signs. The differences specify a functional on h(U).
+Extend this functional to V and represent it by omega(k,-). Conjugating last
+by H_k supplies exactly those sign differences. For dependent equations,
+compatibility of the actual central product phases is a premise, as stated in
+PR5051, so the same correction handles the whole contract. Any word with
+Pauli conjugations inserted has the same unsigned transvection label word;
+therefore free sign corrections cannot beat the lower bounds.
+
+Conjugation equations leave a global scalar phase unspecified. Equality with
+an independently supplied absolute-phase target still needs its own anchor.
+Tensorizing an actual chosen word is valid, but no tensorized paid-rank or
+precision invoice follows from this turn-count theorem.
+
+## Evidence and scope
+
+The proof is uniform in dim V. The finite census independently enumerates
+literal binary symplectic matrices and a complete transvection Cayley graph
+through dimension four. For every source subspace it groups full maps by their
+restricted target images, takes the minimum literal word length, and compares
+the new classifier and every returned witness. Complete sign choices are checked
+only for independent Hermitian generators in the rows where a sharp word is
+returned. The finite counts and file-bound receipt come from `verify.py`.
+
+This is not an audit of PR5051 or the native compiler. The predecessor's proof
+and executable are not dependencies. The all-size claim rests on this written
+argument, with classical transvection structure credited. A general transvection
+reference is Brown and Humphries, [Orbits under symplectic transvections](https://groupoids.org.uk/pdffiles/brown-humphries1.pdf),
+whose introduction also distinguishes generation from individual word length.
+No external theorem from that paper is needed in the cutoff proof above.
+
+No native cost optimum, actual profitable caller, compiler or supplier admission,
+physical movement, dirty-owner schedule, precision, storage, stock, complete
+multiplication theorem or new kappa is established. Independent human and formal
+proof-kernel review are unclaimed.

research/partial-pauli-two-transvection/README.md

@@ -0,0 +1,168 @@
+# Exact low-length completion of partial Pauli contracts
+
+This contribution was produced by Nick Petalas. Apache-2.0.
+
+Claim type: scoped algebraic proof with an exact finite certificate. No new kappa.
+
+For an injective binary symplectic partial map h:U -> V, put D=(h-I)U,
+r=dim D, and define its residual bilinear form by
+
+    b((h-I)u,(h-I)v) = omega(u,(h-I)v).
+
+The form is well defined even when h is specified only on U. Its rank and
+alternating property give an exact decision at the two-transvection cutoff:
+
+| Displacement data | Exact length or proved lower bound |
+|---|---|
+| r=0 | 0 |
+| r=1, b nonzero | 1 |
+| r=1, b=0 | 2 |
+| r=2, b nonsingular and nonalternating | 2 |
+| r=2, b nonsingular and alternating | 3 |
+| r=2, b singular | at least 3 |
+| r>2 | at least r |
+
+The first four rows classify every partial contract admitting at most two
+turns. The fifth row is a sharp boundary. The last two rows leave the longer
+optimum open. [PROOF.md](PROOF.md) gives the dimension-uniform argument and
+explicit attaining words. The rank-one zero-form case constructs two axes
+by a linear system in the existing ambient space, without adjoining ancillas.
+
+For compatible signed Hermitian-Pauli equations, the same lengths are exact
+when arbitrary Pauli sign corrections are free and each quarter-turn costs
+one unit. Every attaining unsigned word lifts to literal Gaussian-dyadic
+Clifford turns, followed by one Pauli conjugation correcting the signs.
+The global scalar phase remains free. This is a formal turn-count tariff,
+separate from native Gaussian rank and the complete physical invoice.
+
+## What this adds
+
+[JoyboyBrian's PR5051](https://github.com/CrocSwap/integer-mult-bounds/pull/5051),
+head `0960807a68ff46acbe6510c8867912ef2324ee71`, supplies the partial signed
+compatibility contract and a general completion construction. It leaves
+optimization open. This contribution adds the exact low-length test, attaining
+words, and the three-turn alternating boundary. It does not replay or audit
+that predecessor. Classical symplectic and residual-form theory is credited;
+no literature-priority claim is made.
+
+The criterion prevents two false simplifications. Displacement rank one can
+require two turns. A nonsingular rank-two residual form can still require
+three if it is alternating. A singular rank-two form cannot pass the two-turn
+cutoff. The API returns `minimum=None` and a lower bound when no exact optimum
+is supplied, so that rejection at this cutoff is never called nonexistence.
+
+## Exact finite evidence
+
+The standalone verifier independently constructs the complete literal
+symplectic matrix corpus and complete transvection Cayley distances. For each
+source subspace it groups full maps by their restricted images and takes the
+minimum word length in that group. It compares the new criterion against every
+such partial map, including all its returned attaining words.
+
+| Binary symplectic dimension | Source subspaces | Partial label contracts |
+|---|---:|---:|
+| 0 | 1 | 1 |
+| 2 | 5 | 16 |
+| 4 | 67 | 10,096 |
+
+There are 10,113 contracts in total. The verifier checks every independent
+Hermitian sign choice for the contracts receiving a sharp attaining word,
+giving 23,231 signed basis contracts. The signed checks enumerate all possible
+final Pauli corrections and compare the linear-system solution with that
+literal fiber. They do not enumerate arbitrary dependent signed lists.
+
+Sixteen further fixed examples cover n=2 through n=9. Eleven malformed
+contracts, an inconsistent linear system, and three mathematical boundary
+fixtures exercise rejection and distinguish rank-only, nonsingularity-only
+and unrestricted two-turn claims. Every check remains active under `-O`.
+The receipt is generated on stdout and binds all seven package files by SHA256.
+No receipt or replay output is hand-written or stored in the checkout.
+
+## Reproduce
+
+From the repository root, using the Python 3.12 standard library:
+
+```sh
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error -X dev research/partial-pauli-two-transvection/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error -X dev -O research/partial-pauli-two-transvection/verify.py
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/partial-pauli-two-transvection
+/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/partial-pauli-two-transvection --check-source-history
+```
+
+A different CPython 3.12 installation may replace the local interpreter path.
+Expected scientific marker is `PASS_PARTIAL_PAULI_TWO_TRANSVECTION no_new_kappa`.
+The last command requires the publication commit and full history. Registered
+normal and optimized checks each have a 120-second limit. Direct verification
+also works in a Git-free copy containing these seven files. The package runner
+isolates import bytecode; direct calls assume the local source directory has
+no stale bytecode imports.
+
+The source-bound orientation required by the card passed with the current
+`scripts/research_selected_baseline.py`; this authenticates selected metadata,
+not the selected scientific construction. The `formal-interface-lemma` card
+is explicitly changed to original algebraic successor work in TASK.json.
+No selected scientific replay, Lean, Docker or historical suite is required
+for or claimed by this result.
+
+## Limits and implementation bounds
+
+The proof covers arbitrary finite binary symplectic dimension and arbitrary U.
+The executable API accepts n<=9 and a basis of at most 18 vectors; dependent
+signed equations must first satisfy the cited compatibility contract. Exact
+word minima are exhaustively corroborated only through n=2. The fixed n<=9
+examples do not make a larger exhaustive-census claim.
+
+All new code uses direct calls, structured loops and explicit failures, with
+no recursion, subprocesses, network, solver, code generation or shared mutable
+state. Functions remain below 60 physical lines. API validation rejects Boolean
+integers, invalid dimensions, over-capacity bases, dependent bases and maps that
+fail to preserve omega. Internal checks verify the nonzero axes and actual
+source-to-target action of every returned word.
+
+Power of Ten rule 3 deviation: CPython allocates integers, tuples and sets while
+executing. The API's largest span has at most 2^18 entries. The exhaustive
+checker is restricted to n<=2, at most 65,536 candidate matrices and a six-round
+Cayley search, at most 720 accepted matrices and 67 source subspaces. It retains
+one subspace's at most 720 restrictions, one attaining word and small counters.
+Each receipt read is limited to seven fixed files of at most 1 MiB. These
+finite capacities bound live state; a fixed-buffer implementation is required
+before using this code in a runtime that prohibits allocation. Warning-strict
+normal and optimized replays provide the available interpreter diagnostics;
+no external linter or type-checker run is claimed.
+
+Native paid rank, arbitrary absolute-phase targets, a profitable physical
+caller, owner endpoints, routing, dirty restoration, precision, storage, stock,
+compiler and outer admission remain open. The selected frontier is unchanged.
+Independent human and formal proof-kernel review are unclaimed.
+
+## Open next questions
+
+1. What is the exact minimum when the rank-two residual form is singular?
+   Start with fixed source spaces for zero and rank-one residual forms. The
+   blocker is the least larger ambient displacement space admitting a completion,
+   rather than another two-turn enumeration.
+2. Can one actual partial signed source contract use this test to reduce its
+   complete physical bill? First fix its caller, phase anchor and dirty-owner
+   contract, then price native Gaussian rank and every retained obligation.
+   Shorter turn length alone does not remove a paid recursive call.
+
+## Credit and related work
+
+JoyboyBrian's #5051 supplies the immediate signed-contract question. David
+Ganz / Dugongue's #4841 supplies native Clifford compilation context. Cao
+Yifan / intqwq #4610, Cinna Davis, zxv, Jacob Alan Sussman and the retained
+native/owner/compiler lineage retain their credit. None of their code is
+copied, modified, imported or replayed here. Citation-only URLs and heads are
+recorded separately from the two historical provenance pins in SOURCES.json.
+No pending Git object is needed for a clean replay.
+
+Nick Petalas's #4864 studies outputs of constrained simultaneous chart moves,
+#4859 studies words between Lagrangian charts, and #4919 studies unrestricted
+GL maps between subspace triples. Those are different objects from a prescribed
+pointwise partial signed-Pauli map. This contribution targets the explicit
+completion-cost gap in the other contributor's #5051, without extending those
+recent packages or comparing their numerical counts.
+
+The classical context includes Ronald Brown and Stephen P. Humphries,
+[Orbits under symplectic transvections](https://groupoids.org.uk/pdffiles/brown-humphries1.pdf).
+The cutoff proof is self-contained and uses no external theorem from that paper.