diff --git a/research/partial-pauli-gaussian-minimum/README.md b/research/partial-pauli-gaussian-minimum/README.md new file mode 100644 index 0000000000..e25c78371f --- /dev/null +++ b/research/partial-pauli-gaussian-minimum/README.md @@ -0,0 +1,42 @@ +# Minimum native Gaussian rank for a partial Pauli contract + +For a compatible signed partial Pauli map, this result gives the least native Gaussian rank over every symplectic completion. It answers the released [Discussion #5334](https://github.com/CrocSwap/integer-mult-bounds/discussions/5334). Compatibility and minimum quarter-turn length are different questions. The complete kappa calculation is unchanged. + +**The minimum.** Let V be a 2n-dimensional binary symplectic space. Let Z be the fixed computational Lagrangian. Let h:U -> U' be an injective partial symplectic isometry. Put A=U intersect Z, B=h(A), c=dim(B intersect Z), and t=dim(U' intersect Z intersect B-perp). Then + + min_g [dim(Z+gZ)-n] = dim(B) + t - 2c, + +where g ranges over all symplectic extensions of h. The minimum is attained. It does not depend on the compatible Pauli signs. The proof below constructs an attaining extension with linear algebra over F2. This is an offline construction; no physical preparation cost is assigned to it. + +**Transverse extension lemma.** In a symplectic space of dimension 2m, a subspace W has a disjoint Lagrangian if and only if dim W <= m. Necessity is the dimension inequality. For sufficiency, take a symplectic basis with W spanned by e_i,f_i for i<=r and e_(r+j) for j<=s. Thus dim W=2r+s<=m. Use r unused symplectic pairs indexed r+s+i. The vectors e_i+e_(r+s+i), f_i+f_(r+s+i), f_(r+j), and one e-vector for each remaining pair span a disjoint Lagrangian. Their pairings vanish in F2. Their components outside W prove disjointness. Symplectic elimination constructs this basis. + +Fix a Lagrangian R and a subspace W with dim W=w<=m. Write D=R intersect W and r0=dim D. Among Lagrangians L disjoint from W, the largest dim(L intersect R) is m-r0. The dimension bound follows because L intersect R is disjoint from D. For attainment, set N=R intersect W-perp, so dim N=m-w+r0>=r0. Choose a linear projection pi:R -> D that is the identity on D and is onto D on N. To construct it, extend a basis of D intersect N separately to D and N; send enough of the added N vectors to the remaining D basis vectors and extend to R. Set K=ker pi. Then dim K=m-r0, K intersect W=0, and K+N=R. The pairing K x W has rank w-r0. In K-perp/K, the image of W intersect K-perp has dimension r0, half the ambient dimension. Apply the transverse extension lemma there and pull its Lagrangian back. The resulting L contains K and is disjoint from W. This proves attainment without an enumeration assumption. + +**Application to the partial map.** Set b=dim B. A completion L=gZ must contain B and satisfy L intersect U'=B. Conversely these two conditions suffice. The pairing maps from Z to U-star and from L to U'-star have images equal to the annihilators of A and B. Their restrictions on A and B agree through h. Choose adapted bases for their kernels and images to extend h on A to an isomorphism Z -> L that preserves all pairings with U. Together with h this defines an isometry U+Z -> U'+L. Symplectic basis extension then extends it to V. This also gives an explicit construction. + +Pass to B-perp/B, of dimension 2m with m=n-b. Define + + W=(U' intersect B-perp)/B, + R=((Z intersect B-perp)+B)/B. + +R is Lagrangian. An admissible L/B is precisely a Lagrangian disjoint from W. In particular dim W<=m: alternatively, transfer W through h to (U intersect A-perp)/A and project into V/Z; its image lies in the (n-b)-dimensional annihilator of A. Moreover dim(R intersect W)=t-c, and dim(L intersect Z)=c+dim((L/B) intersect R). The preceding lemma gives maximum intersection c+(n-b)-(t-c), and hence the stated minimum. These quotient constructions also prove that the chosen L meets U' only in B. + +**Signed dyadic lift and phase boundary.** Complete the unsigned map as above. The fixed-prefix transvection construction in the cited source emits a literal dyadic quarter-turn word for that full symplectic map. For each prescribed Pauli generator, its sign discrepancy is a binary linear functional on U'. Compatibility of dependent signed relations is required. Nondegeneracy of the ambient symplectic form extends this functional to pairing with a Pauli correction. Append that Pauli; it fixes all requested signs and does not change gZ or the rank. Each turn uses the source convention (I-iP)/(1-i), with positive Hermitian P. The literal word chooses its absolute scalar phase. No equality to an externally supplied scalar is implied. A specified target operator requires one exact amplitude check in addition to its signed tableau. Apply the cited native compiler to this word: its one grouped rank-d Gaussian and monomial factors have the attained rank. Their preparation and scan costs remain charged obligations. + +**Exact evidence.** The standalone checker enumerates all symplectic completions and all subspaces for n=0,1,2. It groups completions by their exact partial map and compares all 10,113 minimum values with the formula. It also constructs 386 signed lifts and checks 848 literal Gaussian-rational matrix-column identities. Five controls include an inconsistent dependent Pauli sign, an absolute scalar mismatch, and the one-qubit Z-to-X, X-to-X and X-to-Z cases. The executable census is finite corroboration of the dimension-uniform constructive proof; it is not a polynomial-time implementation of the quotient construction. + +Credit JoyboyBrian's [PR #5051](https://github.com/CrocSwap/integer-mult-bounds/pull/5051) supplies the signed partial-map contract, compatibility test, fixed-prefix extension and turn convention in [pauli.py](https://github.com/CrocSwap/integer-mult-bounds/blob/0960807a68ff46acbe6510c8867912ef2324ee71/research/signed-pauli-partial-extension/pauli.py). David Ganz/Dugongue's [PR #4841](https://github.com/CrocSwap/integer-mult-bounds/pull/4841) supplies the native Gaussian rank, monomial-factor bill and absolute-phase contract in the [compiler proof](https://github.com/CrocSwap/integer-mult-bounds/blob/6debdcdac8fe1c87958f8cd42ccb7db73c0a0eef/research/native-clifford-gauge-compiler/compiler/CLIFFORD-COMPILER.md). Nick Petalas's partial-transvection work is a separate tariff predecessor, as recorded in the released handoff. Symplectic basis extension and the Clifford/Bruhat methods are classical; this result addresses minimization over the prescribed extension fiber. The checker adapts the credited source's literal turn conventions and extension steps, and independently enumerates the full small completion fibers. + +Prepared by Ali Romman with substantial OpenAI Codex assistance; Apache-2.0. + +## Reproduce + +```sh +python3 -B scripts/research_package.py --package research/partial-pauli-gaussian-minimum +``` + +Use Python 3.12 with the standard library. The normal and optimized commands must print `PASS_PARTIAL_PAULI_GAUSSIAN_MINIMUM`. The launcher must print `PASS_REGISTERED_RESEARCH_PACKAGE`. The checker has no external runtime inputs. + +## Open next questions + +Implement the quotient construction on one actual contact constraint set, retain its literal phase and charge all monomial passes. The source binding and physical cost model are not supplied by this package. See `TASK.json` for the structured scope. diff --git a/research/partial-pauli-gaussian-minimum/SOURCES.json b/research/partial-pauli-gaussian-minimum/SOURCES.json new file mode 100644 index 0000000000..277ad46954 --- /dev/null +++ b/research/partial-pauli-gaussian-minimum/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "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" + } + ] +} diff --git a/research/partial-pauli-gaussian-minimum/TASK.json b/research/partial-pauli-gaussian-minimum/TASK.json new file mode 100644 index 0000000000..0068a72b70 --- /dev/null +++ b/research/partial-pauli-gaussian-minimum/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "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": "This enabling proof gives the exact minimum native Gaussian rank over all symplectic completions of any compatible partial signed Pauli map. A dimension-uniform constructive Lagrangian argument attains the formula; a Pauli correction fixes all compatible signs without changing the rank.", + "scope_change_reason": "This is a scoped interface theorem. It does not complete the original supplier or uniform-transfer task.", + "bottleneck_link": "Implement the quotient construction on one actual contact constraint set, retain its literal phase and charge all monomial passes.", + "budget_minutes": 60, + "stop_rule": "Stop after the scoped proof, exact controls and bounded registered replay; do not expand to physical lowering.", + "outcome": "completed", + "evidence": "10,113 complete extension fibers, 386 signed lifts, 848 literal matrix-column identities and five controls", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance; no independent human or proof-kernel acceptance is claimed.", + "open_questions": [ + { + "question": "Implement the quotient construction on one actual contact constraint set, retain its literal phase and charge all monomial passes.", + "why_it_matters": "The abstract result needs an actual caller and a complete cost model.", + "first_step": "Implement the quotient construction on one actual contact constraint set, retain its literal phase and charge all monomial passes.", + "blocked_by": "No production caller or physical cost model is supplied." + } + ], + "upstream_checkpoint": { + "commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "priority_revision": 7, + "checked_at": "2026-10-23T17:53:47.708546+00:00" + }, + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19151441" +} diff --git a/research/partial-pauli-gaussian-minimum/VERIFY.json b/research/partial-pauli-gaussian-minimum/VERIFY.json new file mode 100644 index 0000000000..39e12ed106 --- /dev/null +++ b/research/partial-pauli-gaussian-minimum/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "10,113 complete extension fibers, 386 signed lifts, 848 literal matrix-column identities and five controls" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "10,113 complete extension fibers, 386 signed lifts, 848 literal matrix-column identities and five controls" + } + ] +} diff --git a/research/partial-pauli-gaussian-minimum/verify.py b/research/partial-pauli-gaussian-minimum/verify.py new file mode 100644 index 0000000000..7c1b4af0f6 --- /dev/null +++ b/research/partial-pauli-gaussian-minimum/verify.py @@ -0,0 +1,197 @@ +"""Exact completion census and literal signed Pauli controls. + +Prepared by Ali Romman with substantial OpenAI Codex assistance. Apache-2.0. +The turn, product and signed-extension conventions follow JoyboyBrian's +PR5051 pauli.py at 0960807a68ff46acbe6510c8867912ef2324ee71. +""" +from itertools import product +from fractions import Fraction as F + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def span(rows): + out = {0} + for x in rows: + out |= {v ^ x for v in out} + return out + + +def basis(values): + out, seen = [], {0} + for x in sorted(values): + if x not in seen: + out.append(x) + seen |= {v ^ x for v in seen} + return tuple(out) + + +def omega(a, b, n): + mask = (1 << n) - 1 + return (((a & mask) & (b >> n)) ^ ((b & mask) & (a >> n))).bit_count() % 2 + + +def act(columns, x): + out = 0 + for j, v in enumerate(columns): + if x >> j & 1: + out ^= v + return out + + +def symplectic(n): + out = [] + def extend(cols): + j = len(cols) + if j == 2 * n: + out.append(tuple(cols)) + return + for v in range(1, 1 << (2*n)): + if v not in span(cols) and all(omega(v,w,n)==omega(1<>n + if ((a&p[1])^(b&p[0])).bit_count()%2: + p=(p[0]^a,p[1]^b,(p[2]+(a&b).bit_count()+2*(b&p[0]).bit_count()-1)%4) + return p + + +def lift(n, columns): + current=[1<>n + pv=pauli((x,z,(x&z).bit_count()%4),v) + v=[add(mul((F(1,2),F(1,2)),a),mul((F(1,2),F(-1,2)),b)) for a,b in zip(v,pv)] + return v + + +def compatible(n, constraints): + rows=[]; selected=[] + for p,q in constraints: + value=p[0]|p[1]<>j&1:pp,qq=mulp(pp,a),mulp(qq,b) + if qq[:2]!=q[:2] or (pp[2]-p[2])%4!=(qq[2]-q[2])%4:return False + return True + + +def main(): + total=0; signed=0; columns_checked=0 + chosen=[] + for n in (0,1,2): + group=symplectic(n); subs=spaces(n); cases={} + for g in group: + d=len(basis([v & ((1<>n,((x&mask)&(x>>n)).bit_count()%4) for x in u] + dst=[(y&mask,y>>n,(((y&mask)&(y>>n)).bit_count()+2*(signs>>j&1))%4) for j,y in enumerate(t)] + rhs=[((q[2]-apply(p,gates,n)[2])%4)//2 for p,q in zip(src,dst)] + corrections=[v for v in range(1<<(2*n)) if all(omega(v,y,n)==r for y,r in zip(t,rhs))] + need(bool(corrections),'signed correction exists') + corr=corrections[0] + for p,q in zip(src,dst): + a=apply(p,gates,n); a=(a[0],a[1],(a[2]+2*omega(corr,a[0]|a[1]<