diff --git a/research/clifford-relation-obstructions/.gitattributes b/research/clifford-relation-obstructions/.gitattributes new file mode 100644 index 0000000000..44a23d1fe3 --- /dev/null +++ b/research/clifford-relation-obstructions/.gitattributes @@ -0,0 +1,2 @@ +* text eol=lf +*.gz binary diff --git a/research/clifford-relation-obstructions/MANIFEST.json b/research/clifford-relation-obstructions/MANIFEST.json new file mode 100644 index 0000000000..978b8c04e9 --- /dev/null +++ b/research/clifford-relation-obstructions/MANIFEST.json @@ -0,0 +1,18 @@ +{ + "files_sha256": { + ".gitattributes": "abeba78466be388a1c5f3cb4ad595b915a0aa9402d1d87e37dfe42762e5b91c5", + "dense.py": "760df8621caaa81ab841df39667f910b45b40d9167c02747db346e80649632af", + "independent.py": "6440b846d1dafd540f8d5192602a7e38abf8db5963848306838b8686dd70a954", + "model.py": "5d8c14e1aa62185fcb75725f0c337f00423642cebf121545d38a024567fc6dbf", + "NOTICE.md": "51a6115711b865339854be0d074821a4d360ddc0392c6617e52c118beb64e1b2", + "ORIGINS.json": "afa172d5f1fc8083f8595b7d43c023b834b76e0689a6fe9d66c225c6e92f845a", + "PROOF.md": "62f1f0adaead9ba8beb80118015d6feb81fc120e54a7cc0a0577587f8d5c8eeb", + "rank_support.py": "8999d8cc1a630db23578779cd9b30d15c426917037fbbaaca18b2d390da8bcfb", + "README.md": "9a2f98e47fdab88147630be1c13d108313ec7520612b60c81e60ef587577dc45", + "support.py": "c2dc7ccf0c0e4c7a0513a897ccadda6ffa745d6a0de1addda8b51e9ff956e25d", + "torus.py": "000db69c7d6dc3844655a39fea020cad4354d86793117ccc9ecc3f2863c06ab2", + "VALIDATION.json": "6c235f3c9f055ea87a0a31a6f262711f9f3b93c8c37160c243e6f865a205cd27", + "verify.py": "922c0b18c51155628cf32762479fb3d45721f9a317c93f6288a18e65d80d67d2" + }, + "certificate_payload_sha256": "dafd07d683df169f3c1613bc9ecbab054ce66581d93e7ef0c649286ec2eddc6c" +} diff --git a/research/clifford-relation-obstructions/NOTICE.md b/research/clifford-relation-obstructions/NOTICE.md new file mode 100644 index 0000000000..c14ac4d339 --- /dev/null +++ b/research/clifford-relation-obstructions/NOTICE.md @@ -0,0 +1,34 @@ +# Attribution and source scope + +Prepared by [littleBro](https://github.com/littleBro) with substantial OpenAI +Codex assistance in the research, implementation, proof exposition, packaging +and validation. New contribution under the repository's Apache-2.0 license. +No independent human review or contributor endorsement is represented as +completed. + +The open complex m=3, W=3, s=8 register problem and prior exclusions are +credited to eumemic's [PR #288](https://github.com/CrocSwap/integer-mult-bounds/pull/288), +pinned at `475a088b5862f75f0b10596cfd6842d19531a5ec`, and the predecessors it +credits, including Swapnil Jain's closed-ideas list and P1/P2 and the upstream +Clifford-frame framework. This package does not claim to originate that problem +or the general algebraic methods. + +The implementation is a focused extraction and adaptation of same-author +local exploratory packages. `ORIGINS.json` records hashes of those source +snapshots and of the earlier proof payload. Those provenance hashes are not +external dependencies or a claim that the snapshots were publicly reviewed. +All code and exact witnesses required here are supplied in this directory. + +The source target is CrocSwap/integer-mult-bounds main at +`66849e1475c930fd7732b1a0067ffee7e1e95f60`. Its selected construction was not +changed or replayed as part of this standalone contribution. At that base, +the selected kappa was 0.001635527380375392, conditional as stated in the +selected record and maintainer review. + +Overlap review read the earlier open-PR metadata through #661 and refreshed +recent metadata through #666. PR #620 concerns E8/decoder research; #634 +concerns coding-gap and minrank questions; #651 concerns fixed K-triangle +delivery; #661 concerns fixed-order R420 frame optimality; #662 accelerates +existing helper checks. None of those descriptions supplies these 33 fixed +register-word certificates. This comparison is not an audit of every PR diff +or a proof of literature novelty. The scoped result remains open to review. diff --git a/research/clifford-relation-obstructions/ORIGINS.json b/research/clifford-relation-obstructions/ORIGINS.json new file mode 100644 index 0000000000..558ab920ca --- /dev/null +++ b/research/clifford-relation-obstructions/ORIGINS.json @@ -0,0 +1,15 @@ +{ + "note": "Same-author unpublished research snapshots. These hashes record extraction provenance only; all runtime source and evidence needed for this contribution are included here.", + "local_snapshot_source_sha256": { + "small-register-search/search.py": "4937080f884c6074533e78f296294dbde29c30c93d53b9bc876ff2df15d82811", + "full-block-evolution/verify_blocks.py": "555c83180a34f796b30a97fee66a38b4fcefba3d297d012ea8ba1c73ecede4ef", + "symbolic-generator-evolution/symbolic.py": "953c97bb2eda709ee11e5d4079310f3dd3a196cbba30e52f9fad51d3faea2fcc", + "relation-evolution/support.py": "959f9b730d8c85b1c23efdc9ebfa80e206b01220a4ab77a3d855e6d824ca209b", + "relation-evolution/rank_support.py": "78ced44eb2c5d041955d7816ab5a24d939794971f6e06f9702e3fcdd1ab3b99a", + "relation-evolution/binomial.py": "78ac7052807f65e0c0210ea6769cc1e0db309e78aec3ae18335316758fd6bec8", + "relation-evolution/independent.py": "fe303facfcb59bab2c5738be8fae0f7a99a9719f702fb3aa5300b3f24c1781a0", + "small-register-search/audit.py": "ed8bf19248108f05a940907b1d0dffe471b9277b5ab517bf0e3661863ed774af" + }, + "original_solutions_payload_sha256": "67c74c0c03942f9d6936f9cf8f09e2961750f7d8174ed8097e46493f408df3d2", + "certificate_payload_sha256": "dafd07d683df169f3c1613bc9ecbab054ce66581d93e7ef0c649286ec2eddc6c" +} diff --git a/research/clifford-relation-obstructions/PROOF.md b/research/clifford-relation-obstructions/PROOF.md new file mode 100644 index 0000000000..469f3fdfe2 --- /dev/null +++ b/research/clifford-relation-obstructions/PROOF.md @@ -0,0 +1,132 @@ +# Model and certificate argument + +This written argument concerns the 33 supplied formal words, with arbitrary +complex scalar coefficients. The executable certificate is not a Lean proof. + +## Operators and endpoint + +Use basis vectors |x> indexed by x in F2^3. Let X_v translate x by v, and +Z_v multiply |x> by (-1)^(v dot x). The paid gate, for nonzero v, is + + C_v = ((1+i)/2) I + ((1-i)/2) X_v. + +In particular C_v^2 = X_v. Each occurrence is charged one paid call. The free +unaries are S_j|x> = i^(x_j)|x>, X_j, Z_j, directed CNOT gates +x -> x + x_a e_b, and CZ gates (-1)^(x_a x_b). The 18 free gate indices are +listed explicitly in `model.py`. Their words are fixed inputs, not additional +optimization variables in the exclusion. + +Let G be their projective Clifford group, represented by conjugation on the +six Pauli generators. A Pauli is encoded as i^p X^x Z^z. Scalars that give the +same conjugation action are identified. Let D be the diagonal Pauli subspace +and H its monomial stabilizer. The frame key of g records g^-1(D); equal frame +keys specify the same left coset H g. The Fourier rank rho(g) is the binary +rank of the X parts of the images of the three Z generators. It is constant +on each left H coset. + +A word is a 3-by-3 matrix over C[G], built from fixed unary diagonal matrices +and three arbitrary scalar matrices in GL(3,C). Its required endpoint is: +for each input column s, all nonzero group coefficients across the output +rows lie in one coset H g_s with rho(g_s)=3. This is the precise condition +being excluded. No finite 8-by-8 matrix representation is assumed linearly +independent. The negative conclusion is in the formal group algebra. + +For an intended tensor realization the inherited phase-quotient convention +requires multiplicity divisible by four. The finite dense controls verify +projective operators, not all tensor sizes, compilation or paid bit costs. + +## Necessary Boolean conditions + +Expand the word by paths. A path chooses one scalar entry per block and +contributes their product to one output/input/group coefficient. Equal group +labels are collected before endpoint constraints. The saved words have +coefficient one on each resulting path monomial; the arithmetic checker +explicitly checks this condition when reducing to binomial equations. + +Each scalar entry has a Boolean variable meaning nonzero. Invertibility +requires a nonzero determinant permutation term, although such a term alone +does not imply invertibility. Choose exactly one admissible full-rank frame +per input column. Every coefficient outside that frame must vanish. Exactly +one active monomial in such a coefficient is impossible, so the formula +forbids it. Allowing two or more active terms is only a relaxation. + +There is also a necessary whole-matrix matching test. Augmentation g -> 1 +maps the invertible word to the product of its scalar blocks. If positions +with any full-rank term admit no perfect matching, its augmented endpoint +would be singular. The formula then includes an empty clause. + +Boolean UNSAT is checked by a tree of binary splits, unit reasons and conflict +clauses. The replay uses literal lists, separately from the solver's bitset +propagation. A surviving Boolean model is not an arithmetic solution. + +## Invertibility constraints + +Write a three-block word, in matrix-composition order, as + + diag(w) C diag(v) B diag(u) A diag(t). + +For each middle product g = v_i u_j, let M_g retain the entries B_ij with +that product. Before the outside unaries its coefficient matrix is + + R_g = C M_g A. + +At position (r,s) the outside operations relabel g as w_r g t_s, a bijection +on labels. The chosen endpoint frames thus determine allowed positions of R_g. + +Only classes occupying distinct rows and distinct columns of B receive the +following strengthening. Such an M_g is a partial permutation with scalars. + +1. A required zero column of R_g implies M_g A(:,s)=0 since C is invertible. + Distinct occupied rows imply B_ij A_js=0 at every occupied position. +2. A required zero row implies C(r,:) M_g=0 since A is invertible. + Distinct occupied columns imply C_ri B_ij=0. +3. rank(R_g)=rank(M_g) equals the number of nonzero retained B entries. + A matrix supported on a graph has rank no larger than that graph's maximum + matching. The allowed positions of R_g must admit a matching at least as + large as every active subset of retained B entries. + +These implications yield necessary clauses. Nonpartial classes are left to +the weaker filter. Omitting these constraints cannot create a false exclusion. +The independent encoding builds middle classes from unary group products; +the producer's encoding builds them from path monomials. Their full formulas +are compared for every supplied word. + +## Torus refutations and learned clauses + +Fix one exact entry support and three selected frames. Every retained entry +is in C*. When every unwanted coefficient has at most two active monomials, +its nontrivial equation is x^a+x^b=0, equivalently x^(a-b)=-1. + +The certificate performs unimodular integer row and column operations on the +exponent matrix. Row operations preserve the torus equations; columns give +an invertible monomial substitution x_j=product(z_i^V_ji). A positive diagonal +and zero rows suffice; Smith divisibility is not needed. An odd right-hand +parity on a zero row is inconsistent. + +Otherwise a diagonal entry 1 fixes a sign. An entry 2 with even parity has +both signs as components. Other torsion or excessive component counts are +left unresolved by the arithmetic producer; the negative checker accepts no +certificate that silently omits them. All 78 saved negative certificates have +diagonal entries 1. + +On every component, substitute into det(A) det(B) det(C). If this Laurent +polynomial is identically zero, no point on the component makes all blocks +invertible. The checker directly expands the product using Leibniz's formula, +rather than the producer's successive polynomial products. It checks every +integer operation, the substitution and complete component coverage. + +Such a refutation permits a clause blocking exactly this entry support and +these frame choices. It does not permit blocking neighboring supports or +unspecified frames. The checker verifies the literal learned clause and then +replays the next support proof. A final Boolean contradiction covers all +remaining assignments; the removed ones already have exact refutations. +Therefore the entire fixed word is excluded over C, including scalar blocks +with zero entries. No arithmetic search timeout is used as evidence. + +## Boundaries + +This proves no impossibility for arbitrary three-block words, arbitrary +Clifford circuits, different frame groups or a finite representation that +admits additional linear cancellations. It does not decide the full register +problem in PR #288 or bound integer multiplication. The inputs are 33 explicit +skeletons, not representatives of all possibilities. diff --git a/research/clifford-relation-obstructions/README.md b/research/clifford-relation-obstructions/README.md new file mode 100644 index 0000000000..aa7836d88c --- /dev/null +++ b/research/clifford-relation-obstructions/README.md @@ -0,0 +1,105 @@ +# Exact exclusions for 33 fixed Clifford register words + +**Scoped negative result; no new primitive or kappa claim.** For each of the +33 words in `certificates.json.gz`, no choice of three invertible complex +3-by-3 scalar mixing blocks achieves the specified full-rank coset endpoint +with eight paid calls. This is a statement in a formal projective Clifford +group algebra. It does not exclude arbitrary three-block words or solve the +general m=3, W=3, s=8 register problem left open in [PR #288](https://github.com/CrocSwap/integer-mult-bounds/pull/288). + +The contribution is a self-contained support/rank/torus checker, explicit +fixed-word inputs, exact refutation traces and a written explanation of the +necessary conditions. Every runtime dependency is in this directory or the +Python standard library. No author-local directory, solver installation, +network access or historical research checkout is needed. + +## Reproduce + +From the repository root, with Python 3.10 or later: + +```sh +python -B -S research/clifford-relation-obstructions/verify.py +``` + +Expected final JSON contains: + +```json +{ + "status": "PASS_FIXED_CLIFFORD_WORD_EXCLUSIONS", + "counts": { + "excluded_templates": 33, + "exact_torus_refutations": 78, + "noncommuting_relations": 32 + } +} +``` + +The actual output has additional control counts. The command replays saved +witnesses; it does not rerun the bounded discovery search. It writes no files. +`-O` and `-OO` are explicitly rejected because the checker uses assertions. +`MANIFEST.json` pins source bytes and the decompressed certificate payload; +gzip container bytes are not used to decide mathematical equality. + +## Domain and method + +There are three streams of formal group-algebra elements, and each target +column must be supported in one left monomial coset of Fourier rank three. +Every unary operation and scalar-block location is fixed by the input word. +Each scalar block ranges over all GL(3,C), including matrices with zero +entries. [PROOF.md](PROOF.md) defines the operators, endpoint and model limits. + +For 32 words, the generator prescribed + + U = (I,Q,T), V = (I,P,Q), T = Q^-1 P Q, + +so that PQ = QT and Q is also repeated. P and Q do not commute. P and T each +have one paid gate; Q has one or two, with 16 words of each kind. Free +monomial decorations and outside gates vary, keeping the total at eight. +The other word is a commuting-diamond case from the preceding local search. +All 33 literal words are included; no equivalence-class uniqueness is claimed. + +The support relaxation encodes nonzero entries, a necessary determinant +matching, selected endpoint frames and the fact that a single nonzero term +cannot cancel. Invertibility gives stronger row, column and rank constraints +for partial-permutation middle-product classes. When a Boolean support survives, +binomial torus equations and exact Laurent determinant identities can refute +it. Only that exact support/frame assignment is then forbidden. The final +Boolean proof closes the fixed word. Twenty-nine words close without an +arithmetic cut; four require the 78 saved torus refutations. + +The recorded discovery seed was 521031. The conjugation generator accepted +16 words of each Q cost after 22 and 39 proposals respectively; a 112-gate +representation cap also applied. The final fixed-word search had a 55-second +overall budget, four seconds per word and at most 192 support assignments per +word; it completed all 33 exclusions. These are post-selection research inputs, +not an exhaustive domain or a statistical sample. The seed records provenance; +the literal inputs, rather than a seeded search rerun, define this certificate. + +## Validation and independence + +The checker compares direct trajectory enumeration with sequential polynomial +propagation. It reconstructs rank clauses from unary products and compares +them with the monomial-based encoding. It replays literal Boolean proof trees, +unimodular integer operations and a direct Leibniz expansion of determinant +products. No SAT or arithmetic solver is trusted for a negative conclusion. + +Controls include 33 exact dense skeleton checks, 150 Pauli conjugation +identities, seven paid-gate square identities, four known nine-call solutions, +recovery of their scalar matrices, and an eight-call rejection. A second +eight-call control deliberately survives the Boolean relaxation while its +concrete scalar word fails: Boolean feasibility is not a construction. +Corrupt integer traces, Boolean proofs and learned clauses, missing final +refutations and an unsupported complex-torsion exclusion are rejected. + +The two path/rank encodings share the tableau/coset core. The dense Gaussian +matrix implementation independently checks that core on the finite corpus; +it does not establish an all-size representation theorem. The methods were +implemented and checked with substantial AI assistance, not independent human +peer review. There is no Lean proof or novelty claim for the general support, +rank, torus or determinant techniques. See `VALIDATION.json` for the measured +local checks and [NOTICE.md](NOTICE.md) for attribution. + +The selected frontier, all supplier sources and `upstream/` are unchanged. +This standalone contribution does not replay or strengthen their compiler, +physical, recursive, precision/tape or analytic assumptions. No bit primitive, +complete exponent invoice or practical multiplication speedup is supplied. diff --git a/research/clifford-relation-obstructions/VALIDATION.json b/research/clifford-relation-obstructions/VALIDATION.json new file mode 100644 index 0000000000..e7ca41d9af --- /dev/null +++ b/research/clifford-relation-obstructions/VALIDATION.json @@ -0,0 +1,41 @@ +{ + "status": "PASS", + "environment": { + "system": "Windows", + "python": "3.14.4" + }, + "result": { + "status": "PASS_FIXED_CLIFFORD_WORD_EXCLUSIONS", + "counts": { + "boolean_proof_nodes": 14483, + "support_models_or_refutations": 111, + "dense_skeleton_checks": 33, + "excluded_templates": 33, + "noncommuting_relations": 32, + "exact_torus_refutations": 78, + "dense_generator_identities": 150, + "paid_square_identities": 7, + "positive_nine_call_controls": 4, + "dense_positive_checks": 8, + "relaxation_false_positive": 1, + "negative_eight_call": 1, + "integer_trace_controls": 3, + "corrupt_integer_traces_rejected": 3, + "corrupt_boolean_proofs_rejected": 1, + "corrupt_learned_clauses_rejected": 1, + "missing_final_refutations_rejected": 1, + "unsupported_torsion_exclusions_rejected": 1 + }, + "certificate_payload_sha256": "dafd07d683df169f3c1613bc9ecbab054ce66581d93e7ef0c649286ec2eddc6c" + }, + "checks": { + "fresh_directory_without_repository_or_sibling_packages": "PASS", + "different_working_directory": "PASS", + "changed_gzip_header_and_compression_same_payload": "PASS identical mathematical output", + "corrupt_payload": "rejected", + "-O": "rejected explicitly", + "-OO": "rejected explicitly" + }, + "elapsed_seconds": 78.074, + "scope": "Focused standalone replay only; unchanged repository-wide suite and selected frontier replay not run; no remote CI or human-review claim." +} diff --git a/research/clifford-relation-obstructions/certificates.json.gz b/research/clifford-relation-obstructions/certificates.json.gz new file mode 100644 index 0000000000..7c1dce19f8 Binary files /dev/null and b/research/clifford-relation-obstructions/certificates.json.gz differ diff --git a/research/clifford-relation-obstructions/dense.py b/research/clifford-relation-obstructions/dense.py new file mode 100644 index 0000000000..6bef093135 --- /dev/null +++ b/research/clifford-relation-obstructions/dense.py @@ -0,0 +1,130 @@ +"""Independent exact Gaussian-matrix operator and endpoint controls. + +The matrix arithmetic does not use tableau update formulas. +Apache-2.0; substantial OpenAI Codex assistance. +""" +from fractions import Fraction as Q +from functools import lru_cache +from model import IDENTITY, FREE + +N = 8 + + +def rot(a, b, p): + return ((a, b), (-b, a), (-a, -b), (b, -a))[p % 4] + + +def normalize(e, re, im, projective=False): + while e and all(value % 2 == 0 for value in re+im): + e -= 1 + re, im = [v//2 for v in re], [v//2 for v in im] + variants = [] + for p in range(4 if projective else 1): + entries = [rot(a, b, p) for a, b in zip(re, im)] + variants.append((e, tuple(a for a, _ in entries), tuple(b for _, b in entries))) + return min(variants) + + +def identity(): + return normalize(0, [int(i == j) for i in range(N) for j in range(N)], [0]*64) + + +@lru_cache(maxsize=40_000) +def multiply(a, b, projective=False): + ea, ar, ai = a + eb, br, bi = b + re, im = [0]*64, [0]*64 + for i in range(N): + for k in range(N): + x, y = ar[8*i+k], ai[8*i+k] + if x == y == 0: + continue + for j in range(N): + u, v = br[8*k+j], bi[8*k+j] + re[8*i+j] += x*u-y*v + im[8*i+j] += x*v+y*u + return normalize(ea+eb, re, im, projective) + + +def pauli(value): + x, z, p = value & 7, (value >> 3) & 7, value >> 6 + re, im = [0]*64, [0]*64 + for col in range(8): + re[8*(col ^ x)+col], im[8*(col ^ x)+col] = rot(1, 0, p+2*((z & col).bit_count() % 2)) + return normalize(0, re, im) + + +@lru_cache(None) +def operator(op): + name, a, b = op + re, im = [0]*64, [0]*64 + if name == "C": + for col in range(8): + re[8*col+col], im[8*col+col] = 1, 1 + re[8*(col ^ a)+col], im[8*(col ^ a)+col] = 1, -1 + return normalize(1, re, im) + for col in range(8): + row, p = col, 0 + if name == "S": + p = (col >> a) & 1 + elif name == "X": + row ^= 1 << a + elif name == "Z": + p = 2*((col >> a) & 1) + elif name == "CX": + row ^= ((col >> a) & 1) << b + elif name == "CZ": + p = 2*((col >> a) & 1)*((col >> b) & 1) + else: + raise ValueError(op) + re[8*row+col], im[8*row+col] = rot(1, 0, p) + return normalize(0, re, im) + + +@lru_cache(maxsize=10_000) +def signature(matrix): + # Recover all six conjugated generators by GP = P'G, independently of + # the optimized tableau update formulas used by the search. + images = [] + for generator in IDENTITY: + wanted = multiply(matrix, pauli(generator)) + matches = [value for value in range(256) if multiply(pauli(value), matrix) == wanted] + assert len(matches) == 1 + images.append(matches[0]) + return tuple(images) + + +def independent_frame(g): + basis = [value & 63 for value in g] + result = 0 + for value in range(64): + image = 0 + for i in range(6): + if value & (1 << i): + image ^= basis[i] + if image & 7 == 0: + result |= 1 << value + return result + + +def execute(program): + unit = normalize(*identity(), projective=True) + rows = [{(r, unit): Q(1)} for r in range(3)] + for gate in program: + if gate[0] == 'mix3': + changed = [] + for r in range(3): + row = {} + for c in range(3): + for key, value in rows[c].items(): + row[key] = row.get(key, 0)+gate[1+3*r+c]*value + changed.append({key: value for key, value in row.items() if value}) + rows = changed + else: + op = ('C', gate[2], 0) if gate[0] == 'paid' else FREE[gate[2]] + changed = {} + for (column, matrix), value in rows[gate[1]].items(): + key = column, multiply(operator(op), matrix, True) + changed[key] = changed.get(key, 0)+value + rows[gate[1]] = {key: value for key, value in changed.items() if value} + return [{(col, signature(matrix)): value for (col, matrix), value in row.items()} for row in rows] diff --git a/research/clifford-relation-obstructions/independent.py b/research/clifford-relation-obstructions/independent.py new file mode 100644 index 0000000000..f9bb18fddf --- /dev/null +++ b/research/clifford-relation-obstructions/independent.py @@ -0,0 +1,176 @@ +"""Independent path enumeration and literal integer/Laurent proof replay.""" +from collections import defaultdict +from itertools import combinations, permutations, product + +from model import Engine, FREE + + +def layers(program): + result = [[[] for _ in range(3)]] + for gate in program: + if gate[0] == 'mix3': + result.append([[] for _ in range(3)]) + else: + assert gate[0] in ('paid', 'free') + op = ('C', gate[2], 0) if gate[0] == 'paid' else FREE[gate[2]] + result[-1][gate[1]].append(op) + return result + + +def group(ring, operations): + g = 0 + for op in operations: + g = ring.transitions(op, g) + return g + + +def path_rows(ring, program): + stages = layers(program) + blocks = len(stages)-1 + rows = [{} for _ in range(3)] + for trajectory in product(range(3), repeat=blocks+1): + operations, mask = [], 0 + for k, role in enumerate(trajectory): + operations.extend(stages[k][role]) + if k < blocks: + mask |= 1 << (9*k+3*trajectory[k+1]+role) + key = (group(ring, operations) << 2) | trajectory[0] + polynomial = rows[trajectory[-1]].setdefault(key, {}) + polynomial[mask] = polynomial.get(mask, 0)+1 + return tuple(rows), blocks + + +def rank_formula(program, cnf): + """Build strengthened clauses from unary products, not path polynomials.""" + ring, stages = Engine(), layers(program) + assert len(stages) == 4 + selectors = {(x[1], x[2]): i for i, x in enumerate(cnf['labels']) if x and x[0] == 'frame'} + products = defaultdict(list) + for i in range(3): + for j in range(3): + products[group(ring, stages[1][j]+stages[2][i])].append(3*i+j) + counts = defaultdict(int) + for cells in sorted(tuple(v) for v in products.values()): + if len({p//3 for p in cells}) != len(cells) or len({p % 3 for p in cells}) != len(cells): + continue + i, j = divmod(cells[0], 3) + guards = {} + for r in range(3): + for s in range(3): + g = group(ring, stages[0][s]+stages[1][j]+stages[2][i]+stages[3][r]) + frame, rank = ring.frame_info(g) + if rank == 3: + guards[r, s] = selectors[s, frame] + for s, frames in enumerate(cnf['target_frames']): + for frame in frames: + f = selectors[s, frame] + if any(guards.get((r, s)) == f for r in range(3)): + continue + for position in cells: + cnf['clauses'].append([-f, -(10+position), -(3*(position % 3)+s+1)]) + counts['zero_column'] += 1 + for r in range(3): + allowed = sorted({guards[r, s] for s in range(3) if (r, s) in guards}) + for position in cells: + cnf['clauses'].append([-(19+3*r+position//3), -(10+position), *allowed]) + counts['zero_row'] += 1 + for size in range(1, len(cells)+1): + variables = [] + for rs in combinations(range(3), size): + for ss in permutations(range(3), size): + matching = tuple(zip(rs, ss)) + if any(p not in guards for p in matching): + continue + cnf['labels'].append(['rank_matching', list(cells), list(map(list, matching))]) + v = len(cnf['labels'])-1 + variables.append(v) + for f in sorted({guards[p] for p in matching}): + cnf['clauses'].append([-v, f]) + for subset in combinations(cells, size): + cnf['clauses'].append([*(-(10+p) for p in subset), *variables]) + counts['rank_bound'] += 1 + cnf['variables'] = len(cnf['labels'])-1 + cnf['strengthening_counts'] = dict(counts) + return cnf + + +def diagonal_trace(equations, certificate): + a = [list(row) for row in equations['matrix']] + b = list(equations['rhs_parity']) + n = len(equations['nonzero_entries']) + transform = [[int(i == j) for j in range(n)] for i in range(n)] + for step in certificate['steps']: + op, *args = step + if op == 'row_swap': + i, j = args + assert 0 <= i < len(a) and 0 <= j < len(a) and i != j + a[i], a[j] = a[j], a[i] + b[i], b[j] = b[j], b[i] + elif op == 'row_negate': + i, = args + a[i] = [-v for v in a[i]] + b[i] = -b[i] + elif op == 'row_add': + i, j, amount = args + assert i != j and type(amount) is int + a[i] = [a[i][k]+amount*a[j][k] for k in range(n)] + b[i] += amount*b[j] + elif op == 'col_swap': + i, j = args + assert 0 <= i < n and 0 <= j < n and i != j + for row in a+transform: + row[i], row[j] = row[j], row[i] + else: + assert op == 'col_add' + i, j, amount = args + assert i != j and type(amount) is int + for row in a+transform: + row[i] += amount*row[j] + rank = certificate['rank'] + assert certificate['column_transform'] == transform and certificate['rhs'] == b + assert [a[i][i] for i in range(rank)] == certificate['diagonal'] + assert all(v > 0 for v in certificate['diagonal']) + assert all(not a[i][j] for i in range(len(a)) for j in range(n) if i != j or i >= rank) + + +def determinant_identity(equations, certificate, signs): + """One direct Leibniz expansion of the product, not successive products.""" + rank = certificate['rank'] + transform = certificate['column_transform'] + dimension = len(transform)-rank + entries = {old: new for new, old in enumerate(equations['nonzero_entries'])} + coefficients = defaultdict(int) + all_permutations = tuple(permutations(range(3))) + for choices in product(all_permutations, repeat=equations['blocks']): + chosen = [9*k+3*r+permutation[r] for k, permutation in enumerate(choices) for r in range(3)] + if any(entry not in entries for entry in chosen): + continue + exponents = [sum(transform[entries[entry]][j] for entry in chosen) for j in range(len(transform))] + phase = sum(exponents[i]*signs[i] for i in range(rank)) + phase += sum(p[i] > p[j] for p in choices for i in range(3) for j in range(i+1, 3)) + coefficients[tuple(exponents[rank:])] += (-1)**(phase % 2) + return {e: c for e, c in coefficients.items() if c} + + +def binomial_certificate(expected, result): + assert result['equations'] == expected + cert = result['diagonalization'] + diagonal_trace(expected, cert) + odd = any(v % 2 for v in cert['rhs'][cert['rank']:]) + if result['status'] == 'inconsistent_torus': + assert odd + return + assert not odd and result['status'] in ('all_components_singular', 'exact_rational_point') + choices = [] + for d, b in zip(cert['diagonal'], cert['rhs']): + assert d == 1 or (d == 2 and b % 2 == 0) + choices.append([b % 2] if d == 1 else [0, 1]) + expected_signs = list(map(list, product(*choices))) + if result['status'] == 'all_components_singular': + assert [c['signs'] for c in result['components']] == expected_signs + for component in result['components']: + assert component['signs'] in expected_signs + polynomial = determinant_identity(expected, cert, component['signs']) + assert bool(polynomial) != component['determinant_product_zero'] + if result['status'] == 'all_components_singular': + assert not polynomial diff --git a/research/clifford-relation-obstructions/model.py b/research/clifford-relation-obstructions/model.py new file mode 100644 index 0000000000..1ebf1ebd7c --- /dev/null +++ b/research/clifford-relation-obstructions/model.py @@ -0,0 +1,190 @@ +"""Exact three-stream projective Clifford group-algebra model. + +Apache-2.0. Substantial OpenAI Codex assistance; see NOTICE.md. +""" +from fractions import Fraction as Q +from functools import lru_cache +from itertools import combinations + +M = 3 +IDENTITY = tuple([1 << i for i in range(M)] + [1 << (M+i) for i in range(M)]) +Op = tuple[str, int, int] +PAIRS = ((0, 1), (0, 2), (1, 2)) +FREE = tuple([('S', i, 0) for i in range(M)] + + [('X', i, 0) for i in range(M)] + + [('Z', i, 0) for i in range(M)] + + [('CX', i, j) for i in range(M) for j in range(M) if i != j] + + [('CZ', i, j) for i, j in combinations(range(M), 2)]) + + +def pauli_image(op: Op, value: int) -> int: + x, z, p = value & 7, (value >> 3) & 7, value >> 6 + name, a, b = op + if name == "C": + if (z & a).bit_count() & 1: + x ^= a + p -= 1 + elif name == "S": + u = (x >> a) & 1 + p += u + z ^= u << a + elif name == "X": + p += 2*((z >> a) & 1) + elif name == "Z": + p += 2*((x >> a) & 1) + elif name == "CX": + x ^= ((x >> a) & 1) << b + z ^= ((z >> b) & 1) << a + elif name == "CZ": + u, v = (x >> a) & 1, (x >> b) & 1 + p += 2*u*v + z ^= (u << b) | (v << a) + else: + raise ValueError(op) + return x | (z << 3) | ((p % 4) << 6) + + +def rank_binary(values: list[int]) -> int: + pivots: dict[int, int] = {} + for value in values: + while value: + pivot = value.bit_length()-1 + if pivot in pivots: + value ^= pivots[pivot] + else: + pivots[pivot] = value + break + return len(pivots) + + +def fourier_rank(group: tuple[int, ...]) -> int: + return rank_binary([value & 7 for value in group[M:]]) + + +class Engine: + def __init__(self): + self.groups = [IDENTITY] + self.ids = {IDENTITY: 0} + self.transitions = lru_cache(maxsize=150_000)(self._transition) + self.frames = lru_cache(maxsize=40_000)(self._frame) + + def _frame(self, group_id): + g = self.groups[group_id] + basis = [sum((((g[M+i] >> j) & 1) << i) + | (((g[i] >> j) & 1) << (M+i)) for i in range(M)) + for j in range(M)] + span = [0] + for v in basis: + span += [w ^ v for w in span] + assert len(set(span)) == 8 + return sum(1 << v for v in span) + + def _transition(self, op, group_id): + new = tuple(pauli_image(op, value) for value in self.groups[group_id]) + if new not in self.ids: + self.ids[new] = len(self.groups) + self.groups.append(new) + return self.ids[new] + + def frame_info(self, group): + return self.frames(group), fourier_rank(self.groups[group]) + + +def add_poly(target, source, scalar=1, bit=0): + for mask, coefficient in source.items(): + assert not mask & bit + key = mask | bit + value = target.get(key, 0)+scalar*coefficient + if value: + target[key] = value + else: + target.pop(key, None) + + +def generic_paths(ring, program, kind): + """One independent variable per matrix entry, one selected entry per path.""" + rows = [{i: {0: 1}} for i in range(3)] + blocks = 0 + for gate in program: + if gate[0] not in ('mix', 'mix3'): + _, role, index = gate + op = ('C', index, 0) if gate[0] == 'paid' else FREE[index] + rows[role] = {(ring.transitions(op, key >> 2) << 2) | (key & 3): p + for key, p in rows[role].items()} + continue + assert gate[0] == ('mix' if kind == 2 else 'mix3') + roles = PAIRS[gate[1]] if kind == 2 else range(3) + changed = [] + for i in range(kind): + row = {} + for j, role in enumerate(roles): + bit = 1 << (kind*kind*blocks+kind*i+j) + for key, polynomial in rows[role].items(): + add_poly(row.setdefault(key, {}), polynomial, bit=bit) + changed.append(row) + for role, row in zip(roles, changed): + rows[role] = row + blocks += 1 + return tuple(rows), blocks + + +def coefficient_records(ring, rows): + records, targets = [], [set() for _ in range(3)] + for output, row in enumerate(rows): + # Interned integer IDs depend on what an Engine saw earlier. Proof + # row IDs must instead follow stable Clifford tableaus and columns. + for key, polynomial in sorted(row.items(), key=lambda item: (item[0] & 3, ring.groups[item[0] >> 2])): + frame, rank = ring.frame_info(key >> 2) + column = key & 3 + records.append({'output': output, 'column': column, 'frame': frame, + 'rank': rank, 'poly': polynomial}) + if rank == 3: + targets[column].add(frame) + return records, targets + + +def decode(program): + result = [] + for raw in program: + kind = raw[0] + if kind == 'mix3': + assert len(raw) == 10 + gate = (kind, *(Q(x) for x in raw[1:])) + else: + assert kind in ('paid', 'free') and len(raw) == 3 + assert type(raw[1]) is int and 0 <= raw[1] < 3 + assert type(raw[2]) is int + assert (1 <= raw[2] <= 7) if kind == 'paid' else (0 <= raw[2] < 18) + gate = tuple(raw) + result.append(gate) + return tuple(result) + + +def execute(ring, program): + rows = [{i: Q(1)} for i in range(3)] + for gate in program: + if gate[0] == 'mix3': + changed = [] + for r in range(3): + row = {} + for c in range(3): + for key, value in rows[c].items(): + row[key] = row.get(key, 0)+gate[1+3*r+c]*value + changed.append({key: value for key, value in row.items() if value}) + rows = changed + else: + op = ('C', gate[2], 0) if gate[0] == 'paid' else FREE[gate[2]] + rows[gate[1]] = {(ring.transitions(op, key >> 2) << 2) | (key & 3): value + for key, value in rows[gate[1]].items()} + return tuple(rows) + + +def endpoint_frames(ring, rows): + answer = [] + for column in range(3): + values = {ring.frame_info(key >> 2) for row in rows for key, v in row.items() + if v and key & 3 == column} + if len(values) != 1 or next(iter(values))[1] != 3: + return None + answer.append(next(iter(values))[0]) + return answer diff --git a/research/clifford-relation-obstructions/rank_support.py b/research/clifford-relation-obstructions/rank_support.py new file mode 100644 index 0000000000..0c37381b22 --- /dev/null +++ b/research/clifford-relation-obstructions/rank_support.py @@ -0,0 +1,80 @@ +"""Add exact consequences of invertibility to the path-support relaxation. + +For each middle label g: R_g=C M_g A. When M_g is a partial permutation +with scalar entries, its rank is its number of nonzero entries. A zero +column/row of R_g also gives a zero column/row after cancelling C/A. +""" +from collections import defaultdict +from itertools import combinations, permutations + +from model import Engine, generic_paths, coefficient_records +from support import encode_support + + +def strengthen(cnf, records): + assert cnf['blocks'] == 3 + clauses, labels = cnf['clauses'], cnf['labels'] + selectors = {(v[1], v[2]): i for i, v in enumerate(labels) if v and v[0] == 'frame'} + groups = defaultdict(dict) + for record in records: + cells = set() + for mask in record['poly']: + middle = (mask >> 9) & 511 + assert middle.bit_count() == 1 + cells.add(middle.bit_length()-1) + key = tuple(sorted(cells)) + position = record['output'], record['column'] + assert position not in groups[key] + groups[key][position] = record + added = CounterLite() + for cells, grid in sorted(groups.items()): + assert len(grid) == 9 + rows, columns = [i//3 for i in cells], [i % 3 for i in cells] + partial = len(set(rows)) == len(rows) and len(set(columns)) == len(columns) + if not partial: + continue + allowed = {(r, s): selectors[s, record['frame']] for (r, s), record in grid.items() if record['rank'] == 3} + for s, targets in enumerate(cnf['target_frames']): + for frame in targets: + if any(grid[r, s]['rank'] == 3 and grid[r, s]['frame'] == frame for r in range(3)): + continue + for cell in cells: + i, j = divmod(cell, 3) + clauses.append([-selectors[s, frame], -(10+cell), -(3*j+s+1)]) + added['zero_column'] += 1 + for r in range(3): + guards = sorted({allowed[r, s] for s in range(3) if (r, s) in allowed}) + for cell in cells: + i, j = divmod(cell, 3) + clauses.append([-(19+3*r+i), -(10+cell), *guards]) + added['zero_row'] += 1 + for size in range(1, len(cells)+1): + matchings = [] + for rs in combinations(range(3), size): + for ss in permutations(range(3), size): + positions = list(zip(rs, ss)) + if not all(p in allowed for p in positions): + continue + labels.append(['rank_matching', list(cells), [list(p) for p in positions]]) + v = len(labels)-1 + matchings.append(v) + for guard in sorted({allowed[p] for p in positions}): + clauses.append([-v, guard]) + for active in combinations(cells, size): + clauses.append([*(-(10+i) for i in active), *matchings]) + added['rank_bound'] += 1 + cnf['variables'] = len(labels)-1 + cnf['strengthening_counts'] = dict(added) + return cnf + + +class CounterLite(dict): + def __missing__(self, key): + return 0 + + +def compile_support(program): + ring = Engine() + rows, blocks = generic_paths(ring, program, 3) + records, targets = coefficient_records(ring, rows) + return strengthen(encode_support(records, targets, blocks), records) diff --git a/research/clifford-relation-obstructions/support.py b/research/clifford-relation-obstructions/support.py new file mode 100644 index 0000000000..162d9f7b45 --- /dev/null +++ b/research/clifford-relation-obstructions/support.py @@ -0,0 +1,194 @@ +"""Necessary Boolean support conditions, with replayable DPLL refutations. + +Over C, one nonzero monomial cannot sum to zero. Two or more may or may not +cancel. SAT is therefore only a relaxation; UNSAT excludes the whole word. +""" +from collections import Counter +from itertools import permutations +import time + +from model import Engine, generic_paths, coefficient_records + + +def encode_support(records, targets, blocks): + clauses, labels = [], [None] + rank_support = [[any(r['output'] == i and r['column'] == j and r['rank'] == 3 + for r in records) for j in range(3)] for i in range(3)] + # Augmentation sends every group element to 1 and preserves invertibility. + # Its possible nonzero entries must admit a determinant matching. + if not any(all(rank_support[r][p[r]] for r in range(3)) for p in permutations(range(3))): + clauses.append([]) + def variable(label): + labels.append(label) + return len(labels)-1 + for k in range(blocks): + for r in range(3): + for c in range(3): + variable(['entry', k, r, c]) + # Nonsingular matrix => at least one nonzero determinant summand. + matchings = [] + for k in range(blocks): + choices = [] + for permutation in permutations(range(3)): + v = variable(['matching', k, list(permutation)]) + choices.append(v) + for row, col in enumerate(permutation): + clauses.append([-v, 9*k+3*row+col+1]) + clauses.append(choices) + matchings.append(choices) + frames = [] + for column, candidates in enumerate(targets): + choices = {frame: variable(['frame', column, frame]) for frame in sorted(candidates)} + clauses.append(list(choices.values())) + for i, a in enumerate(choices.values()): + for b in list(choices.values())[i+1:]: + clauses.append([-a, -b]) + frames.append(choices) + terms = {} + for record in records: + paths = [] + for mask, coefficient in sorted(record['poly'].items()): + assert coefficient != 0 and mask.bit_count() == blocks + if mask not in terms: + v = variable(['term', mask]) + factors = [i+1 for i in range(9*blocks) if mask & (1 << i)] + for factor in factors: + clauses.append([-v, factor]) + clauses.append([v, *(-factor for factor in factors)]) + terms[mask] = v + paths.append(terms[mask]) + guard = [frames[record['column']][record['frame']]] if record['rank'] == 3 else [] + for v in paths: + clauses.append([-v, *(p for p in paths if p != v), *guard]) + return {'clauses': clauses, 'labels': labels, 'variables': len(labels)-1, + 'blocks': blocks, 'target_frames': [sorted(t) for t in targets], + 'rank_supported_entries': rank_support} + + +def compile_support(program): + ring = Engine() + rows, blocks = generic_paths(ring, program, 3) + records, targets = coefficient_records(ring, rows) + return encode_support(records, targets, blocks) + + +class Limit(Exception): + pass + + +def solve(cnf, seconds=1, max_nodes=40000): + started = time.monotonic() + encoded, frequency = [], Counter() + for clause in cnf['clauses']: + positive = sum(1 << (v-1) for v in set(clause) if v > 0) + negative = sum(1 << (-v-1) for v in set(clause) if v < 0) + assert not positive & negative + encoded.append((positive, negative)) + for v in clause: + frequency[abs(v)] += 1 + nodes, propagations = 0, 0 + def visit(yes, no): + nonlocal nodes, propagations + nodes += 1 + if nodes > max_nodes or time.monotonic()-started >= seconds: + raise Limit + units = [] + while True: + changed, best = False, None + for index, (positive, negative) in enumerate(encoded): + if positive & yes or negative & no: + continue + remaining = (positive | negative) & ~(yes | no) + if not remaining: + return None, {'units': units, 'conflict': index} + count = remaining.bit_count() + if count == 1: + variable = remaining.bit_length() + literal = variable if remaining & positive else -variable + units.append([literal, index]) + if literal > 0: + yes |= remaining + else: + no |= remaining + propagations += 1 + changed = True + elif best is None or count < best[0]: + best = count, remaining + if not changed: + break + if best is None: + return [int(bool(yes & (1 << i))) for i in range(cnf['variables'])], None + candidates = [i+1 for i in range(cnf['variables']) if best[1] & (1 << i)] + variable = max(candidates, key=lambda i: (frequency[i], -i)) + bit = 1 << (variable-1) + model, positive = visit(yes | bit, no) + if model is not None: + return model, None + model, negative = visit(yes, no | bit) + if model is not None: + return model, None + return None, {'units': units, 'split': variable, 'positive': positive, 'negative': negative} + try: + model, proof = visit(0, 0) + status = 'support_feasible' if model is not None else 'support_obstruction' + except Limit: + model, proof, status = None, None, 'resource_limit' + return {'status': status, 'model': model, 'proof': proof, 'nodes': nodes, + 'propagations': propagations, 'elapsed_seconds': time.monotonic()-started, + 'limits': {'seconds': seconds, 'nodes': max_nodes}} + + +def verify(cnf, result): + """Literal-list clause replay; independent of the bitset solving routine.""" + clauses = cnf['clauses'] + if result['status'] == 'support_feasible': + model = result['model'] + assert len(model) == cnf['variables'] and all(v in (0, 1) for v in model) + assert all(any(bool(model[abs(v)-1]) == (v > 0) for v in clause) for clause in clauses) + assert result['proof'] is None + return 0 + if result['status'] == 'resource_limit': + assert result['proof'] is None and result['model'] is None + return 0 + assert result['status'] == 'support_obstruction' and result['model'] is None + nodes = 0 + def check(node, assignment): + nonlocal nodes + nodes += 1 + assignment = dict(assignment) + def residual(index): + assert 0 <= index < len(clauses) + literals = [] + for literal in clauses[index]: + variable = abs(literal) + if variable not in assignment: + literals.append(literal) + else: + assert assignment[variable] != (literal > 0), ('already satisfied', index) + return literals + for literal, reason in node['units']: + assert residual(reason) == [literal] + assert abs(literal) not in assignment + assignment[abs(literal)] = literal > 0 + if 'conflict' in node: + assert not residual(node['conflict']) + else: + v = node['split'] + assert 1 <= v <= cnf['variables'] and v not in assignment + check(node['positive'], {**assignment, v: True}) + check(node['negative'], {**assignment, v: False}) + check(result['proof'], {}) + return nodes + + +def selected_support(cnf, result): + assert result['status'] == 'support_feasible' + entries = [[0]*9 for _ in range(cnf['blocks'])] + frames = [None]*3 + for label, value in zip(cnf['labels'][1:], result['model']): + if label[0] == 'entry': + _, k, r, c = label + entries[k][3*r+c] = value + elif label[0] == 'frame' and value: + frames[label[1]] = label[2] + return {'entry_support': entries, 'frames': frames} diff --git a/research/clifford-relation-obstructions/torus.py b/research/clifford-relation-obstructions/torus.py new file mode 100644 index 0000000000..d1b6fcc097 --- /dev/null +++ b/research/clifford-relation-obstructions/torus.py @@ -0,0 +1,198 @@ +"""Exact torus equations on one Boolean support; no general Groebner search.""" +from fractions import Fraction as Q +from itertools import product, permutations + +from model import Engine, generic_paths, coefficient_records + + +def equations(program, selection): + ring = Engine() + rows, blocks = generic_paths(ring, program, 3) + records, _ = coefficient_records(ring, rows) + nonzero = [9*k+i for k, block in enumerate(selection['entry_support']) for i, v in enumerate(block) if v] + allowed = sum(1 << i for i in nonzero) + equations, equations_seen = [], set() + for record in records: + if record['frame'] == selection['frames'][record['column']]: + continue + terms = [(mask, value) for mask, value in record['poly'].items() if not mask & ~allowed] + if not terms: + continue + assert len(terms) != 1, 'Boolean support should exclude lone unwanted terms' + if len(terms) > 2: + return {'status': 'nonbinomial', 'largest_active_sum': len(terms)} + assert all(coefficient == 1 for _, coefficient in terms) + a, b = terms[0][0], terms[1][0] + row = tuple(((a >> i) & 1)-((b >> i) & 1) for i in nonzero) + if next(v for v in row if v) < 0: + row = tuple(-v for v in row) + if row not in equations_seen: + equations_seen.add(row) + equations.append(list(row)) + return {'status': 'binomial', 'matrix': equations, 'rhs_parity': [1]*len(equations), + 'nonzero_entries': nonzero, 'blocks': blocks} + + +def diagonalize(matrix, rhs, n): + """Unimodular row/column Euclidean operations, with an explicit trace. + + Divisibility between successive diagonal entries is unnecessary. Column + operations give x_j=product(z_k**V[j,k]); row operations transform rhs. + """ + a = [list(row) for row in matrix] + b = list(rhs) + v = [[int(i == j) for j in range(n)] for i in range(n)] + m, steps, k = len(a), [], 0 + def swap_rows(i, j): + a[i], a[j], b[i], b[j] = a[j], a[i], b[j], b[i] + steps.append(['row_swap', i, j]) + def swap_columns(i, j): + for row in a: + row[i], row[j] = row[j], row[i] + for row in v: + row[i], row[j] = row[j], row[i] + steps.append(['col_swap', i, j]) + while k < min(m, n): + pivot = next(((i, j) for i in range(k, m) for j in range(k, n) if a[i][j]), None) + if pivot is None: + break + if pivot[0] != k: + swap_rows(k, pivot[0]) + if pivot[1] != k: + swap_columns(k, pivot[1]) + while True: + row = next((i for i in range(k+1, m) if a[i][k]), None) + if row is not None: + amount = -(a[row][k] // a[k][k]) + a[row] = [x+amount*y for x, y in zip(a[row], a[k])] + b[row] += amount*b[k] + steps.append(['row_add', row, k, amount]) + if a[row][k]: + swap_rows(k, row) + continue + col = next((j for j in range(k+1, n) if a[k][j]), None) + if col is not None: + amount = -(a[k][col] // a[k][k]) + for line in a: + line[col] += amount*line[k] + for line in v: + line[col] += amount*line[k] + steps.append(['col_add', col, k, amount]) + if a[k][col]: + swap_columns(k, col) + continue + break + if a[k][k] < 0: + a[k] = [-x for x in a[k]] + b[k] = -b[k] + steps.append(['row_negate', k]) + k += 1 + assert all(not a[i][j] for i in range(m) for j in range(n) if i != j or i >= k) + return {'rank': k, 'diagonal': [a[i][i] for i in range(k)], 'rhs': b, + 'column_transform': v, 'steps': steps} + + +def multiply(a, b): + out = {} + for ea, ca in a.items(): + for eb, cb in b.items(): + exponent = tuple(x+y for x, y in zip(ea, eb)) + out[exponent] = out.get(exponent, 0)+ca*cb + return {e: c for e, c in out.items() if c} + + +def determinant_product(equations, diagonal, signs): + transform = diagonal['column_transform'] + rank = diagonal['rank'] + dimension = len(transform)-rank + entries = {} + for i, index in enumerate(equations['nonzero_entries']): + phase = sum(transform[i][j]*signs[j] for j in range(rank)) % 2 + entries[index] = (tuple(transform[i][rank:]), (-1)**phase) + total = {(0,)*dimension: 1} + for k in range(equations['blocks']): + determinant = {} + for p in permutations(range(3)): + factors = [entries.get(9*k+3*r+p[r]) for r in range(3)] + if any(f is None for f in factors): + continue + parity = sum(p[i] > p[j] for i in range(3) for j in range(i+1, 3)) + exponent = tuple(sum(f[0][j] for f in factors) for j in range(dimension)) + coefficient = (-1)**parity + for factor in factors: + coefficient *= factor[1] + determinant[exponent] = determinant.get(exponent, 0)+coefficient + determinant = {e: c for e, c in determinant.items() if c} + total = multiply(total, determinant) + if not total: + break + return total, entries + + +def nonzero_point(polynomial, dimension): + current, point = polynomial, [] + assert current + for i in range(dimension): + degree = max(e[i] for e in current)-min(e[i] for e in current) + for value in range(1, degree+2): + substituted = {} + for exponent, coefficient in current.items(): + e = (*exponent[:i], 0, *exponent[i+1:]) + substituted[e] = substituted.get(e, 0)+coefficient*Q(value)**exponent[i] + substituted = {e: c for e, c in substituted.items() if c} + if substituted: + point.append(value) + current = substituted + break + else: + raise AssertionError('a nonzero Laurent polynomial lost all degree+1 points') + assert list(current) == [(0,)*dimension] + return point + + +def complete(program, selection): + eq = equations(program, selection) + if eq['status'] != 'binomial': + return None, eq + diag = diagonalize(eq['matrix'], eq['rhs_parity'], len(eq['nonzero_entries'])) + result = {'equations': eq, 'diagonalization': diag, 'components': []} + if any(b % 2 for b in diag['rhs'][diag['rank']:]): + result['status'] = 'inconsistent_torus' + return None, result + roots = [] + for d, b in zip(diag['diagonal'], diag['rhs']): + if d == 1: + roots.append([b % 2]) + elif d == 2 and b % 2 == 0: + roots.append([0, 1]) + else: + result.update(status='nonreal_torsion_pending', pending_diagonal=d, pending_rhs=b) + return None, result + if sum(len(r) == 2 for r in roots) > 10: + result['status'] = 'component_limit' + return None, result + for signs in product(*roots): + polynomial, entries = determinant_product(eq, diag, signs) + result['components'].append({'signs': list(signs), 'determinant_product_zero': not polynomial}) + if not polynomial: + continue + dimension = len(diag['column_transform'])-diag['rank'] + point = nonzero_point(polynomial, dimension) + matrices = [[Q(0)]*9 for _ in range(eq['blocks'])] + for index, (exponent, coefficient) in entries.items(): + value = Q(coefficient) + for z, e in zip(point, exponent): + value *= Q(z)**e + assert value + matrices[index//9][index % 9] = value + word, k = [], 0 + for gate in program: + if gate[0] == 'mix3': + word.append(('mix3', *matrices[k])) + k += 1 + else: + word.append(gate) + result.update(status='exact_rational_point', free_point=point, matrices=[[str(v) for v in m] for m in matrices]) + return tuple(word), result + result['status'] = 'all_components_singular' + return None, result diff --git a/research/clifford-relation-obstructions/verify.py b/research/clifford-relation-obstructions/verify.py new file mode 100644 index 0000000000..471993bad0 --- /dev/null +++ b/research/clifford-relation-obstructions/verify.py @@ -0,0 +1,237 @@ +"""Replay 33 fixed-word exclusions and mathematical positive/negative controls.""" +if not __debug__: + raise SystemExit('Verification requires assertions; run Python without -O.') + +from collections import Counter +from copy import deepcopy +from hashlib import sha256 +from itertools import permutations +import gzip +import json +from pathlib import Path + +from model import (Engine, IDENTITY, FREE, decode, generic_paths, + coefficient_records, execute, endpoint_frames, pauli_image) +from independent import (path_rows, layers, group, rank_formula, + binomial_certificate, diagonal_trace) +from support import encode_support, verify, selected_support, solve +from rank_support import compile_support as strengthened +from torus import equations, complete, diagonalize +import dense + +ROOT = Path(__file__).resolve().parent + + +def block_selection(cnf, selection): + clause = [] + for i, label in enumerate(cnf['labels']): + if not label: + continue + if label[0] == 'entry': + _, k, r, c = label + clause.append(-i if selection['entry_support'][k][3*r+c] else i) + elif label[0] == 'frame' and selection['frames'][label[1]] == label[2]: + clause.append(-i) + return clause + + +def check_dense(program): + ring = Engine() + rows = execute(ring, program) + wanted = [{(key & 3, ring.groups[key >> 2]): value for key, value in row.items()} for row in rows] + assert wanted == dense.execute(program) + for i, tableau in enumerate(ring.groups): + assert ring.frames(i) == dense.independent_frame(tableau) + return ring, rows + + +def check_template(template, counts, dense_check=True): + program, answer = decode(template['program']), template['result'] + assert sum(g[0] == 'paid' for g in program) == 8 + assert sum(g[0] == 'mix3' for g in program) == 3 + ring = Engine() + rows, blocks = path_rows(ring, program) + assert (rows, blocks) == generic_paths(ring, program, 3) + records, targets = coefficient_records(ring, rows) + cnf = rank_formula(program, encode_support(records, targets, blocks)) + assert cnf == strengthened(program) + assert sha256(json.dumps(cnf, sort_keys=True).encode()).hexdigest() == answer['cnf_sha256'] + assert answer['status'] == 'excluded' and answer['steps'] + for number, step in enumerate(answer['steps']): + result = step['support'] + counts['boolean_proof_nodes'] += verify(cnf, result) + counts['support_models_or_refutations'] += 1 + if result['status'] == 'support_obstruction': + assert number == len(answer['steps'])-1 + continue + assert result['status'] == 'support_feasible' + selection = selected_support(cnf, result) + assert selection == step['selection'] + arithmetic = step['binomial'] + assert arithmetic['status'] in ('all_components_singular', 'inconsistent_torus') + binomial_certificate(equations(program, selection), arithmetic) + assert step['blocking_clause'] == block_selection(cnf, selection) + cnf['clauses'].append(step['blocking_clause']) + counts['exact_torus_refutations'] += 1 + assert answer['steps'][-1]['support']['status'] == 'support_obstruction' + if 'defining_words' in template: + words = {name: decode(word) for name, word in template['defining_words'].items()} + def unary(word): + return group(ring, layers(word)[0][0]) + pq = unary(words['Q']+words['P']) + assert pq == unary(words['T']+words['Q']) + assert pq != unary(words['P']+words['Q']) + assert ring.frame_info(pq)[1] == template['shared_product_rank'] + assert template['q_calls'] in (1, 2) + assert sum(g[0] == 'paid' for g in words['Q']) == template['q_calls'] + counts['noncommuting_relations'] += 1 + if dense_check: + literal = tuple(('mix3', 2, 1, 0, 1, 1, 1, 0, 1, 1) if g[0] == 'mix3' else g for g in program) + check_dense(literal) + counts['dense_skeleton_checks'] += 1 + counts['excluded_templates'] += 1 + + +def actual_boolean_model(cnf, program): + ring = Engine() + frames = endpoint_frames(ring, execute(ring, program)) + assert frames is not None + matrices = [g[1:] for g in program if g[0] == 'mix3'] + active = sum(1 << (9*k+i) for k, matrix in enumerate(matrices) for i, value in enumerate(matrix) if value) + model = [] + for label in cnf['labels'][1:]: + kind, *args = label + if kind == 'entry': + k, r, c = args + value = bool(matrices[k][3*r+c]) + elif kind == 'matching': + k, permutation = args + value = all(matrices[k][3*r+permutation[r]] for r in range(3)) + elif kind == 'frame': + column, frame = args + value = frames[column] == frame + elif kind == 'term': + mask, = args + value = not mask & ~active + else: + assert kind == 'rank_matching' + variable = len(model)+1 + guards = [c[1] for c in cnf['clauses'] if len(c) == 2 and c[0] == -variable] + value = all(model[g-1] for g in guards) + model.append(int(bool(value))) + result = {'status': 'support_feasible', 'model': model, 'proof': None} + verify(cnf, result) + return selected_support(cnf, result) + + +def det3(matrix): + total = 0 + for p in permutations(range(3)): + value = (-1)**sum(p[i] > p[j] for i in range(3) for j in range(i+1, 3)) + for r in range(3): + value *= matrix[3*r+p[r]] + total += value + return total + + +def reject(action): + try: + action() + except (AssertionError, ValueError, KeyError, IndexError): + return + raise AssertionError('corrupt or ineligible witness accepted') + + +def controls(templates, counts): + for op in FREE+tuple(('C', v, 0) for v in range(1, 8)): + matrix = dense.operator(op) + for generator in IDENTITY: + assert dense.multiply(matrix, dense.pauli(generator)) == dense.multiply(dense.pauli(pauli_image(op, generator)), matrix) + counts['dense_generator_identities'] += 1 + for v in range(1, 8): + assert dense.multiply(dense.operator(('C', v, 0)), dense.operator(('C', v, 0))) == dense.pauli(v) + counts['paid_square_identities'] += 1 + for trial, axes in enumerate(((1, 2, 4), (3, 2, 4), (1, 6, 4), (5, 2, 4))): + a = ('mix3', 1, 1, 0, 0, 1, 1, 1, 0, 1) + b = ('mix3', 1, 0, 0, 0, trial+1, 0, 0, 0, -1) + c = ('mix3', 2, 1, 0, 1, 1, 1, 0, 1, 1) + u, v = ((), (axes[0],), axes[:2]), (axes, axes[1:], axes[2:]) + word = tuple([a]+[('paid', r, x) for r, unit in enumerate(u) for x in unit] + +[b]+[('paid', r, x) for r, unit in enumerate(v) for x in unit]+[c]) + ring, rows = check_dense(word) + assert endpoint_frames(ring, rows) is not None + assert all(det3(g[1:]) for g in word if g[0] == 'mix3') + selection = actual_boolean_model(strengthened(word), word) + candidate, result = complete(word, selection) + assert candidate is not None and result['status'] == 'exact_rational_point' + assert all(det3(g[1:]) for g in candidate if g[0] == 'mix3') + ring, rows = check_dense(candidate) + assert endpoint_frames(ring, rows) is not None + binomial_certificate(equations(word, selection), result) + counts['positive_nine_call_controls'] += 1 + counts['dense_positive_checks'] += 2 + if trial == 0: + for removed, wanted in ((1, 'support_feasible'), (6, 'support_obstruction')): + bad = word[:removed]+word[removed+1:] + ring, rows = check_dense(bad) + assert endpoint_frames(ring, rows) is None + cnf = strengthened(bad) + test = solve(cnf, seconds=2) + assert test['status'] == wanted + verify(cnf, test) + counts['relaxation_false_positive' if wanted == 'support_feasible' else 'negative_eight_call'] += 1 + for matrix, rhs in (([[2]], [1]), ([[1], [1]], [0, 1]), ([[2, 3], [4, 6]], [1, 0])): + eq = {'matrix': matrix, 'rhs_parity': rhs, 'nonzero_entries': list(range(len(matrix[0])))} + trace = diagonalize(matrix, rhs, len(matrix[0])) + diagonal_trace(eq, trace) + counts['integer_trace_controls'] += 1 + forged = deepcopy(trace) + forged['rhs'][0] += 1 + reject(lambda: diagonal_trace(eq, forged)) + counts['corrupt_integer_traces_rejected'] += 1 + fixture = {'clauses': [[1, 2], [1, -2], [-1, 2], [-1, -2]], 'variables': 2} + result = solve(fixture) + verify(fixture, result) + node = result['proof'] + while 'conflict' not in node: + node = node['positive'] + node['conflict'] = 0 + reject(lambda: verify(fixture, result)) + counts['corrupt_boolean_proofs_rejected'] += 1 + source = next(t for t in templates if len(t['result']['steps']) > 1) + forged = deepcopy(source) + forged['result']['steps'][0]['blocking_clause'].pop() + reject(lambda: check_template(forged, Counter(), False)) + counts['corrupt_learned_clauses_rejected'] += 1 + forged = deepcopy(source) + forged['result']['steps'].pop() + reject(lambda: check_template(forged, Counter(), False)) + counts['missing_final_refutations_rejected'] += 1 + eq = {'matrix': [[2]], 'rhs_parity': [1], 'nonzero_entries': [0], 'blocks': 3} + false = {'status': 'all_components_singular', 'equations': eq, + 'diagonalization': diagonalize([[2]], [1], 1), 'components': []} + reject(lambda: binomial_certificate(eq, false)) + counts['unsupported_torsion_exclusions_rejected'] += 1 + + +def main(): + manifest = json.loads((ROOT/'MANIFEST.json').read_text(encoding='utf-8')) + for name, wanted in manifest['files_sha256'].items(): + assert sha256((ROOT/name).read_bytes()).hexdigest() == wanted, name + raw = gzip.decompress((ROOT/'certificates.json.gz').read_bytes()) + assert sha256(raw).hexdigest() == manifest['certificate_payload_sha256'] + data = json.loads(raw) + assert data['schema'] == 1 and len(data['templates']) == 33 + assert len({t['id'] for t in data['templates']}) == 33 + counts = Counter() + for template in data['templates']: + check_template(template, counts) + controls(data['templates'], counts) + assert counts['excluded_templates'] == 33 and counts['exact_torus_refutations'] == 78 + assert counts['noncommuting_relations'] == 32 + print(json.dumps({'status': 'PASS_FIXED_CLIFFORD_WORD_EXCLUSIONS', + 'counts': dict(counts), 'certificate_payload_sha256': sha256(raw).hexdigest()}, indent=2)) + + +if __name__ == '__main__': + main()