diff --git a/research/signed-pauli-partial-extension/PROOF.md b/research/signed-pauli-partial-extension/PROOF.md new file mode 100644 index 0000000000..ddc78a2d59 --- /dev/null +++ b/research/signed-pauli-partial-extension/PROOF.md @@ -0,0 +1,151 @@ +# Completing a partial signed-Pauli native contract + +Prepared for JoyboyBrian with substantial OpenAI Codex assistance; Apache-2.0. +This is a written proof with finite exact corroboration, not proof-kernel review. + +Use bare Paulis P=i^p X^x Z^z on n binary axes. Labels v=(x,z) lie in +V=F_2^(2n), with omega(v,w)=x·w_z+z·w_x. A Pauli is Hermitian exactly +when p≡x·z (mod2). We allow dependent equations and ±I constraints. +Given Hermitian equations U P_i U^-1=Q_i, put W=span(v_i), k=dim W, +rank(omega|W)=2r, and t=k−2r. Count Cliffords modulo arbitrary scalar phase; +this is the finite projective Clifford group, not a count of physical headers. + +## The complete compatibility theorem + +The equations have a Clifford solution if and only if: + +1. The ordered source and target labels have exactly the same binary relations, + so v_i↦w_i defines an injective linear map h:W→V. +2. omega(v_i,v_j)=omega(w_i,w_j) for every pair. +3. Every central product relation has the same actual i-phase. Equivalently, + choose any independent source sublist. For each remaining equation, express + its label as a sum of this basis; multiply the corresponding Hermitian + generators in that fixed order, and compare the central scalar between + this product and the equation's Pauli. The scalar must agree on both sides. + +These conditions preserve all Pauli multiplication relations, not only signs +on a chosen independent basis. They are necessary under conjugation. For the +equivalence in item3, the presentation of the Pauli group generated by the +chosen basis consists of its central i, generator squares, and pairwise +commutators. Squares are fixed because every supplied generator is Hermitian; +item2 fixes commutators. Every other source generator is a uniquely specified +central multiple of the fixed ordered product. Thus checking these finitely +many relations suffices for every word relation. No exponential enumeration +of generator relations is needed. + +## Constructive symplectic extension + +Here is a direct binary proof of the required special case of Witt extension. +Process independent source labels v_1,…,v_k in order, maintaining a symplectic +map S which is already correct on earlier labels. Let v=S(v_j), w=h(v_j), +and let P be the span of earlier target labels. Then v,w are outside P and +omega(v,p)=omega(w,p) for every p in P. If v=w nothing is required. +Otherwise v+w∈P-perp. If omega(v,w)=1, the transvection + + T_(v+w)(a)=a+omega(a,v+w)(v+w) + +fixes P pointwise and sends v to w. If omega(v,w)=0, choose u satisfying + + omega(u,p)=omega(v,p) for p in P, + omega(u,v)=omega(u,w)=1. + +This binary linear system is consistent. A relation among a basis of P,v,w +cannot involve just one of v,w, since each is outside P. The only possible +new relation has v+w=p in P; the prescribed right-hand side for p is +omega(v,v+w)=omega(v,w)=0, equal to 1+1. Nondegeneracy of omega then makes +every consistent functional representable by a vector u. The two axes v+u +and u+w belong to P-perp. Their transvections fix P and send v→u→w. +Thus at most 2k explicit transvections construct a full symplectic extension. +Gaussian elimination solves the displayed systems; no ambient vector search +or unproved isometry oracle is used. + +For a nonzero axis a=(a_x,a_z), let H_a=i^(popcount(a_x&a_z)) X^a_x Z^a_z. +It is Hermitian and squares to I. The literal dyadic Clifford + + C_a=(I−i H_a)/(1−i) + +implements T_a and is exactly the source compiler's positive `turn` gate. +If P anticommutes with H_a, C_a P C_a^-1=−i H_a P; otherwise P is fixed. +This proves the phase update used by the implementation, including Y axes. +The product of these literal gates gives a chosen Clifford U0 extending h +on labels. Its Hermitian images may still have wrong signs. By conditions2–3, +the difference between desired and actual signs is a binary linear functional +on h(W). Nondegeneracy gives a Pauli K whose conjugation supplies precisely +this character. Solve omega(K,w_j)=delta_j, then append literal X and Z +gates. Their global phase is part of the emitted word; it is not discarded. +This constructs a solution of every signed equation and proves sufficiency. + +## Exact projective completion count + +First count symplectic extensions of the fixed h. Choose a nondegenerate +2r-dimensional summand H of W; W=H direct-sum R with R=rad(W), dim R=t. +The pointwise stabilizer of H acts as Sp_(2N)(2) on H-perp, N=n−r. Fixing W +further means fixing an ordered basis of the isotropic t-space R. There are + + I(N,t)=product_(j=0)^(t−1)(2^(2N−j)−2^j) + +ordered independent isotropic t-tuples: after j choices the next vector is in +their orthogonal complement of dimension2N−j but outside their 2^j-element +span. The constructive extension argument above implies transitivity on such +tuples. Since |Sp_(2N)(2)|=2^(N^2) product_(j=1)^N(2^(2j)−1), orbit-stabilizer +gives |Sp_(2N)(2)|/I(N,t) symplectic extensions of h. The same group-order +formula follows by choosing a first nonzero symplectic basis vector, a partner +of pairing one, and recursing on their orthogonal complement. + +Over each full symplectic map, projective Clifford lifts form a torsor for +the 2^(2n) Pauli conjugations. This can be seen without counting matrices: +two lifts differ by signs on the 2n standard Hermitian generators, every such +sign character is implemented by a unique Pauli label, and a map fixing all +signed generators commutes with X and Z and hence is scalar. The k independent +specified signs impose k independent linear equations. Thus the number is + + 2^(2n−k) |Sp_(2(n−r))(2)| / I(n−r,t). (1) + +All compatible choices have this same count; incompatible input has count zero. +The formula includes k=0, the full signed tableau k=2n, and n=0. No unused +workspace or discarded input is introduced by the construction. + +## A real phase obstruction and the absolute-phase boundary + +For one qubit, X→X, Z→Z, Y→−Y preserves all label relations and pairwise +commutators, but X Z Y=−iI would become+iI. It has zero completions. X fixed +alone has four projective completions; X and Z fixed have one. + +Partial conjugation equations, even a full signed tableau, never specify the +global scalar of U. In particular I and −I satisfy exactly the same equations. +The API emits an actual chosen literal dyadic word. It does NOT assert that +this word equals an independently supplied physical target. Such equality +still requires the source compiler's exact nonzero amplitude anchor. Both this +distinction and the i^(phase*f) law at tensor width f are explicit controls. + +Every emitted base word is tensorized letter by letter. Functoriality proves +U^tensor(f) P_i^tensor(f) (U^-1)^tensor(f)=Q_i^tensor(f) for all positive f. +Source global phases tensorize too. Tensorizing an entire sum or dropping an +anchor phase is not authorized by this argument. + +## Actual caller and complete obligation ledger + +The pinned native Clifford compiler (#4841, Dugongue and its retained source +lineage) accepts a full literal gate word or an unsigned Lagrangian and emits +phase-exact free adapters around one rank-d Gaussian call. This package adds +the missing entry contract from incomplete signed operator constraints. Its +emitted literal words are passed to the actual source CLI, retaining full +small-input column checks and nine-bit tableau/anchor replay. The existing +compiler is a declared source dependency, not a theorem independently audited +in full by this contribution. Classical Witt and Clifford structure retain +their attribution; no mathematical or synthesis-priority claim is made. + +| Obligation | Status | +|---|---| +| All-size signed compatibility, construction and count | Written proof above; finite exact corroboration | +| Literal emitted dyadic gates, no clean ancilla | Constructively specified; source CLI bound | +| One rank-d lowering and free-adapter bill | Inherited conditional compiler, d≤n only | +| Minimum paid rank among completions | Unknown; no optimization claim | +| Chosen word's phase and literal tensor semantics | Retained explicitly | +| Equality to a supplied absolute-phase target | Unknown without its separate amplitude anchor | +| Actual profitable changed word, owner endpoints and complete invoice | Unknown | +| Precision, stock, fixed-tape, outer and supplier admission | Unknown | + +The reference implementation is bounded to n≤9 for the source calibration; +the proof and count are for arbitrary n. No complete multiplication theorem, +selected-frontier change or new κ is claimed. Stop at this conditional entry API. diff --git a/research/signed-pauli-partial-extension/README.md b/research/signed-pauli-partial-extension/README.md new file mode 100644 index 0000000000..b7f3c12b91 --- /dev/null +++ b/research/signed-pauli-partial-extension/README.md @@ -0,0 +1,125 @@ +# Complete partial signed-Pauli native contracts + +A set of partial native-chart conjugation constraints can match all binary +labels and commutators and still be impossible because its exact central +Pauli relations disagree. This package gives the complete all-size criterion,+a constructive literal dyadic Clifford word, and the exact number of +**projective** Clifford completions. It does not infer an absolute-phase target +from conjugation data. + +For Hermitian equations `U P_i U^-1 = Q_i`, compatibility means equal label +relation spaces, matching symplectic pairings, and equal actual central phases +in all generator relations. [PROOF.md](PROOF.md) reduces the latter check to a +basis and proves sufficiency using at most two transvections per independent +label followed by a Pauli sign correction. It constructs actual source `turn`, +`x` and `s` gates, with no clean ancilla or discarded data. A one-qubit example +`X→X, Z→Z, Y→−Y` passes the unsigned tests but fails because `X Z Y=−iI`. + +If the label span has dimension `k=2r+t`, symplectic rank `2r` and radical +dimension `t`, the compatible count is + +``` +2^(2n-k) |Sp_(2(n-r))(2)| / + product_(j=0)^(t-1)(2^(2(n-r)-j)-2^j). +``` + +The theorem covers every nonnegative n. The reference implementation is +explicitly bounded to `n≤9` for native-source calibration. This is a scoped +written proof with finite exact corroboration, prepared for **JoyboyBrian** +with substantial OpenAI Codex assistance. Classical Witt, symplectic and +Clifford structure retain credit; no literature-priority, independent human +or proof-kernel acceptance is claimed. + +[Canonical claim and status](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19140242). + +## Actual caller and phase contract + +Dugongue's retained native Clifford compiler (#4841) accepts a full literal +word or an unsigned Lagrangian, then emits phase-exact free adapters around +one rank-d Gaussian call. This supplies its missing entry contract from +incomplete signed operator constraints. Every live dependency is pinned at +main `f259dabc7d70e0db8d6d36bfda888f008bbfecc1` in +[SOURCES.json](SOURCES.json). Source files remain unchanged; the original NOTICE.md and LICENSE are also +exported byte for byte with their full predecessor attribution. + +The checker authenticates the source before loading that exact file with +`runpy.run_path`, which reads source bytes directly rather than an imported +bytecode cache. It calls the actual `tableau`, `compile_word`, `replay`, `state` +and `lift_word` functions on eleven newly completed words. Nine small cases +have all input columns checked; the additional three-bit case has eight +columns, and the nine-bit case has the complete signed tableau plus its exact +zero-state column checked by the source compiler. These are focused calls, +not a replay of the predecessor's complete historical suite. + +`I` and `−I` have the same signed tableau. The API chooses one literal word; +it does not promise equality to a separately supplied word with that tableau. +The source's actual negative-identity word and exact amplitude anchor witness +this distinction. Tensor controls retain global phase `i^(a*f)`, and the +all-width conclusion tensorizes each base letter separately. No sum is +silently tensorized as one letter. + +## Independent finite evidence + +The separate literal oracle builds full Pauli monomial matrices and computes +conjugations by matrix composition, independently of the implementation's +phase formula. Complete closures give all 24 one-qubit and 11,520 two-qubit +projective signed Clifford tableaus. For a canonical representative of every +possible source-span symplectic type, it compares **every distinct target +restriction** and its realization multiplicity: + +| n | Source index sets | Distinct restrictions | +|---|---|---:| +| 1 | empty; X1; X1,Z1 | 31 | +| 2 | empty; X1; X1,X2; X1,Z1; X1,Z1,X2; full | 15,271 | + +All **15,302** returned words are independently evaluated gate by gate by the +literal oracle, not merely tested for membership in a full group. Five semantic +rejections, five malformed-input rejections, scalar/zero-dimensional controls, +the negative-identity anchor and widths-two/three global-phase controls are +recorded in [RESULT.json](RESULT.json). This is the precise bounded coverage; +it is not enumeration of arbitrary-dimensional input constraints. + +## Reproduce + +Use Python 3.12 and its standard library: + +```sh +python3.12 -W error -B scripts/research_package.py --package research/signed-pauli-partial-extension +python3.12 -W error -B scripts/check_research_commit.py --package research/signed-pauli-partial-extension --check-source-history +``` + +The registered hook runs normal and optimized Python. Direct `verify.py` +works in an official committed export without Git or network access. It reads +the deterministic type-sensitive receipt and never modifies it. To generate a +fresh receipt use `verify.py --write /a/new/file.json`; an occupied path fails. +The receipt authenticates local proof/code/metadata and live source bytes. +Python managed allocation and arbitrary-precision arithmetic are diagnostic +software, not physical constant-time operations. + +## Full ledger and stopping decision + +The uniform compatibility, construction and projective count are proved in +the written argument. The literal gates and phase boundary are constructively +specified and bound to the source compiler. One rank-d lowering is an inherited +conditional compiler statement; the constructed word gives `d≤n`, not an +optimal paid-rank theorem. A profitable changed consumer, all owner endpoints, +physical movement, precision, stock, source-uniform funding and outer supplier +admission remain unknown. The selected κ stays 0.00302015. + +The decision is **narrow**: stop at this complete partial operator entry API. + +## Open next questions + +1. Minimize paid rank among compatible completions. First specify actual + partial operator constraints from a changed chronological caller and its + complete allowance. The present existence/count theorem does not optimize + Fourier rank or prove a net paid saving. +2. Match a supplied absolute-phase target. First provide its exact nonzero + amplitude anchor; a full signed tableau still leaves its scalar free. +3. Bind one useful completion into a whole owner-typed caller, retaining + frozen endpoints and every incident transition. Missing physical costs, + precision and stock block any supplier or κ conclusion. + +Credit Dugongue for #4841's native compiler and explicit phase/anchor contract; +Cao Yifan / intqwq #4610, Cinna Davis, zxv, Jacob Alan Sussman, the retained +Clifford/native/owner/compiler lineage and Bravyi–Maslov normal-form background. +Source notices remain intact; new material is Apache-2.0. diff --git a/research/signed-pauli-partial-extension/RESULT.json b/research/signed-pauli-partial-extension/RESULT.json new file mode 100644 index 0000000000..c584987762 --- /dev/null +++ b/research/signed-pauli-partial-extension/RESULT.json @@ -0,0 +1,414 @@ +{ + "absolute_phase": { + "identity_tableau_negative_anchor_rejected": true, + "literal_global_phase_tensor_widths": [ + 2, + 3 + ] + }, + "actual_compiler": [ + { + "n": 1, + "paid_rank": 0, + "source_replay_columns": 2, + "word": [] + }, + { + "n": 1, + "paid_rank": 0, + "source_replay_columns": 2, + "word": [] + }, + { + "n": 1, + "paid_rank": 0, + "source_replay_columns": 2, + "word": [] + }, + { + "n": 2, + "paid_rank": 0, + "source_replay_columns": 4, + "word": [] + }, + { + "n": 2, + "paid_rank": 0, + "source_replay_columns": 4, + "word": [ + [ + "turn", + 1, + 1, + 1 + ], + [ + "turn", + 1, + 3, + 1 + ], + [ + "s", + 1, + 2 + ] + ] + }, + { + "n": 2, + "paid_rank": 1, + "source_replay_columns": 4, + "word": [ + [ + "turn", + 1, + 1, + 1 + ], + [ + "turn", + 1, + 3, + 1 + ], + [ + "turn", + 3, + 1, + 1 + ], + [ + "s", + 1, + 2 + ] + ] + }, + { + "n": 2, + "paid_rank": 0, + "source_replay_columns": 4, + "word": [ + [ + "turn", + 1, + 1, + 1 + ], + [ + "turn", + 1, + 3, + 1 + ], + [ + "turn", + 1, + 2, + 1 + ], + [ + "turn", + 1, + 0, + 1 + ], + [ + "s", + 1, + 2 + ] + ] + }, + { + "n": 2, + "paid_rank": 1, + "source_replay_columns": 4, + "word": [ + [ + "turn", + 1, + 1, + 1 + ], + [ + "turn", + 1, + 3, + 1 + ], + [ + "turn", + 1, + 2, + 1 + ], + [ + "turn", + 1, + 0, + 1 + ], + [ + "turn", + 2, + 1, + 1 + ], + [ + "s", + 1, + 2 + ] + ] + }, + { + "n": 2, + "paid_rank": 1, + "source_replay_columns": 4, + "word": [ + [ + "turn", + 1, + 1, + 1 + ], + [ + "turn", + 1, + 3, + 1 + ], + [ + "turn", + 3, + 1, + 1 + ], + [ + "turn", + 1, + 2, + 1 + ], + [ + "turn", + 1, + 0, + 1 + ], + [ + "turn", + 0, + 2, + 1 + ], + [ + "s", + 1, + 2 + ] + ] + }, + { + "n": 3, + "paid_rank": 2, + "source_replay_columns": 8, + "word": [ + [ + "turn", + 3, + 3, + 1 + ], + [ + "turn", + 5, + 7, + 1 + ], + [ + "x", + 2 + ], + [ + "s", + 2, + 2 + ] + ] + }, + { + "n": 9, + "paid_rank": 4, + "source_replay_columns": 1, + "word": [ + [ + "turn", + 1, + 1, + 1 + ], + [ + "turn", + 97, + 63, + 1 + ], + [ + "turn", + 106, + 82, + 1 + ], + [ + "turn", + 7, + 43, + 1 + ], + [ + "s", + 8, + 2 + ] + ] + } + ], + "complete_supplier": false, + "controls": { + "full_signed_tableau_count": 1, + "malformed_rejections": 5, + "one_fixed_generator_count": 4, + "semantic_rejections": 5, + "zero_dimensional_count": 1 + }, + "count_contract": "projective Clifford; literal representative chooses its own phase", + "finite_domains": [ + { + "n": 1, + "projective_group": 24, + "types": [ + { + "group_order": 24, + "indices": [], + "literal_word_checks": 1, + "maximum_literal_gates": 0, + "restrictions": 1, + "sha256": "e6ce053854cbb609f1e920745a2b16e313b6e138f6adf02f01d536e109cb06d8" + }, + { + "group_order": 24, + "indices": [ + 0 + ], + "literal_word_checks": 6, + "maximum_literal_gates": 2, + "restrictions": 6, + "sha256": "ea69f8b859c8fd14e7c3e31afd0940aa95602f404ac535d47265176f6679ba43" + }, + { + "group_order": 24, + "indices": [ + 0, + 1 + ], + "literal_word_checks": 24, + "maximum_literal_gates": 4, + "restrictions": 24, + "sha256": "a61f588d7c4ddaba264016dd7aa9b71d160549023ea6fa9e82459fd5a93fab63" + } + ] + }, + { + "n": 2, + "projective_group": 11520, + "types": [ + { + "group_order": 11520, + "indices": [], + "literal_word_checks": 1, + "maximum_literal_gates": 0, + "restrictions": 1, + "sha256": "04f539bc6b0669ad86e1e8a446fd46fd271d7371ca79318d78bcaf0192ec4392" + }, + { + "group_order": 11520, + "indices": [ + 0 + ], + "literal_word_checks": 30, + "maximum_literal_gates": 3, + "restrictions": 30, + "sha256": "65381e0c0fe10a56f2f20d9c6d49facfe6312603e03bb832e31e8cb1517ece86" + }, + { + "group_order": 11520, + "indices": [ + 0, + 1 + ], + "literal_word_checks": 360, + "maximum_literal_gates": 5, + "restrictions": 360, + "sha256": "5f849c1c84b5daea8c0cb8ddc2a1e958cd359170007dc31bc9687e6155d86dd5" + }, + { + "group_order": 11520, + "indices": [ + 0, + 2 + ], + "literal_word_checks": 480, + "maximum_literal_gates": 6, + "restrictions": 480, + "sha256": "6abcb6339ae7491171740429fc464dffe054990a0020b7dd2ab9b6569e568b08" + }, + { + "group_order": 11520, + "indices": [ + 0, + 2, + 1 + ], + "literal_word_checks": 2880, + "maximum_literal_gates": 7, + "restrictions": 2880, + "sha256": "9008f1d7562d96edbb551805d50bfdb0a45fc86d07fed293b8aac2e8c061360a" + }, + { + "group_order": 11520, + "indices": [ + 0, + 1, + 2, + 3 + ], + "literal_word_checks": 11520, + "maximum_literal_gates": 9, + "restrictions": 11520, + "sha256": "d0372c0fb742e0105d6b4e393d7a223bdb7d5f6869014c16f72608e9b7409e19" + } + ] + } + ], + "local_sha256": { + "PROOF.md": "00b495bbf278a98ded6aef6bee7938b821f9b1effcb58d60a19a4706203265ea", + "README.md": "8bde3fc092ef164f974d63350df97b95bcab3d490d71bc3d9100baaaf9693666", + "SOURCES.json": "e4da1be576b6c3966fffd57a211318cf687e3e77382996a789cb7be197f6c4d5", + "TASK.json": "f202d87428e7e5ca12e63f0423c5019cce8e85a0c87a6243b46296987a46de71", + "VERIFY.json": "8c0e0a7e1e260698affd61a4ab70df00a99264829cc809d39826340d910b5342", + "pauli.py": "8d3d9706a53ba43725c75da7d0f58b777939a194626449fd1934581c0b59074e", + "verify.py": "e5d72f8bf02f87e966b5e9676917420b6438a877c20cfd34e01d7b39a12f086a" + }, + "new_kappa": false, + "schema_version": 1, + "sources": { + "research/native-clifford-gauge-compiler/LICENSE": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "research/native-clifford-gauge-compiler/NOTICE.md": "ea459c3cae30546924cc4d3521eca3d982db19d34ae37cb04d0651909df1081e", + "research/native-clifford-gauge-compiler/compiler/CLIFFORD-COMPILER.md": "415ed8b4a87e9b48e08a25db06483501a3457aeb2fb9269fe754b52570c9eec3", + "research/native-clifford-gauge-compiler/compiler/clifford_compile.py": "a1cea1f165e7504a54607ea9d7e1d68c09dfd5533e3a958f8825d68800ddc80f", + "research/native-clifford-gauge-compiler/decoder/CROSS-REVIEW-DYNAMIC.md": "5025c3af4fa6f8e9b13c4a0a41eed2e3ae9fdd55767136d048c38c673508e191" + } +} diff --git a/research/signed-pauli-partial-extension/SOURCES.json b/research/signed-pauli-partial-extension/SOURCES.json new file mode 100644 index 0000000000..2583fc8156 --- /dev/null +++ b/research/signed-pauli-partial-extension/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1", + "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" + }, + { + "path": "research/native-clifford-gauge-compiler/compiler/CLIFFORD-COMPILER.md", + "usage": "input", + "git_blob": "8352a565c7eedd3d2567a92f077f29b6fff33e5c", + "sha256": "415ed8b4a87e9b48e08a25db06483501a3457aeb2fb9269fe754b52570c9eec3" + }, + { + "path": "research/native-clifford-gauge-compiler/compiler/clifford_compile.py", + "usage": "input", + "git_blob": "63cd255ab30c86739675a9306618f05ba2f0ebe0", + "sha256": "a1cea1f165e7504a54607ea9d7e1d68c09dfd5533e3a958f8825d68800ddc80f" + }, + { + "path": "research/native-clifford-gauge-compiler/decoder/CROSS-REVIEW-DYNAMIC.md", + "usage": "input", + "git_blob": "08fe0e1535ff08f8ee4f37e8ef1f1e6ac2e270a1", + "sha256": "5025c3af4fa6f8e9b13c4a0a41eed2e3ae9fdd55767136d048c38c673508e191" + }, + { + "path": "research/native-clifford-gauge-compiler/NOTICE.md", + "usage": "input", + "git_blob": "5519958ecf6200f04b63a4783f805394c717b915", + "sha256": "ea459c3cae30546924cc4d3521eca3d982db19d34ae37cb04d0651909df1081e" + }, + { + "path": "research/native-clifford-gauge-compiler/LICENSE", + "usage": "input", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + } + ] +} diff --git a/research/signed-pauli-partial-extension/TASK.json b/research/signed-pauli-partial-extension/TASK.json new file mode 100644 index 0000000000..678f9d53eb --- /dev/null +++ b/research/signed-pauli-partial-extension/TASK.json @@ -0,0 +1,107 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1", + "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": "Complete partial signed-Pauli conjugation contracts with constructive literal dyadic Clifford extension and exact projective completion counts.", + "scope_change_reason": "Replace the generic formal/compact-switch card with an uncovered actual native compiler entry contract. This is symplectic signed operator data, distinct from coordinate-GL subspace extension and existing complete tableau/anchor verification.", + "bottleneck_link": "Reject phase-inconsistent partial native charts and construct actual literal completions before the native one-call compiler boundary.", + "budget_minutes": 60, + "stop_rule": "Stop after the all-size compatibility/count proof, literal construction and focused source-bound corroboration; no paid-rank optimization or downstream native campaign.", + "outcome": "partial", + "evidence": "PROOF.md, pauli.py, verify.py and RESULT.json", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance; independent automated parent review requested. No independent human or proof-kernel acceptance.", + "open_questions": [ + { + "question": "Minimize paid Fourier rank over compatible completions.", + "why_it_matters": "Existence does not show a useful paid invoice.", + "first_step": "Specify one actual changed caller and complete cost allowance.", + "blocked_by": "Concrete partial constraints and every incident paid transition." + }, + { + "question": "Match a supplied absolute-phase target.", + "why_it_matters": "Conjugation equations leave the global scalar undetermined.", + "first_step": "Supply an exact nonzero amplitude anchor and compare it with the chosen literal word.", + "blocked_by": "Independent target anchor." + }, + { + "question": "Install one completion in a complete owner-typed caller.", + "why_it_matters": "A local algebraic completion is not a supplier.", + "first_step": "Bind frozen endpoints, dirty returns and chronological operators.", + "blocked_by": "Physical movement, precision, stock and outer admission." + } + ] +} diff --git a/research/signed-pauli-partial-extension/VERIFY.json b/research/signed-pauli-partial-extension/VERIFY.json new file mode 100644 index 0000000000..fa1a8ecb5c --- /dev/null +++ b/research/signed-pauli-partial-extension/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/native-clifford-gauge-compiler/compiler/CLIFFORD-COMPILER.md", + "research/native-clifford-gauge-compiler/compiler/clifford_compile.py", + "research/native-clifford-gauge-compiler/decoder/CROSS-REVIEW-DYNAMIC.md", + "research/native-clifford-gauge-compiler/NOTICE.md", + "research/native-clifford-gauge-compiler/LICENSE" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete small projective groups, every partial symplectic type, independent literal emitted words and actual source compiler/phase/tensor bindings." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same independent counts, type-sensitive receipt and source/phase controls under optimized Python." + } + ] +} diff --git a/research/signed-pauli-partial-extension/pauli.py b/research/signed-pauli-partial-extension/pauli.py new file mode 100644 index 0000000000..02bf706979 --- /dev/null +++ b/research/signed-pauli-partial-extension/pauli.py @@ -0,0 +1,207 @@ +"""Complete partial Hermitian Pauli conjugations; exact binary arithmetic. + +Prepared for JoyboyBrian with substantial OpenAI Codex assistance. Apache-2.0. +""" +from math import prod + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def parity(value): + return value.bit_count() & 1 + + +def omega(a, b, n): + mask = (1 << n) - 1 + return parity(((a & mask) & (b >> n)) ^ ((a >> n) & (b & mask))) + + +def label(p, n): + return p[0] | (p[1] << n) + + +def multiply(a, b): + return a[0] ^ b[0], a[1] ^ b[1], (a[2] + b[2] + 2 * parity(a[1] & b[0])) % 4 + + +def span_coordinates(rows, value): + pivots = {} + for j, row in enumerate(rows): + tag = 1 << j + while row and row.bit_length() - 1 in pivots: + old, coefficient = pivots[row.bit_length() - 1] + row ^= old + tag ^= coefficient + if row: + pivots[row.bit_length() - 1] = row, tag + coefficient = 0 + while value and value.bit_length() - 1 in pivots: + old, tag = pivots[value.bit_length() - 1] + value ^= old + coefficient ^= tag + return None if value else coefficient + + +def rank(rows): + independent = [] + for row in rows: + if span_coordinates(independent, row) is None: + independent.append(row) + return len(independent) + + +def solve(rows, rhs, width): + """Solve binary equations, taking all free variables zero.""" + pivots = {} + for row, bit in zip(rows, rhs): + while row and row.bit_length() - 1 in pivots: + old, value = pivots[row.bit_length() - 1] + row ^= old + bit ^= value + if not row: + need(not bit, "inconsistent internal linear system") + else: + pivots[row.bit_length() - 1] = row, bit + value = 0 + for pivot, (row, bit) in sorted(pivots.items()): + if bit ^ parity(row & value): + value |= 1 << pivot + need(value < (1 << width), "linear-system width") + return value + + +def dual(vector, n): + mask = (1 << n) - 1 + return (vector >> n) | ((vector & mask) << n) + + +def apply_gate(pauli, gate): + x, z, phase = pauli + if gate[0] == "turn": + a, b, sign = gate[1:] + if parity((a & z) ^ (b & x)): + phase += (a & b).bit_count() + 2 * parity(b & x) - sign + x ^= a + z ^= b + elif gate[0] == "x": + phase += 2 * parity(z & gate[1]) + elif gate[0] == "s": + phase += gate[2] * (x & gate[1]).bit_count() + if gate[2] % 2: + z ^= x & gate[1] + else: + need(gate[0] == "phase", "unknown literal gate") + return x, z, phase % 4 + + +def apply_word(pauli, gates): + for gate in gates: + pauli = apply_gate(pauli, gate) + return pauli + + +def validate(n, constraints): + need(type(n) is int and 0 <= n <= 9, "reference n must be 0..9") + for pair in constraints: + need(len(pair) == 2, "constraint pair length") + for p in pair: + need(len(p) == 3 and all(type(v) is int for v in p), "typed Pauli triple") + x, z, phase = p + need(0 <= x < (1 << n) and 0 <= z < (1 << n) and 0 <= phase < 4, + "Pauli range") + need(phase % 2 == parity(x & z), "Hermitian Pauli required") + + +def analyze(n, constraints): + validate(n, constraints) + selected, source, target = [], [], [] + for j, (p, q) in enumerate(constraints): + if span_coordinates(source, label(p, n)) is None: + selected.append(j) + source.append(label(p, n)) + target.append(label(q, n)) + if rank(target) != len(target): + return None, "label-relations" + for i, v in enumerate(source): + for j, w in enumerate(source): + if omega(v, w, n) != omega(target[i], target[j], n): + return None, "commutators" + for p, q in constraints: + coordinate = span_coordinates(source, label(p, n)) + pp = qq = (0, 0, 0) + for j, index in enumerate(selected): + if coordinate & (1 << j): + pp = multiply(pp, constraints[index][0]) + qq = multiply(qq, constraints[index][1]) + if label(qq, n) != label(q, n): + return None, "label-relations" + if (pp[2] - p[2]) % 4 != (qq[2] - q[2]) % 4: + return None, "central-relations" + restricted = [sum(omega(a, b, n) << j for j, b in enumerate(source)) for a in source] + k, twice_r = len(source), rank(restricted) + need(twice_r % 2 == 0, "alternating rank must be even") + return {"indices": selected, "source": source, "target": target, + "k": k, "r": twice_r // 2, "t": k - twice_r}, "compatible" + + +def sp_order(n): + return (1 << (n * n)) * prod((1 << (2 * j)) - 1 for j in range(1, n + 1)) + + +def completion_count(n, data): + ambient = n - data["r"] + orbit = prod((1 << (2 * ambient - j)) - (1 << j) for j in range(data["t"])) + symplectic = sp_order(ambient) + need(symplectic % orbit == 0, "pointwise stabilizer quotient") + return (1 << (2 * n - data["k"])) * (symplectic // orbit) + + +def complete(n, constraints): + """Return projective count and an actual chosen dyadic Clifford word.""" + data, reason = analyze(n, constraints) + if data is None: + return {"count": 0, "reason": reason, "gates": None} + columns = [1 << i for i in range(2 * n)] + fixed, gates = [], [] + mask = (1 << n) - 1 + for source, target in zip(data["source"], data["target"]): + current = 0 + for j, column in enumerate(columns): + if source & (1 << j): + current ^= column + axes = [] + if current != target: + if omega(current, target, n): + axes = [current ^ target] + else: + rows = [dual(p, n) for p in (*fixed, current, target)] + rhs = [omega(current, p, n) for p in fixed] + [1, 1] + middle = solve(rows, rhs, 2 * n) + axes = [current ^ middle, middle ^ target] + for axis in axes: + need(axis != 0 and all(not omega(axis, p, n) for p in fixed), "fixed-prefix axis") + columns = [v ^ (axis if omega(v, axis, n) else 0) for v in columns] + gates.append(["turn", axis & mask, axis >> n, 1]) + fixed.append(target) + rhs = [] + for index in data["indices"]: + p, q = constraints[index] + actual = apply_word(tuple(p), gates) + need(label(actual, n) == label(q, n) and (q[2] - actual[2]) % 2 == 0, + "unsigned symplectic completion") + rhs.append(((q[2] - actual[2]) % 4) // 2) + correction = solve([dual(p, n) for p in data["target"]], rhs, 2 * n) + if correction & mask: + gates.append(["x", correction & mask]) + if correction >> n: + gates.append(["s", correction >> n, 2]) + need(all(apply_word(tuple(p), gates) == tuple(q) for p, q in constraints), "signed completion") + tableau = [apply_word((1 << j, 0, 0), gates) for j in range(n)] + tableau += [apply_word((0, 1 << j, 0), gates) for j in range(n)] + return {"count": completion_count(n, data), "reason": reason, + "gates": gates, "tableau": tableau, + "dimensions": {k: data[k] for k in ("k", "r", "t")}, + "global_phase_contract": "literal word chooses its own phase; no supplied target equality"} diff --git a/research/signed-pauli-partial-extension/verify.py b/research/signed-pauli-partial-extension/verify.py new file mode 100644 index 0000000000..e4059ee5f6 --- /dev/null +++ b/research/signed-pauli-partial-extension/verify.py @@ -0,0 +1,229 @@ +"""Literal finite-Pauli oracle, partial counts and actual compiler binding.""" +from collections import Counter +import argparse +import hashlib +import json +from pathlib import Path +import runpy +import sys + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) +from pauli import complete, need, apply_word + + +def encoded(value): + return json.dumps(value, sort_keys=True, separators=(",", ":")) + + +def sha(path): + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def literal_pauli(n, p): + x, z, phase = p + return tuple((j ^ x, (phase + 2 * ((j & z).bit_count() % 2)) % 4) + for j in range(1 << n)) + + +def product(a, b): + return tuple((a[k][0], (phase + a[k][1]) % 4) for k, phase in b) + + +def as_pauli(matrix, n): + x, phase = matrix[0] + z = sum((((matrix[1 << j][1] - phase) % 4) // 2) << j for j in range(n)) + p = x, z, phase + need(literal_pauli(n, p) == matrix, "literal Pauli reconstruction") + return p + + +def signed_group(n): + """Closure using literal monomial products, not the implementation formula.""" + mask = (1 << n) - 1 + ps = [(x, z, ((x & z).bit_count() + 2 * sign) % 4) + for x in range(1 << n) for z in range(1 << n) for sign in range(2)] + transitions, actions = [], {} + for axis in range(1, 1 << (2 * n)): + x, z = axis & mask, axis >> n + h = literal_pauli(n, (x, z, (x & z).bit_count() % 4)) + table = {} + for p in ps: + matrix = literal_pauli(n, p) + hp, ph = product(h, matrix), product(matrix, h) + image = matrix if hp == ph else tuple((k, (phase - 1) % 4) for k, phase in hp) + table[p] = as_pauli(image, n) + transitions.append(table) + actions[("turn", x, z, 1)] = table + for typ in ("x", "s"): + for mask in range(1 << n): + gate = (typ, mask) if typ == "x" else (typ, mask, 2) + k = literal_pauli(n, (mask, 0, 0) if typ == "x" else (0, mask, 0)) + actions[gate] = {p: as_pauli(product(product(k, literal_pauli(n, p)), k), n) + for p in ps} + identity = tuple([(1 << j, 0, 0) for j in range(n)] + + [(0, 1 << j, 0) for j in range(n)]) + seen, queue = {identity}, [identity] + for tableau in queue: + for action in transitions: + target = tuple(action[p] for p in tableau) + if target not in seen: + seen.add(target) + queue.append(target) + need(len(seen) == {1: 24, 2: 11520}[n], "literal full signed group") + return identity, seen, actions + + +def finite_counts(n): + identity, group, actions = signed_group(n) + shapes = [[], [0], [0, 1]] if n == 1 else [[], [0], [0, 1], + [0, 2], [0, 2, 1], [0, 1, 2, 3]] + reports, compiler_cases = [], [] + for indices in shapes: + counts = Counter(tuple(tableau[i] for i in indices) for tableau in group) + transcript = hashlib.sha256() + longest = 0 + for targets, count in sorted(counts.items()): + constraints = list(zip([identity[i] for i in indices], targets)) + result = complete(n, constraints) + need(result["count"] == count, "independent full-group restriction count") + need(tuple(result["tableau"]) in group, "constructed signed tableau outside group") + literal = identity + for gate in result["gates"]: + literal = tuple(actions[tuple(gate)][p] for p in literal) + need(literal == tuple(result["tableau"]), "independent literal emitted word") + need(tuple(literal[i] for i in indices) == targets, "independent partial images") + need(len(result["gates"]) <= 2 * len(indices) + 2, "gate upper bound") + longest = max(longest, len(result["gates"])) + transcript.update(encoded([targets, count, result["tableau"]]).encode()) + chosen = sorted(counts)[len(counts) // 3] + result = complete(n, list(zip([identity[i] for i in indices], chosen))) + compiler_cases.append((n, result["gates"], result["tableau"])) + reports.append({"indices": indices, "restrictions": len(counts), + "literal_word_checks": len(counts), + "group_order": len(group), "maximum_literal_gates": longest, + "sha256": transcript.hexdigest()}) + return {"n": n, "projective_group": len(group), "types": reports}, compiler_cases + + +def controls(): + x, z, y = (1, 0, 0), (0, 1, 0), (1, 1, 1) + bad = [ + (1, [(x, x), (z, z), (y, (1, 1, 3))], "central-relations"), + (1, [(x, x), (x, z)], "label-relations"), + (1, [(x, x), (z, x)], "label-relations"), + (2, [(x, x), (z, (2, 0, 0))], "commutators"), + (1, [((0, 0, 0), (0, 0, 2))], "central-relations"), + ] + for n, pairs, reason in bad: + result = complete(n, pairs) + need(result["count"] == 0 and result["reason"] == reason, "semantic rejection") + need(complete(1, [(x, x)])["count"] == 4, "one fixed generator") + need(complete(1, [(x, x), (z, z)])["count"] == 1, "full signed tableau") + need(complete(0, [((0, 0, 2), (0, 0, 2))])["count"] == 1, "zero dimension") + malformed = [(True, []), (10, []), (1, [((True, 0, 0), x)]), + (1, [((1, 1, 0), y)]), (1, [((2, 0, 0), x)])] + for n, pairs in malformed: + try: + complete(n, pairs) + except ValueError: + continue + raise ValueError("malformed contract accepted") + return {"semantic_rejections": len(bad), "malformed_rejections": len(malformed), + "one_fixed_generator_count": 4, "full_signed_tableau_count": 1, + "zero_dimensional_count": 1} + + +def source_bindings(cases): + source_path = ROOT / "research/native-clifford-gauge-compiler/compiler/clifford_compile.py" + # run_path reads the authenticated source directly, without an imported pyc. + source = runpy.run_path(str(source_path), run_name="pinned_native_source") + records = [] + for n, word, expected in cases: + need(source["tableau"](n, word) == expected, "actual source signed tableau") + certificate = source["compile_word"](n, word) + columns = source["replay"](n, word, certificate, full_columns=n <= 3) + need(0 <= certificate["paid_rank"] <= n, "source rank-d bound") + records.append({"n": n, "word": word, "paid_rank": certificate["paid_rank"], + "source_replay_columns": columns}) + return source, records + + +def larger_and_phase_cases(): + cases = [] + for n in (3, 9): + mask = (1 << n) - 1 + word = [["turn", (7 * j + 3) & mask, (11 * j + 5) & mask, + 1 if j % 2 else -1] for j in range(12)] + ps = [(1 << j, 0, 0) for j in range(min(3, n))] + ps += [(0, 1, 0), (3, 0, 0), (1, 1, 1)] + constraints = [(p, apply_word(p, word)) for p in ps] + result = complete(n, constraints) + need(result["count"] > 0, "larger literal source contract") + cases.append((n, result["gates"], result["tableau"])) + return cases + + +def phase_and_tensor(source): + negative = [["turn", 1, 0, 1], ["turn", 1, 0, 1], + ["turn", 0, 1, 1], ["turn", 0, 1, 1]] * 2 + actual = source["compile_word"](1, negative) + source["replay"](1, negative, actual) + need(actual["paid_rank"] == 0 and actual["G_global_i"] == 2, "negative identity anchor") + x, z = (1, 0, 0), (0, 1, 0) + chosen = complete(1, [(x, x), (z, z)]) + need(chosen["gates"] == [] and source["state"](1, negative) != + source["state"](1, chosen["gates"]), "projective is not absolute target equality") + for f in (2, 3): + lifted = source["lift_word"](1, [["phase", 1]], f) + need(lifted == [["phase", f]], "literal phase tensorization") + certificate = source["compile_word"](f, lifted) + source["replay"](f, lifted, certificate) + need(certificate["G_global_i"] == f % 4, "tensor absolute phase") + need(source["state"](f, lifted) != source["state"](f, [["phase", 1]]), + "dropped tensor phase must be detected") + return {"identity_tableau_negative_anchor_rejected": True, + "literal_global_phase_tensor_widths": [2, 3]} + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--write", type=Path) + args = parser.parse_args() + if args.write: + need(not args.write.exists(), "occupied receipt output") + pins = json.loads((HERE / "SOURCES.json").read_text()) + live = {} + for item in pins["files"]: + if item["usage"] == "input": + digest = sha(ROOT / item["path"]) + need(digest == item["sha256"], "source authentication: " + item["path"]) + live[item["path"]] = digest + reports, cases = [], [] + for n in (1, 2): + report, selected = finite_counts(n) + reports.append(report) + cases.extend(selected) + cases.extend(larger_and_phase_cases()) + source, bindings = source_bindings(cases) + result = {"schema_version": 1, "finite_domains": reports, "controls": controls(), + "actual_compiler": bindings, "absolute_phase": phase_and_tensor(source), + "sources": live, "local_sha256": {p.name: sha(p) for p in sorted(HERE.iterdir()) + if p.is_file() and p.name != "RESULT.json"}, + "new_kappa": False, "complete_supplier": False, + "count_contract": "projective Clifford; literal representative chooses its own phase"} + if args.write: + with args.write.open("x") as stream: + stream.write(json.dumps(result, indent=2, sort_keys=True) + "\n") + else: + need(encoded(json.loads((HERE / "RESULT.json").read_text())) == encoded(result), + "type-sensitive receipt mismatch") + print("PASS_SIGNED_PAULI_PARTIAL_EXTENSION " + encoded({ + "restrictions": sum(t["restrictions"] for r in reports for t in r["types"]), + "actual_compiler_cases": len(bindings)})) + + +if __name__ == "__main__": + main()