From d32b46c02387b3bc9dc0bea344b2c6271b08c5f9 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 09:24:11 +0100 Subject: [PATCH] feat(research): classify low-length partial Pauli completions --- .../partial-pauli-two-transvection/PROOF.md | 200 +++++++++++++++++ .../partial-pauli-two-transvection/README.md | 168 +++++++++++++++ .../SOURCES.json | 40 ++++ .../partial-pauli-two-transvection/TASK.json | 136 ++++++++++++ .../VERIFY.json | 36 ++++ .../partial-pauli-two-transvection/algebra.py | 144 +++++++++++++ .../partial-pauli-two-transvection/verify.py | 202 ++++++++++++++++++ 7 files changed, 926 insertions(+) create mode 100644 research/partial-pauli-two-transvection/PROOF.md create mode 100644 research/partial-pauli-two-transvection/README.md create mode 100644 research/partial-pauli-two-transvection/SOURCES.json create mode 100644 research/partial-pauli-two-transvection/TASK.json create mode 100644 research/partial-pauli-two-transvection/VERIFY.json create mode 100644 research/partial-pauli-two-transvection/algebra.py create mode 100644 research/partial-pauli-two-transvection/verify.py diff --git a/research/partial-pauli-two-transvection/PROOF.md b/research/partial-pauli-two-transvection/PROOF.md new file mode 100644 index 0000000000..20cf3e0f5e --- /dev/null +++ b/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= 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+. 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)= 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 ; 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. diff --git a/research/partial-pauli-two-transvection/README.md b/research/partial-pauli-two-transvection/README.md new file mode 100644 index 0000000000..fa6116dfce --- /dev/null +++ b/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. diff --git a/research/partial-pauli-two-transvection/SOURCES.json b/research/partial-pauli-two-transvection/SOURCES.json new file mode 100644 index 0000000000..14c62ca0b4 --- /dev/null +++ b/research/partial-pauli-two-transvection/SOURCES.json @@ -0,0 +1,40 @@ +{ + "schema_version": 1, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "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" + } + ], + "citation_only_references": [ + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/5051", + "head": "0960807a68ff46acbe6510c8867912ef2324ee71", + "author": "JoyboyBrian", + "path": "research/signed-pauli-partial-extension/PROOF.md", + "sha256": "00b495bbf278a98ded6aef6bee7938b821f9b1effcb58d60a19a4706203265ea", + "usage": "Citation only. No bytes or results are loaded at runtime; the new cutoff proof is self-contained." + }, + { + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/4841", + "head": "6debdcdac8fe1c87958f8cd42ccb7db73c0a0eef", + "author": "David Ganz / Dugongue", + "usage": "Native compiler context only; no compiler import or claimed tariff." + }, + { + "url": "https://groupoids.org.uk/pdffiles/brown-humphries1.pdf", + "authors": "Ronald Brown and Stephen P. Humphries", + "title": "Orbits under symplectic transvections", + "usage": "Classical theory credit; no external theorem required in the proof." + } + ] +} diff --git a/research/partial-pauli-two-transvection/TASK.json b/research/partial-pauli-two-transvection/TASK.json new file mode 100644 index 0000000000..b1bced553c --- /dev/null +++ b/research/partial-pauli-two-transvection/TASK.json @@ -0,0 +1,136 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "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": "Exact zero/one/two symplectic-transvection completion criterion for arbitrary compatible partial signed-Pauli contracts, with a sharp nonsingular alternating rank-two three-turn boundary.", + "scope_change_reason": "The assignment requests original successor mathematics rather than an audit or a proof-assistant campaign. JoyboyBrian PR5051 supplies the partial signed-contract setting and leaves cost optimization open. This proves a new scoped turn-length decision; it does not equate turn length with native Gaussian rank.", + "bottleneck_link": "Algebraic side result: replace a general completion upper bound with an exact low-length test before constructing a native caller. Any actual paid-rank or supplier benefit still needs a separately priced physical program.", + "budget_minutes": 60, + "stop_rule": "Stop after the first proved low-length criterion and finite independent word check; do not optimize unresolved longer-word cases or launch a native search.", + "outcome": "completed", + "evidence": "PROOF.md; standalone verify.py compares every partial isometry in dimensions 0,2,4 with independent literal word minima and checks all supplied attaining words and independent sign choices.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Determine exact minimum length for the singular rank-two residual-form cases excluded at the two-turn cutoff.", + "why_it_matters": "A lower bound of three does not say whether a physical candidate has a short attaining word.", + "first_step": "Separate the zero and rank-one residual forms with explicit fixed source spaces before deriving a dimension-uniform construction.", + "blocked_by": "The residual space may need to grow beyond D; the present criterion gives no optimal larger completion." + }, + { + "question": "Optimize the actual native Gaussian rank and full physical cost under one specified partial signed contract.", + "why_it_matters": "Transvection count alone does not price recursive calls or imply a kappa improvement.", + "first_step": "Choose a literal source caller, retain its phase anchor and dirty-owner endpoints, and evaluate each complete candidate with the native compiler tariff.", + "blocked_by": "A named caller, profitable complete invoice, routing, precision, storage and stock are not supplied." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19141408", + "upstream_checkpoint": { + "commit": "d809e986a1b1b45aae167ce83e85b989e5174e97", + "priority_revision": 7, + "checked_utc": "2026-10-23T08:21:43.743803+00:00", + "decision": "Retain scientific base 4c0a359d88f22f05189d51f48387750b801a45d4. Governing guidance and selected record unchanged; PR5051 is now merged and still leaves optimization open. No scientific source input changed." + }, + "preserved_checkout": { + "branch": null, + "state": "detached HEAD; no earlier branch attached", + "commit": "4c0a359d88f22f05189d51f48387750b801a45d4", + "preceding_commits": [ + "9deaf5cf4420605d45b087f2fc40e689e17a2f21", + "5948b8770d5f6df94d70a9f8ec6c0759586f592c", + "e30cfa384f7e48581f9e5a5cb036b1ee7a3b46a9" + ] + }, + "overlap": { + "checked_utc": "2026-10-23T08:08:55Z", + "open_pr_bodies": 329, + "discussion_records": 4190, + "remote_pagination_complete": true, + "local_notes_materialized": 129, + "tracked_notes": 6760, + "limitations": "Sparse local notes, arbitrary code diffs and unpublished work are not exhaustively searched. Main README and merged-PR distinctive-term searches supplement the cached scan. Own recent GL subspace and chart-neighborhood packages concern different objects, not this pointwise partial Pauli contract." + }, + "final_overlap": { + "checked_utc": "2026-10-23T08:22:40Z", + "open_pr_bodies": 302, + "discussion_records": 4198, + "remote_pagination_complete": true, + "local_notes_materialized": 131, + "tracked_notes": 6760, + "result": "Matches were the immediate predecessor, this contribution and unrelated older Pauli usage; main README and three merged-PR searches found no delivered cutoff. This is bounded text coverage, not a novelty certificate." + } +} diff --git a/research/partial-pauli-two-transvection/VERIFY.json b/research/partial-pauli-two-transvection/VERIFY.json new file mode 100644 index 0000000000..4a6cb95d86 --- /dev/null +++ b/research/partial-pauli-two-transvection/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "-X", + "dev", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Independent literal symplectic matrices and complete transvection Cayley minima; every partial restriction; signed attaining lifts; invalid inputs and singular/alternating boundary controls." + }, + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "-X", + "dev", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Independent literal symplectic matrices and complete transvection Cayley minima; every partial restriction; signed attaining lifts; invalid inputs and singular/alternating boundary controls." + } + ] +} diff --git a/research/partial-pauli-two-transvection/algebra.py b/research/partial-pauli-two-transvection/algebra.py new file mode 100644 index 0000000000..c5656b088f --- /dev/null +++ b/research/partial-pauli-two-transvection/algebra.py @@ -0,0 +1,144 @@ +"""Low-length binary symplectic extensions, with bounded executable inputs.""" + +def require(condition: bool, message: str) -> None: + if not condition: + raise ValueError(message) + + +def omega(v: int, w: int, n: int) -> int: + mask = (1 << n) - 1 + return (((v & mask) & (w >> n)).bit_count() + + ((v >> n) & (w & mask)).bit_count()) & 1 + + +def span(basis: tuple[int, ...]) -> set[int]: + require(len(basis) <= 18, "span capacity exceeded") + result = {0} + for vector in basis: + result |= {x ^ vector for x in tuple(result)} + return result + + +def turn_word(v: int, axes: tuple[int, ...], n: int) -> int: + for axis in axes: + if omega(v, axis, n): + v ^= axis + return v + + +def validate(n: int, source: tuple[int, ...], target: tuple[int, ...]) -> None: + require(type(n) is int and 0 <= n <= 9, "expected integer 0 <= n <= 9") + require(type(source) is tuple and type(target) is tuple, "expected tuples") + require(len(source) == len(target) <= 2 * n, "invalid basis lengths") + for basis in (source, target): + require(all(type(v) is int and 0 < v < 1 << (2 * n) for v in basis), + "invalid nonzero binary vector") + require(len(span(basis)) == 1 << len(basis), "dependent basis") + for v, image_v in zip(source, target): + for w, image_w in zip(source, target): + require(omega(v, w, n) == omega(image_v, image_w, n), + "map does not preserve the symplectic form") + + +def solve_pairings(n: int, vectors: tuple[int, ...], values: tuple[int, ...]) -> int: + """Solve omega(vectors[j], answer) = values[j] by binary elimination.""" + require(len(vectors) == len(values) <= 19, "linear-system capacity exceeded") + pivots: dict[int, tuple[int, int]] = {} + mask = (1 << n) - 1 + for vector, value in zip(vectors, values): + row = ((vector & mask) << n) | (vector >> n) + rhs = value + for column in range(2 * n): + if (row >> column) & 1: + if column not in pivots: + pivots[column] = (row, rhs) + break + old_row, old_rhs = pivots[column] + row ^= old_row + rhs ^= old_rhs + else: + require(rhs == 0, "inconsistent pairing system") + answer = 0 + for column in range(2 * n - 1, -1, -1): + if column in pivots: + row, rhs = pivots[column] + if ((row & answer).bit_count() & 1) != rhs: + answer |= 1 << column + return answer + + +class Decision: + __slots__ = ("residual_rank", "residual_form", "minimum", "lower_bound", "axes") + + def __init__(self, residual_rank: int, residual_form: tuple[tuple[int, ...], ...], + minimum: int | None, lower_bound: int, axes: tuple[int, ...] | None): + self.residual_rank = residual_rank + self.residual_form = residual_form + self.minimum = minimum + self.lower_bound = lower_bound + self.axes = axes + + +def displacement_data(n: int, source: tuple[int, ...], target: tuple[int, ...] + ) -> tuple[tuple[int, ...], tuple[tuple[int, ...], ...]]: + images: tuple[int, ...] = () + preimages: tuple[int, ...] = () + for v, w in zip(source, target): + if (v ^ w) not in span(images): + images += (v ^ w,) + preimages += (v,) + form = tuple(tuple(omega(v, d, n) for d in images) for v in preimages) + return images, form + + +def two_axes(images: tuple[int, ...], form: tuple[tuple[int, ...], ...] + ) -> tuple[int, int]: + """Diagonalize a nonsingular nonalternating two-dimensional residual form.""" + vectors = (images[0], images[1], images[0] ^ images[1]) + coordinates = ((1, 0), (0, 1), (1, 1)) + for i, left in enumerate(coordinates): + norm = sum(left[j] * form[j][k] * left[k] + for j in range(2) for k in range(2)) & 1 + if norm: + for h, right in enumerate(coordinates): + pairing = sum(right[j] * form[j][k] * left[k] + for j in range(2) for k in range(2)) & 1 + if h != i and pairing == 0: + return vectors[i], vectors[h] + raise ValueError("no triangular residual basis") + + +def low_length(n: int, source: tuple[int, ...], target: tuple[int, ...]) -> Decision: + """Decide length <= 2, and the nonsingular alternating rank-two boundary. + + minimum=None supplies only lower_bound, never infeasibility. Axes are in + execution order, followed by an optional Pauli sign correction. + """ + validate(n, source, target) + images, form = displacement_data(n, source, target) + rank = len(images) + axes: tuple[int, ...] + if rank == 0: + axes = () + elif rank == 1: + d = images[0] + if form[0][0]: + axes = (d,) + else: + values = tuple(int(v != w) for v, w in zip(source, target)) + (0,) + a = solve_pairings(n, source + (d,), values) + axes = (a, a ^ d) + elif rank == 2: + determinant = (form[0][0] * form[1][1]) ^ (form[0][1] * form[1][0]) + if determinant == 0: + return Decision(rank, form, None, 3, None) + if form[0][0] == form[1][1] == 0: + axes = (images[0], images[1], images[0] ^ images[1]) + else: + axes = two_axes(images, form) + else: + return Decision(rank, form, None, rank, None) + require(all(axis != 0 for axis in axes), "zero transvection axis") + require(all(turn_word(v, axes, n) == w for v, w in zip(source, target)), + "constructed word violates the contract") + return Decision(rank, form, len(axes), len(axes), axes) diff --git a/research/partial-pauli-two-transvection/verify.py b/research/partial-pauli-two-transvection/verify.py new file mode 100644 index 0000000000..49b4f7f50f --- /dev/null +++ b/research/partial-pauli-two-transvection/verify.py @@ -0,0 +1,202 @@ +"""Independent literal word census for the new low-length criterion.""" + +import hashlib +import itertools +import json +from pathlib import Path + +from algebra import low_length, solve_pairings + + +def check(condition: bool, message: str) -> None: + if not condition: + raise RuntimeError(message) + + +def pairing(v: int, w: int, n: int) -> int: + result = 0 + for bit in range(n): + result ^= ((v >> bit) & 1) * ((w >> (n + bit)) & 1) + result ^= ((w >> bit) & 1) * ((v >> (n + bit)) & 1) + return result + + +def action(matrix: tuple[int, ...], v: int) -> int: + answer = 0 + for bit, column in enumerate(matrix): + if (v >> bit) & 1: + answer ^= column + return answer + + +def literal_groups(n: int) -> tuple[dict[tuple[int, ...], int], int]: + check(0 <= n <= 2, "literal census capacity") + identity = tuple(1 << bit for bit in range(2 * n)) + distance = {identity: 0} + frontier = [identity] + for depth in range(1, 7): + next_frontier = [] + for matrix in frontier: + for axis in range(1, 1 << (2 * n)): + moved = tuple(v ^ (axis if pairing(v, axis, n) else 0) for v in matrix) + if moved not in distance: + distance[moved] = depth + next_frontier.append(moved) + frontier = next_frontier + check(not frontier, "Cayley search bound exhausted") + literal = set() + for columns in itertools.product(range(1 << (2 * n)), repeat=2 * n): + if all(pairing(columns[i], columns[j], n) == pairing(identity[i], identity[j], n) + for i in range(2 * n) for j in range(2 * n)): + literal.add(columns) + check(set(distance) == literal, "Cayley corpus differs from literal symplectic matrices") + return distance, len(literal) + + +def subspace_bases(n: int) -> list[tuple[int, ...]]: + spaces: dict[frozenset[int], tuple[int, ...]] = {frozenset({0}): ()} + for dimension in range(2 * n): + old_spaces = tuple(spaces.items()) + for space, basis in old_spaces: + if len(basis) != dimension: + continue + for v in range(1, 1 << (2 * n)): + if v not in space: + enlarged = frozenset(space | {x ^ v for x in space}) + if enlarged not in spaces: + spaces[enlarged] = basis + (v,) + return list(spaces.values()) + + +def signed_image(phase: int, v: int, axes: tuple[int, ...], n: int) -> tuple[int, int]: + """Conjugate i^phase X^x Z^z using the literal (I-i H_axis)/(1-i).""" + mask = (1 << n) - 1 + for axis in axes: + if pairing(v, axis, n): + exponent = ((axis & mask) & (axis >> n)).bit_count() + exponent += 2 * ((axis >> n) & (v & mask)).bit_count() + phase = (phase + exponent - 1) % 4 + v ^= axis + return phase, v + + +def signed_corrections(n: int, source: tuple[int, ...], target: tuple[int, ...], + axes: tuple[int, ...]) -> int: + mask = (1 << n) - 1 + errors = [] + for v, w in zip(source, target): + phase, image = signed_image(((v & mask) & (v >> n)).bit_count() % 4, v, axes, n) + desired = ((w & mask) & (w >> n)).bit_count() % 4 + check(image == w and (phase - desired) % 2 == 0, "non-Hermitian image") + errors.append(((phase - desired) // 2) & 1) + count = 0 + for signs in itertools.product((0, 1), repeat=len(source)): + wanted = tuple(sign ^ error for sign, error in zip(signs, errors)) + candidates = [a for a in range(1 << (2 * n)) + if all(pairing(a, w, n) == bit for w, bit in zip(target, wanted))] + check(len(candidates) == 1 << (2 * n - len(source)), "wrong sign-correction fiber") + correction = solve_pairings(n, target, wanted) + check(correction in candidates, "invalid Pauli correction") + count += 1 + return count + + +def census(n: int) -> dict[str, object]: + group, group_size = literal_groups(n) + bases = subspace_bases(n) + histogram = [0] * 7 + known = [0] * 4 + unknown = 0 + signed = 0 + digest = hashlib.sha256() + for source in bases: + restrictions: dict[tuple[int, ...], int] = {} + for matrix, cost in group.items(): + target = tuple(action(matrix, v) for v in source) + restrictions[target] = min(cost, restrictions.get(target, 7)) + for target, actual in sorted(restrictions.items()): + result = low_length(n, source, target) + histogram[actual] += 1 + check((result.minimum is not None and result.minimum <= 2) == (actual <= 2), + "incorrect zero/one/two-transvection decision") + check(result.lower_bound <= actual, "false lower bound") + if result.minimum is None: + unknown += 1 + else: + check(result.minimum == actual, "incorrect sharp length") + known[result.minimum] += 1 + check(result.axes is not None, "missing attaining word") + for v, w in zip(source, target): + for axis in result.axes: + v ^= axis if pairing(v, axis, n) else 0 + check(v == w, "literal witness failure") + signed += signed_corrections(n, source, target, result.axes) + digest.update(json.dumps([source, target, actual, result.axes]).encode()) + return {"n": n, "group": group_size, "source_subspaces": len(bases), + "contracts": sum(histogram), "length_histogram": histogram, + "sharp_lengths_supplied": known, "lower_bound_only": unknown, + "signed_basis_contracts": signed, "digest": digest.hexdigest()} + + +def controls() -> dict[str, int]: + bad = [(-1, (), ()), (True, (), ()), (10, (), ()), (1, [], ()), + (1, (1,), ()), (1, (0,), (1,)), (1, (True,), (1,)), + (1, (4,), (1,)), (2, (1, 1), (1, 2)), + (2, (1, 2), (1, 1)), (2, (1, 2), (1, 4))] + for args in bad: + try: + low_length(*args) + except ValueError: + continue + raise RuntimeError("malformed contract accepted") + first = low_length(2, (1,), (3,)) + check(first.minimum == 2 and first.residual_form == ((0,),), "singular rank-one control") + singular = low_length(2, (1, 2), (2, 3)) + check(singular.minimum is None and singular.lower_bound == 3 + and singular.residual_form == ((0, 0), (0, 0)), "singular rank-two control") + source = (1, 2, 4, 8) + target = (1, 2, 6, 9) + third = low_length(2, source, target) + check(third.minimum == 3 and third.residual_form == ((0, 1), (1, 0)), + "alternating rank-two control") + try: + solve_pairings(1, (1, 1), (0, 1)) + except ValueError: + return {"invalid_contracts": len(bad), "boundary_controls": 3, + "inconsistent_systems": 1} + raise RuntimeError("inconsistent pairing system accepted") + + +def large_examples() -> dict[str, int]: + cases = 0 + for n in range(2, 10): + e, f = 1, 2 + source = tuple(1 << bit for bit in range(2 * n)) + axes = (e, f, e ^ f) + target = tuple(signed_image(0, v, axes, n)[1] for v in source) + result = low_length(n, source, target) + check(result.minimum == 3, "all-width alternating example") + one = low_length(n, (1,), (3,)) + check(one.minimum == 2, "all-width singular rank-one example") + cases += 2 + return {"fixed_examples_n2_through_n9": cases} + + +def main() -> None: + output = {"censuses": [census(n) for n in range(3)], + "controls": controls(), "higher_dimensions": large_examples()} + package = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "algebra.py", "verify.py") + hashes = {} + for name in names: + data = (package / name).read_bytes() + check(len(data) <= 1 << 20, "package file capacity") + hashes[name] = hashlib.sha256(data).hexdigest() + output["source_sha256"] = hashes + print(json.dumps(output, sort_keys=True, indent=2)) + print("PASS_PARTIAL_PAULI_TWO_TRANSVECTION no_new_kappa") + + +if __name__ == "__main__": + main()