diff --git a/research/three-swap-compression-seed6/CERTIFICATES.json.gz b/research/three-swap-compression-seed6/CERTIFICATES.json.gz new file mode 100644 index 0000000000..2f45bc5ac6 Binary files /dev/null and b/research/three-swap-compression-seed6/CERTIFICATES.json.gz differ diff --git a/research/three-swap-compression-seed6/CLAIM.md b/research/three-swap-compression-seed6/CLAIM.md new file mode 100644 index 0000000000..d70ad6eaae --- /dev/null +++ b/research/three-swap-compression-seed6/CLAIM.md @@ -0,0 +1,8 @@ +CLAIM +Track: bit supplier; OS assignment seed 6. +Base: ef5f39403610d231a0c27e8a6b4f08c10209bcd6. +Question: can a fourth restored dirty register reduce three coordinate-SWAP targets below nine paid coordinate-CNOT calls in the formal F2[GL2(F2)] model? +Predecessors: @commdata2338 PR1414 at 9e1640094f649ba6db9742796825a8d6c238989b and PR1491 at 69638b36c691d3e1b8463526fd68c849e8d1aef9. The latter covers exactly three registers. This changes the availability of a restored dirty extra register and uses rank compression/constraint solving, not a larger unnormalized Cayley census. +Method/domain: prove any seven-call arbitrary-workspace counterexample compresses to at most four roles; normalize the three equally labeled rank-one projector image vectors; exactly encode all 35 seven-letter patterns with three a/four b calls. Seed6 rotates the processing order. First price the optimistic call alphabet: nine is baseline, seven would be a relaxed saving; scalar basis changes remain free only in this relaxation. +Expected artifact: checked compression proof and bounded exact solver evidence or witness; no physical supplier, precision/hosting admission or kappa claim. A timeout or failed search will not be called an impossibility result. +Expected finish: 2026-10-14T02:57:00Z. Experiment cutoff: 02:42Z, reserving the last 15 minutes for verification. Claim expires: 03:57Z. diff --git a/research/three-swap-compression-seed6/PROOF.md b/research/three-swap-compression-seed6/PROOF.md new file mode 100644 index 0000000000..9a1e4dfc6d --- /dev/null +++ b/research/three-swap-compression-seed6/PROOF.md @@ -0,0 +1,188 @@ +# Three coordinate swaps: arbitrary dirty workspace costs nine calls + +This is a computer-assisted theorem in the exact formal register model of +commdata2338's PR1414 and PR1491. The written rank-compression argument is the +arbitrary-register step. The 35 checked CNF/DRUP certificates are an essential +finite premise. Neither part is a multiplication theorem or an unconditional +lower bound for bit circuits. + +## Model and claim + +Let `G=GL_2(F2)`, `R=F2[G]`, and + +``` +a = [[1,1],[0,1]], b = [[1,0],[1,1]], s = aba = bab = [[0,1],[1,0]]. +``` + +Registers are arbitrary R-module inputs. For any finite register count r, +allow free scalar `GL_r(F2)` changes and paid units + +``` +D_N(g) = I + ([g]+1) N, g in {a,b}, +N = u v^T over F2, v^T u = 1. +``` + +Each paid occurrence costs one; inverses are paid. There are no other free +address operations, copies, erasures, overwrites or clean allocations. With +`P=diag(I_t,0)`, t active coordinate swaps request the complete formal map + +``` +T_t = I + ([s]+1) P. +``` + +Every one of the remaining r−t registers starts arbitrarily dirty and is +returned identically; all original dirty coordinates have the stated map. +Equality is in `M_r(R)`, not only the natural 2r-dimensional representation. + +**Theorem.** For every finite r≥3, three active swaps require exactly **nine** +paid calls, even with arbitrary free scalar mixing and restored dirty extras. + +The attaining word needs only the three active registers. The lower bound +uses a stronger free-scalar relaxation than a physical supplier may admit. +The complete paid bill is nine including undo work; no free source access, +frame conversion or coefficient preparation is asserted for a physical +implementation. This closes the arbitrary-workspace three-target question +left by PR1414 and the exactly-three-register certificate PR1491. + +## 1. Normalize scalar work and use sign parity + +As in PR1414, move scalar basis changes to the right; they conjugate each N +and preserve its rank-one idempotence. The augmentation `[g] -> 1` sends every +paid unit and T_t to I, so the final scalar factor must be I. All free mixing +is therefore represented by the choices of u,v in the paid factors. + +The sign map `G=S3 -> C2`, with characteristic-two algebra +`F2[C2]=F2[epsilon]/(epsilon^2)`, sends each paid factor to `I+epsilon N` and +T_t to `I+epsilon P`. Therefore `sum N_i=P`. Since `trace N_i=v_i^T u_i=1`, + +``` +number of paid calls = t modulo 2. +``` + +For t=3 a word shorter than nine has odd length at most seven. + +## 2. General role-compression lemma + +**Lemma.** Any q-call word for T_t has an equivalent q-call word on at most +q−t registers, retaining t active swaps and restored dirty extras. Moreover +the number of a calls and the number of b calls are each at least t. + +Let U_a be the span of the image vectors u_i of a-labeled calls, and U_b the +span for b-labeled calls. Apply the natural address representation of G to +2r coordinates, ordered by their two address components. The paid factors +become block shears + +``` +a: [[I,N],[0,I]], b: [[I,0],[N,I]]. +``` + +The target is + +``` +[[I+P, P], [P, I+P]]. +``` + +Follow chronological left multiplication. Only a calls change the top block +row, and each change has output image contained in the corresponding line +span(u_i). The top-right block initially vanishes and ends at P. Thus +`im P <= U_a`. Likewise the bottom-left block gives `im P <= U_b`. This is a +necessary consequence of a formal word, with no claim that this address +representation is faithful. + +If n_a and n_b are the two label counts, then + +``` +n_a >= t, n_b >= t, +dim(U_a+U_b) <= dim U_a+dim U_b−t <= n_a+n_b−t = q−t. +``` + +Set C=U_a+U_b. Every image vector u_i belongs to C, so each projector N_i +preserves C. Its restriction still has rank one and is idempotent: +`u_i in C` and `v_i^T u_i=1`, so `v_i|C` is nonzero. Also P preserves C because +`im P <= C`. Restrict the complete formal identity to C. Since P is an +idempotent of rank t on C, choose a scalar basis + +``` +C = im P direct-sum (C intersect ker P). +``` + +The restricted endpoint is exactly t swaps plus identity on the other +`dim C−t` dirty registers. All restricted paid units are members of the same +alphabet. No clean scratch is introduced. This proves the lemma for arbitrary +finite r and arbitrary R-module inputs. + +## 3. Seven calls reduce to 35 normalized four-register patterns + +The label-count part of the lemma gives at least six calls for t=3; parity +leaves only seven below nine. At seven, the label counts are (3,4) or (4,3), +and the compressed register count is at most four. + +Conjugating address maps by s exchanges a and b while preserving the target +s. Hence assume three a calls and four b calls. Because the three a image +vectors span im P, they are linearly independent and constitute a basis of +that three-dimensional active space. A single scalar basis change, chosen +inside im P and extended on `C intersect ker P`, sends these vectors, in their +word order, to e0,e1,e2. It leaves P unchanged. If dim C=3, append a fourth +identity register with arbitrary dirty input and zero coupling. + +Consequently every seven-call arbitrary-workspace counterexample has a +four-register representative with the three a image vectors fixed at +e0,e1,e2. All v vectors remain arbitrary subject to `v^T u=1`; every b factor +has all four-bit u,v choices. The fourth register must be returned identically. +There are exactly `binomial(7,3)=35` a/b label patterns. These reductions do +not identify patterns by an unproved cyclic, time or symmetry quotient. + +## 4. Exact finite encoding and certificate check + +`cnf.py` independently realizes G as permutations of the three nonzero +binary address vectors. For each label pattern it builds a Boolean formula +for all source u,v bits and all formal coefficients of the four-register +product. The three normalized a image vectors are constants. Every projector +has the exact `v^T u=1` constraint. All 96 output coefficient bits (six group +labels times sixteen matrix entries) are constrained to T_3, including the +fourth dirty register and every possible leakage coefficient. + +For chronological left multiplication, if S_h is the scalar matrix at group +label h, define `w_h,j = sum_k v_k S_h,k,j`. A g call updates + +``` +S'_h,i,j = S_h,i,j + u_i (w_h,j + w_(g*h),j). +``` + +Here g is an involution. XOR and AND use Tseitin clauses with both directions +of equivalence, not one-way implications. Every choice of admissible u,v has +exactly its induced state extension; satisfiability is equivalent to the +normalized word's existence. The original clauses have no heuristic cuts. + +All 35 formulas are UNSAT. The supplied `CERTIFICATES.json.gz` contains the +literal clauses and proof records. `verify.py` rebuilds every formula and +requires exact equality. It checks each added proof clause by unit propagation +under the negation of that clause, using only the original clauses and earlier +validated additions. Deletion records are ignored; every retained clause is +already a consequence of the original formula, so retaining it is sound. +Every certificate must derive the empty clause. No SAT solver is used by this +replay. The proof-producing run used python-sat 1.8.dev24 / Glucose3; the +separate Boolean right-product encoding used Z3 4.13.4.0 and also returned +35 UNSAT results without timeout. That independent run is corroboration; +the checked RUP certificates supply the finite premise. + +The checker tests its watched propagation against a separate slow implementation +on all two-variable clause sets and all consistent literal assumptions, and +rejects invalid and incomplete proofs. Exact Tseitin truth-table controls and +a satisfying assignment for the full nine-call construction guard encoding +vacuity. Natural-representation-only equality is explicitly rejected as an +insufficient endpoint test. + +Combining all 35 exclusions with Sections 1–3 eliminates every word shorter +than nine on any finite dirty workspace. This is a computer-assisted scoped +theorem; neither the written argument nor the checker is verified in Lean. + +## 5. Nine calls attain the entire dirty boundary + +For any scalar idempotent N, direct expansion gives +`D_N(g) D_N(h) = D_N(gh)`. Apply b,a,b to each of the three distinct coordinate +projectors E00,E11,E22. Since `bab=s`, each active register undergoes exactly +its required swap; all other registers remain identity. There are nine paid +calls, no scratch registers, no scalar basis changes and no omitted restoration. +The literal formal word and its faithful 24-column regular representation +are checked in the replay. This proves the upper bound and finishes the theorem. diff --git a/research/three-swap-compression-seed6/README.md b/research/three-swap-compression-seed6/README.md new file mode 100644 index 0000000000..df66217d53 --- /dev/null +++ b/research/three-swap-compression-seed6/README.md @@ -0,0 +1,173 @@ +# Three swaps with arbitrary restored dirty registers cost nine calls + +**Scoped computer-assisted negative theorem; no new κ.** In the formal +`F2[GL_2(F2)]` coordinate-CNOT register model, three coordinate-SWAP targets +require exactly **nine paid calls**, for any finite number of restored dirty +registers, even with arbitrary free scalar mixing. The explicit nine-call +word uses only the three active registers and restores the full boundary. + +The new arbitrary-register step is a general compression lemma: a q-call word +for t swaps compresses to at most q−t registers. For three targets, parity and +address-representation rank leave only seven-call improvements; they compress +to four registers. Normalizing one label's three image vectors gives exactly +35 cases. Every case has a supplied UNSAT proof checked by two implementations. +The result rules out shared work in this specific optimistic alphabet. It is +not a lower bound for physical bit suppliers or other operation alphabets. + +This addresses the arbitrary-workspace question in commdata2338's +[#1414](https://github.com/CrocSwap/integer-mult-bounds/pull/1414), pinned at +`9e1640094f649ba6db9742796825a8d6c238989b`, and extends the register-count scope +of their [#1491](https://github.com/CrocSwap/integer-mult-bounds/pull/1491), pinned +at `69638b36c691d3e1b8463526fd68c849e8d1aef9`. #1491 proves nine for exactly +three registers by a different Cayley census. Our proof does not import its +finite enumeration or rely on its lower-bound conclusion. No priority claim +is made for the formal model, sign quotient or the nine-call upper bound. + +## Exact scope and complete paid comparison + +The [proof](PROOF.md) defines every operation. A paid factor is +`I+([g]+1)uv^T`, with `g=a or b` and `v^T u=1` over F2. Each occurrence, +including an inverse, costs one. Extra registers start arbitrarily dirty and +must return identically, with no leakage to active outputs. Scalar register +basis changes are free in the lower-bound relaxation; no address operations, +COPY/ERASE, clean rows, overwrites or data-dependent choices are free. + +Baseline: three calls `b,a,b` on each active coordinate projector, nine total. +The proposed seven-call shared alternative would save two in this optimistic +model. The exact certificates exclude it, including the fourth dirty row. +The attaining word needs no scalar preparation, helper allocation or deferred +restoration. A physical compiler would still price every complete address +call, coefficient/source access, frames, tape, precision and hosting. Such a +compiler or supplier recurrence is not provided; no multiplication endpoint +is inferred from unit paid-call counts. + +## New proof mechanism + +Apply the natural two-coordinate representation only as a necessary condition. +Let U_a and U_b span the paid projector image vectors for the two labels. +The target's top-right and bottom-left blocks both have image im(P), of +dimension t, so `im(P) <= U_a intersect U_b`. Therefore + +``` +dim(U_a+U_b) <= q−t. +``` + +Every paid projector and P preserves this subspace. Restriction retains +rank-one idempotence and exactly the same formal target on t active roles +plus restored dirty extras. This proves compression for arbitrary finite +workspace. At q=7,t=3, the smaller label count is three, and those three image +vectors form a basis of im(P). One scalar basis change fixes them at e0,e1,e2. +Exchanging address coordinates covers the reverse label counts. There are +`binomial(7,3)=35` remaining seven-letter patterns; none is omitted by a +heuristic or cyclic quotient. + +For each pattern, all normalized projector choices are covered: eight choices +per fixed-image a projector and 120 choices per b projector. The constraint +proof covers the resulting Boolean domain; it is not a brute-force enumeration +of the corresponding 106,168,320,000 tuples per pattern. + +## Evidence and verification + +[CERTIFICATES.json.gz](CERTIFICATES.json.gz) contains all 35 exact CNFs and +DRUP proof logs. The decompressed payload SHA256 is +`90a23d6b20de8329e3db9e7555d1fb81a8c99edf5a4a76f9cd0ac1058b0b7ffa`. +Container bytes need not match across gzip versions: proof-relevant content +and rebuilt clauses are checked exactly. + +- `cnf.py` builds a left-product formal group-algebra encoding, including all + 96 output coefficient bits and every fourth-register leakage coefficient. +- `verify.py` rebuilds every CNF and checks every proof by reverse unit + propagation. All 161,432 original clauses and 3,836 validated additions are + covered. Deletions are safely ignored because retained validated clauses + remain consequences of the original formula. +- `independent.py` imports no encoder or watched checker. It checks all proof + additions again with a separate scanning propagation engine, and the + complete 24-column faithful regular boundary for one/two/three-swap words. +- `search.py` independently encodes right products using Boolean Z3 state + variables and explicit 2x2 address matrices. It returns UNSAT on all 35 + patterns, with no timeouts. [SEARCH.json](SEARCH.json) records that completed + bounded run; it is corroboration, not the proof trusted by replay. +- Controls reject invalid or unfinished proofs and an incorrect paid label. + Exact truth tables check both directions of Tseitin equivalence. Watched + and scanning unit propagation agree on all 2,304 two-variable cases. An + explicit satisfying assignment checks the actual nine-call CNF. A natural + representation kernel fixture demonstrates why that representation alone + does not certify a formal endpoint. + +Proof generation used python-sat 1.8.dev24 / Glucose3's +[DRUP interface](https://pysathq.github.io/docs/html/api/solvers.html). +The optional independent SMT run used z3-solver 4.13.4.0. Neither dependency +is needed to verify the committed certificates. No Lean or human review is +claimed. The written compression argument supplies the unbounded-register +step; finite solver output alone would not establish that step. + +## Reproduce + +From repository root, Python 3.12 and the standard library: + +```sh +python3.12 scripts/research_package.py --package research/three-swap-compression-seed6 +``` + +Expected: `PASS_THREE_SWAP_COMPRESSION`, +`PASS_INDEPENDENT_THREE_SWAP_COMPRESSION`, and +`PASS_REGISTERED_RESEARCH_PACKAGE ... outcome=negative-result`. +The development host took about two seconds for the watched replay and +35 seconds for the independent scanning replay. Wall times are observations, +not performance guarantees. Both checks also pass with Python assertions off. + +Optional regeneration of this package's certificates and the independent SMT +run, using the pinned [build dependencies](requirements-build.txt): + +```sh +python3.12 -m venv /tmp/three-swap-build +/tmp/three-swap-build/bin/pip install -r research/three-swap-compression-seed6/requirements-build.txt +/tmp/three-swap-build/bin/python research/three-swap-compression-seed6/generate.py +/tmp/three-swap-build/bin/python research/three-swap-compression-seed6/search.py --output /tmp/three-swap-search.json +``` + +A newly generated proof need not have the same clause sequence; it must be +validated and retain the complete 35-case domain. Regeneration touches only +this package. Immutable predecessor sources are not changed. + +## Assignment, sources and limits + +OS seed **6**, bit-supplier track. Exact base: +`ef5f39403610d231a0c27e8a6b4f08c10209bcd6`. The seed rotates the solver processing +order starting at case six. The new question is the restored extra register +and rank compression, not a different optimizer seed. [TASK.json](TASK.json) +records the three candidate scopes, overlap, stopping rule and next questions; +[SOURCES.json](SOURCES.json) pins the model predecessors and historical state. +The [claim](CLAIM.md) is Discussion #1514. + +The selected #1094 frontier, selected PR589 bit supplier and `upstream/` are +unchanged. Full selected cold replay and repository-wide artifact regeneration +were not run for this isolated proof package. Physical/all-size compiler, +common-label, hosting, precision/tape, analytic and bit H1–H5 obligations +remain inherited. The theorem concerns formal group-algebra equality for +arbitrary modules; a different physical address representation or paid +alphabet needs its own argument. + +## Open next questions + +For four active swaps, an eight-call counterexample can be padded with a +canceling paid pair to ten calls; compression bounds a ten-call counterexample +to at most six registers. First separate the 4/6 and 5/5 label-count cases: only the former +has a full fixed-image basis normalization. An exact encoding and checked +proof or witness would decide the next instance; no larger-target conclusion +is implied here. Separately, a physical compiler must price free scalar work +before any formal-model witness could imply a supplier gain. Structured first +steps and blockers are in TASK.json. + +## Credit and license + +Prepared by Cinna Davis (`1337isnot1337`) with substantial OpenAI Codex +assistance in proof, implementation, verification and writing. New work is +Apache-2.0. Credit commdata2338 for #1414/#1491's formal nonabelian model, +normalization, sign parity, earlier finite results and questions; Gareth +Davidson's #1333 for the scalar-mixing paid-call relaxation; and Ali Romman's +[three-register abelian obstruction](../bit-three-register-lower-bound/README.md) +as the task's model-change starting point. The selected bit lineage remains +credited to DreamingOfClouds/eumemic and its supplier/review contributors. +No predecessor executable implementation is imported. PySAT/Glucose and Z3 +are optional proof-generation tools and retain their respective licenses. diff --git a/research/three-swap-compression-seed6/SEARCH.json b/research/three-swap-compression-seed6/SEARCH.json new file mode 100644 index 0000000000..bdea8cdfd3 --- /dev/null +++ b/research/three-swap-compression-seed6/SEARCH.json @@ -0,0 +1,222 @@ +{ + "engine": "Z3 Boolean coefficient recurrence", + "z3_version": "4.13.4", + "assignment_seed": 6, + "registers": 4, + "active_swap_targets": 3, + "paid_calls": 7, + "timeout_ms_per_pattern": 15000, + "patterns_total": 35, + "results": [ + { + "labels": "abababb", + "status": "unsat", + "elapsed_seconds": 0.160987, + "pattern_index": 6 + }, + { + "labels": "ababbab", + "status": "unsat", + "elapsed_seconds": 0.157935, + "pattern_index": 7 + }, + { + "labels": "ababbba", + "status": "unsat", + "elapsed_seconds": 0.155523, + "pattern_index": 8 + }, + { + "labels": "abbaabb", + "status": "unsat", + "elapsed_seconds": 0.143454, + "pattern_index": 9 + }, + { + "labels": "abbabab", + "status": "unsat", + "elapsed_seconds": 0.143061, + "pattern_index": 10 + }, + { + "labels": "abbabba", + "status": "unsat", + "elapsed_seconds": 0.145243, + "pattern_index": 11 + }, + { + "labels": "abbbaab", + "status": "unsat", + "elapsed_seconds": 0.143274, + "pattern_index": 12 + }, + { + "labels": "abbbaba", + "status": "unsat", + "elapsed_seconds": 0.145884, + "pattern_index": 13 + }, + { + "labels": "abbbbaa", + "status": "unsat", + "elapsed_seconds": 0.139365, + "pattern_index": 14 + }, + { + "labels": "baaabbb", + "status": "unsat", + "elapsed_seconds": 0.15832, + "pattern_index": 15 + }, + { + "labels": "baababb", + "status": "unsat", + "elapsed_seconds": 0.180388, + "pattern_index": 16 + }, + { + "labels": "baabbab", + "status": "unsat", + "elapsed_seconds": 0.158699, + "pattern_index": 17 + }, + { + "labels": "baabbba", + "status": "unsat", + "elapsed_seconds": 0.156362, + "pattern_index": 18 + }, + { + "labels": "babaabb", + "status": "unsat", + "elapsed_seconds": 0.168274, + "pattern_index": 19 + }, + { + "labels": "bababab", + "status": "unsat", + "elapsed_seconds": 0.166889, + "pattern_index": 20 + }, + { + "labels": "bababba", + "status": "unsat", + "elapsed_seconds": 0.16547, + "pattern_index": 21 + }, + { + "labels": "babbaab", + "status": "unsat", + "elapsed_seconds": 0.163895, + "pattern_index": 22 + }, + { + "labels": "babbaba", + "status": "unsat", + "elapsed_seconds": 0.156688, + "pattern_index": 23 + }, + { + "labels": "babbbaa", + "status": "unsat", + "elapsed_seconds": 0.150761, + "pattern_index": 24 + }, + { + "labels": "bbaaabb", + "status": "unsat", + "elapsed_seconds": 0.147084, + "pattern_index": 25 + }, + { + "labels": "bbaabab", + "status": "unsat", + "elapsed_seconds": 0.147823, + "pattern_index": 26 + }, + { + "labels": "bbaabba", + "status": "unsat", + "elapsed_seconds": 0.146633, + "pattern_index": 27 + }, + { + "labels": "bbabaab", + "status": "unsat", + "elapsed_seconds": 0.146029, + "pattern_index": 28 + }, + { + "labels": "bbababa", + "status": "unsat", + "elapsed_seconds": 0.148129, + "pattern_index": 29 + }, + { + "labels": "bbabbaa", + "status": "unsat", + "elapsed_seconds": 0.150947, + "pattern_index": 30 + }, + { + "labels": "bbbaaab", + "status": "unsat", + "elapsed_seconds": 0.145553, + "pattern_index": 31 + }, + { + "labels": "bbbaaba", + "status": "unsat", + "elapsed_seconds": 0.148527, + "pattern_index": 32 + }, + { + "labels": "bbbabaa", + "status": "unsat", + "elapsed_seconds": 0.145756, + "pattern_index": 33 + }, + { + "labels": "bbbbaaa", + "status": "unsat", + "elapsed_seconds": 0.139969, + "pattern_index": 34 + }, + { + "labels": "aaabbbb", + "status": "unsat", + "elapsed_seconds": 0.140685, + "pattern_index": 0 + }, + { + "labels": "aababbb", + "status": "unsat", + "elapsed_seconds": 0.160608, + "pattern_index": 1 + }, + { + "labels": "aabbabb", + "status": "unsat", + "elapsed_seconds": 0.145807, + "pattern_index": 2 + }, + { + "labels": "aabbbab", + "status": "unsat", + "elapsed_seconds": 0.143241, + "pattern_index": 3 + }, + { + "labels": "aabbbba", + "status": "unsat", + "elapsed_seconds": 0.140534, + "pattern_index": 4 + }, + { + "labels": "abaabbb", + "status": "unsat", + "elapsed_seconds": 0.160153, + "pattern_index": 5 + } + ] +} diff --git a/research/three-swap-compression-seed6/SOURCES.json b/research/three-swap-compression-seed6/SOURCES.json new file mode 100644 index 0000000000..ddde2a3b24 --- /dev/null +++ b/research/three-swap-compression-seed6/SOURCES.json @@ -0,0 +1,53 @@ +{ + "schema_version": 1, + "base_commit": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "research/bit-three-register-lower-bound/README.md", + "usage": "provenance", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + }, + { + "path": "docs/research/community-batch1099-review.md", + "usage": "provenance", + "git_blob": "6cb6ec061a071a06a2d18cd4dc3e9a2b05d28099", + "sha256": "7e76d2c38e5fce30587835b7251df1430488ae4dd372611ef69a3f03f476b6cb" + } + ], + "external_predecessors": [ + { + "pr": 1414, + "author": "commdata2338", + "commit": "9e1640094f649ba6db9742796825a8d6c238989b", + "path": "research/coordinate-cnot-register-bound/PROOF.md", + "sha256": "bcee89f92dcce8253bd7eae6e924ddff598c900da81979c6171a412f03d765e1", + "usage": "model/proof attribution; no executable code imported" + }, + { + "pr": 1491, + "author": "commdata2338", + "commit": "69638b36c691d3e1b8463526fd68c849e8d1aef9", + "path": "research/three-swap-cnot-census/PROOF.md", + "sha256": "92ad674b23a526f8251b458f91efd67eef9028d034234acb18503f2775399f90", + "usage": "prior exactly-three-register scope; its finite result is not a premise of the new certificate" + } + ], + "local_certificate": { + "path": "CERTIFICATES.json.gz", + "payload_sha256": "90a23d6b20de8329e3db9e7555d1fb81a8c99edf5a4a76f9cd0ac1058b0b7ffa", + "equality": "Decoded proof-relevant payload and freshly rebuilt clauses; regenerated compressed container equality is not required." + } +} diff --git a/research/three-swap-compression-seed6/TASK.json b/research/three-swap-compression-seed6/TASK.json new file mode 100644 index 0000000000..cd035b7617 --- /dev/null +++ b/research/three-swap-compression-seed6/TASK.json @@ -0,0 +1,111 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 2, + "base_commit": "ef5f39403610d231a0c27e8a6b4f08c10209bcd6", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write a complete operation alphabet outside one named premise and price a baseline before searching identities.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "refined", + "actual_scope": "Prove the q-minus-t role-compression lemma and the nine-call three-SWAP minimum on arbitrary finite restored dirty workspace in the exact F2[GL2(F2)] rank-one-idempotent paid alphabet.", + "scope_change_reason": "Use the nonabelian formal coordinate-CNOT model and change the exactly-three-register premise of PR1491 to arbitrary restored dirty workspace. Rank compression and a normalized CNF/DRUP proof replace a larger unnormalized Cayley search.", + "bottleneck_link": "An extra restored dirty register might share coordinate address work; a seven-call improvement would beat the optimistic nine-call baseline. The exact result excludes that route in this named alphabet, with no physical supplier or kappa implication.", + "budget_minutes": 60, + "stop_rule": "One 60-minute run; orientation <=12 minutes; experiment cutoff 02:42 UTC; complete all 35 normalized seven-letter patterns (15 seconds per SMT case), preserve every certificate, and reserve final 15 minutes for verification. No retries on a closed Cayley class.", + "outcome": "negative-result", + "evidence": "PROOF.md arbitrary-register compression; CERTIFICATES.json.gz all 35 literal CNF/DRUP certificates; both standard-library proof checkers; SEARCH.json independent complete Z3 run.", + "author": "Cinna Davis (1337isnot1337), with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance with proof, encodings, independent certificate checking and prose; no human or Lean verification claimed.", + "open_questions": [ + { + "question": "Do four active swaps admit ten paid calls in this alphabet?", + "why_it_matters": "Compression limits that next candidate to at most six registers, but the three-target conclusion does not settle it.", + "first_step": "Separate the 4/6 and 5/5 label-count cases; normalize the four-image basis only in the former, then derive an exact CNF domain and proof or witness.", + "blocked_by": "No justified normalization of the 5/5 image spans or completed six-register certificate." + }, + { + "question": "Can a different physically realizable address alphabet improve a paid supplier?", + "why_it_matters": "The negative theorem only covers the formal two-coordinate rank-one-idempotent alphabet, with scalar work optimistically free.", + "first_step": "Name a changed legal unit, price complete source/scalar/frame/restoration work, and test an exact dirty-boundary instance.", + "blocked_by": "No physical realization, precision invoice or contracting supplier recurrence." + } + ], + "assignment_track": "bit supplier", + "assignment_seed": 6, + "considered_candidates": [ + { + "scope": "Semantic H2/K bridge on one restored helper-star prefix", + "decision": "Avoided close overlap with PR1311 and the PR1194 semantic prefix-substitution line." + }, + { + "scope": "One later retirement cut or helper470 slot move", + "decision": "Avoided close overlap with PR1271/1393/1480." + }, + { + "scope": "Three coordinate swaps with a restored fourth dirty role, then arbitrary-workspace compression", + "decision": "Chosen: changes the extra-register premise of PR1491 and uses a new rank reduction with independent CNF/RUP evidence." + } + ], + "coordination": { + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1514", + "no_pinned_coordination_issue": true + }, + "overlap": { + "open_pr_records": 756, + "discussion_records": 191, + "limits": "Fresh gh pr list with bodies supplemented find_overlap, whose PR refresh failed because installed gh lacks --slurp. Discussion pagination was complete as reported. No code-diff-wide novelty claim.", + "nearest_prs": [ + { + "number": 1414, + "head": "9e1640094f649ba6db9742796825a8d6c238989b", + "author": "commdata2338", + "scope": "two swaps, arbitrary restored workspace" + }, + { + "number": 1491, + "head": "69638b36c691d3e1b8463526fd68c849e8d1aef9", + "author": "commdata2338", + "scope": "three swaps, exactly three registers" + } + ], + "final_open_pr_records": 781, + "final_predecessor_heads_unchanged": true + }, + "experiment_finished_utc": "2026-10-14T02:22:21Z", + "verification_started_utc": "2026-10-14T02:22:21Z", + "registered_final_replay_started_utc": "2026-10-14T02:29:00Z", + "verification": "Registered replay passed both exact proof checkers, all CNF/gadget/scope controls, source pins, selected-record integrity and diff checks; no selected cold replay or supplier adoption claimed." +} diff --git a/research/three-swap-compression-seed6/VERIFY.json b/research/three-swap-compression-seed6/VERIFY.json new file mode 100644 index 0000000000..e988888e2e --- /dev/null +++ b/research/three-swap-compression-seed6/VERIFY.json @@ -0,0 +1,31 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All 35 exact CNFs, every RUP addition, meaningful soundness/gadget/coverage controls and explicit satisfying nine-call assignment." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/independent.py" + ], + "timeout_seconds": 300, + "checks": "Separate scanning replay of every proof addition and faithful regular dirty-input witness, importing no constructor or watched checker." + } + ] +} diff --git a/research/three-swap-compression-seed6/cnf.py b/research/three-swap-compression-seed6/cnf.py new file mode 100644 index 0000000000..b21a2923ef --- /dev/null +++ b/research/three-swap-compression-seed6/cnf.py @@ -0,0 +1,81 @@ +#!/usr/bin/env python3 +"""Independent left-product Tseitin CNF over a permutation group algebra. +No Z3 dependency. Cinna Davis with OpenAI Codex assistance. Apache-2.0. +""" +import itertools + +GROUP=tuple(itertools.permutations(range(3))) +INDEX={g:i for i,g in enumerate(GROUP)} +IDENT=INDEX[(0,1,2)];A=INDEX[(0,2,1)];B=INDEX[(2,1,0)];SWAP=INDEX[(1,0,2)] +MUL=[[INDEX[tuple(p[q[i]] for i in range(3))] for q in GROUP] for p in GROUP] + +class Formula: + def __init__(self):self.variables=1;self.clauses=[[1]];self.projectors=[];self.operations=[] + def variable(self):self.variables+=1;return self.variables + def clause(self,*lits):self.clauses.append(list(lits)) + def both(self,a,b): + if a==1:return b + if b==1:return a + if a==-1 or b==-1 or a==-b:return -1 + if a==b:return a + t=self.variable();self.operations.append((t,"and",a,b));self.clause(-t,a);self.clause(-t,b);self.clause(t,-a,-b);return t + def xor(self,a,b): + if a==-1:return b + if b==-1:return a + if a==1:return -b + if b==1:return -a + if a==b:return -1 + if a==-b:return 1 + t=self.variable();self.operations.append((t,"xor",a,b)) + for clause in [(-a,-b,-t),(a,b,-t),(a,-b,t),(-a,b,t)]:self.clause(*clause) + return t + def parity(self,values): + out=-1 + for value in values:out=self.xor(out,value) + return out + +def patterns():return [''.join('a' if j in positions else 'b' for j in range(7)) for positions in itertools.combinations(range(7),3)] + +def encode(labels,pinned=None): + f=Formula();r=4;ordinal=0 + state=[[[1 if h==IDENT and i==j else -1 for j in range(r)] for i in range(r)] for h in range(6)] + for step,label in enumerate(labels): + if label=='a':u=[1 if i==ordinal else -1 for i in range(r)];ordinal+=1 + else:u=[f.variable() for _ in range(r)] + v=[f.variable() for _ in range(r)];f.projectors.append((u,v)) + f.clause(f.parity(f.both(u[i],v[i]) for i in range(r))) + if pinned is not None: + for name,values in [('u',u),('v',v)]: + for i,value in enumerate(values):f.clause(value if (pinned[step][name]>>i)&1 else -value) + g=A if label=='a' else B + # Left multiplication, with a row contraction and left group translation. + contracted=[[f.parity(f.both(v[k],state[h][k][j]) for k in range(r)) for j in range(r)] for h in range(6)] + new=[[[0]*r for _ in range(r)] for _ in range(6)] + for h in range(6): + previous=MUL[g][h] # g is an involution + for j in range(r): + change=f.xor(contracted[h][j],contracted[previous][j]) + for i in range(r):new[h][i][j]=f.xor(state[h][i][j],f.both(u[i],change)) + state=new + for h in range(6): + for i in range(r): + for j in range(r): + required=i==j and h==(SWAP if i<3 else IDENT) + f.clause(state[h][i][j] if required else -state[h][i][j]) + return f + +def concrete(word,r=4): + state=[[[int(h==IDENT and i==j) for j in range(r)] for i in range(r)] for h in range(6)] + for gate in word: + u,v,g=gate['u'],gate['v'],A if gate['label']=='a' else B + if not (u and v and (u&v).bit_count()%2):raise ValueError('illegal projector') + previous=state + state=[[row[:] for row in block] for block in previous] + for h in range(6): + for j in range(r): + delta=0 + for k in range(r): + if v>>k&1:delta^=previous[h][k][j]^previous[MUL[g][h]][k][j] + for i in range(r): + if u>>i&1:state[h][i][j]^=delta + return state diff --git a/research/three-swap-compression-seed6/generate.py b/research/three-swap-compression-seed6/generate.py new file mode 100644 index 0000000000..12277c85a0 --- /dev/null +++ b/research/three-swap-compression-seed6/generate.py @@ -0,0 +1,26 @@ +#!/usr/bin/env python3 +"""Generate independent SAT certificates; optional pinned build dependencies. +Cinna Davis with OpenAI Codex assistance. Apache-2.0. +""" +import gzip,json,time +from pathlib import Path +from pysat.solvers import Glucose3 +import pysat +import cnf +ROOT=Path(__file__).resolve().parent +results=[] +for index in list(range(6,35))+list(range(6)): + labels=cnf.patterns()[index];formula=cnf.encode(labels);started=time.monotonic() + with Glucose3(bootstrap_with=formula.clauses,with_proof=True) as solver: + sat=solver.solve();proof=solver.get_proof() + if sat:raise RuntimeError('SAT in independent encoder: '+labels) + # If the formula is contradictory at load time, get_proof may be empty. + # Empty-clause RUP checking still verifies that directly. + if not proof or proof[-1]!='0':proof.append('0') + item={'index':index,'labels':labels,'variables':formula.variables,'clauses':formula.clauses,'proof':proof} + results.append(item) + print(json.dumps({'index':index,'labels':labels,'variables':formula.variables,'clauses':len(formula.clauses),'proof_lines':len(proof),'seconds':round(time.monotonic()-started,6)}),flush=True) +payload={'format':'CNF-and-DRUP-v1','generator':'python-sat '+pysat.__version__+' Glucose3','results':sorted(results,key=lambda x:x['index'])} +raw=(json.dumps(payload,sort_keys=True,separators=(',',':'))+'\n').encode() +with gzip.GzipFile(filename='',mode='wb',fileobj=(ROOT/'CERTIFICATES.json.gz').open('wb'),mtime=0) as stream:stream.write(raw) +print('DONE patterns='+str(len(results))+' payload_bytes='+str(len(raw)),flush=True) diff --git a/research/three-swap-compression-seed6/independent.py b/research/three-swap-compression-seed6/independent.py new file mode 100644 index 0000000000..c2d03e2c6f --- /dev/null +++ b/research/three-swap-compression-seed6/independent.py @@ -0,0 +1,87 @@ +#!/usr/bin/env python3 +"""Independent slow DRUP replay and faithful regular-representation controls. +Imports no constructor, CNF or watched-proof checker. +Cinna Davis with substantial OpenAI Codex assistance. Apache-2.0. +""" +import gzip,itertools,json,time +from pathlib import Path +ROOT=Path(__file__).resolve().parent + +def require(ok,message): + if not ok:raise RuntimeError(message) + +def conflict(database,negated): + assigned={} + for literal in negated: + variable=abs(literal);value=literal>0 + if variable in assigned and assigned[variable]!=value:return True + assigned[variable]=value + while True: + change=False + for row in database: + available=[];satisfied=False + for literal in row: + variable=abs(literal) + if variable not in assigned:available.append(literal) + elif assigned[variable]==(literal>0):satisfied=True;break + if satisfied:continue + if not available:return True + if len(available)==1: + literal=available[0];variable=abs(literal);value=literal>0 + if variable in assigned and assigned[variable]!=value:return True + if variable not in assigned:assigned[variable]=value;change=True + if not change:return False + +def replay(record): + database=[tuple(row) for row in record['clauses']];steps=0;finished=False + for line in record['proof']: + pieces=line.split() + if pieces[0]=='d':continue + row=tuple(map(int,pieces));require(row[-1]==0 and 0 not in row[:-1],'bad proof syntax') + row=row[:-1];require(all(abs(x)<=record['variables'] for x in row),'bad proof variable') + require(conflict(database,[-x for x in row]),'independent non-RUP addition') + database.append(row);steps+=1 + if not row:finished=True + require(finished,'independent proof has no empty clause') + return steps + +def regular_controls(): + permutations=list(itertools.permutations(range(3)));index={g:i for i,g in enumerate(permutations)} + def product(a,b):return tuple(a[b[i]] for i in range(3)) + ident=(0,1,2);a=(0,2,1);b=(2,1,0);swap=product(product(b,a),b) + # Faithfulness: a group-algebra coefficient is visible on the identity basis vector. + require(len({index[product(g,ident)] for g in permutations})==6,'regular representation is not faithful') + columns=0 + for active in (1,2,3): + word=[(role,label) for role in range(active) for label in (b,a,b)] + for original in range(24): + data=[0]*4;data[original//6]=1<<(original%6) + initial=data[:] + for role,label in word: + moved=0 + for h in range(6): + if data[role]>>h&1:moved^=1<>h&1:moved^=1<>3)&1)^((g>>1)&1)*((g>>2)&1))==1] + natural=0 + for g in coordinates:natural^=g + require(natural==0 and sum(1<self.variables for x in clause):raise ValueError('invalid literal') + clause=list(dict.fromkeys(clause)) + if not clause:self.empty=True;return + if len(clause)==1:self.units.append(clause[0]);return + index=len(self.clauses);self.clauses.append(clause) + self.watches[clause[0]].append(index);self.watches[clause[1]].append(index) + def conflict(self,assumptions): + if self.empty:return True + values=[0]*(self.variables+1);queue=[] + def assign(literal): + index=abs(literal);value=1 if literal>0 else -1 + if values[index]==-value:return False + if values[index]==0:values[index]=value;queue.append(literal) + return True + def evaluate(literal):return values[abs(literal)]*(1 if literal>0 else -1) + for literal in [*self.units,*assumptions]: + if not assign(literal):return True + processed=0 + while processed0:position+=1;continue + replacement=next((i for i in range(2,len(clause)) if evaluate(clause[i])>=0),None) + if replacement is not None: + clause[1],clause[replacement]=clause[replacement],clause[1] + watching[position]=watching[-1];watching.pop();self.watches[clause[1]].append(index) + continue + if evaluate(other)<0 or not assign(other):return True + position+=1 + return False + +def check_proof(variables,clauses,proof): + database=Database(variables,clauses);additions=deletions=0;closed=False + for line in proof: + tokens=line.split() + if not tokens:raise ValueError('empty proof record') + deletion=tokens[0]=='d' + if deletion:tokens=tokens[1:] + literals=[int(x) for x in tokens] + if not literals or literals[-1]!=0 or 0 in literals[:-1]:raise ValueError('invalid proof terminator') + clause=literals[:-1] + if any(abs(x)>variables for x in clause):raise ValueError('proof variable outside CNF') + if deletion:deletions+=1;continue + if not database.conflict([-x for x in clause]):raise ValueError('non-RUP proof addition') + database.add(clause);additions+=1 + if not clause:closed=True + if not closed:raise ValueError('proof never derives empty clause') + return {'rup_additions':additions,'ignored_deletions':deletions} + +def slow_conflict(clauses,assumptions): + values={} + for literal in assumptions: + if -literal in values:return True + values[literal]=True + changed=True + while changed: + changed=False + for clause in clauses: + if any(x in values for x in clause):continue + available=[x for x in clause if -x not in values] + if not available:return True + if len(available)==1: + x=available[0] + if x not in values:values[x]=True;changed=True + return False diff --git a/research/three-swap-compression-seed6/search.py b/research/three-swap-compression-seed6/search.py new file mode 100644 index 0000000000..8c9281ffbb --- /dev/null +++ b/research/three-swap-compression-seed6/search.py @@ -0,0 +1,117 @@ +#!/usr/bin/env python3 +"""Bounded, exact Boolean encoding of normalized seven-call three-SWAP words. +Cinna Davis with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +import itertools +import json +from pathlib import Path +import time +import z3 + +ROOT=Path(__file__).resolve().parent + +def mm(a,b): + return sum(((sum(((a>>(2*i+k))&1)*((b>>(2*k+j))&1) for k in range(2))&1)<<(2*i+j)) for i in range(2) for j in range(2)) +GROUP=tuple(n for n in range(16) if (((n&1)*((n>>3)&1)^((n>>1)&1)*((n>>2)&1)))==1) +INDEX={g:i for i,g in enumerate(GROUP)} +IDENT,A,B,SWAP=9,11,13,6 + +def xor(values): + result=z3.BoolVal(False) + for x in values:result=z3.Xor(result,x) + return result + +def target(r=4,active=3): + return [[(1<>k)&1:operand^=state[i][k] + translated=0 + for h in range(6): + if (operand>>h)&1:translated^=1<>j)&1:new[i][j]^=delta + state=new + return state + +def encode(labels,timeout_ms=15000,pinned=None): + r=4;solver=z3.Solver();solver.set(timeout=timeout_ms,random_seed=6) + state=[[[z3.BoolVal(h==INDEX[IDENT] and i==j) for j in range(r)] for i in range(r)] for h in range(6)] + projectors=[];a_count=0 + for step,label in enumerate(labels): + if label=='a': + u=[z3.BoolVal(i==a_count) for i in range(r)];a_count+=1 + else:u=[z3.Bool(f'u_{step}_{i}') for i in range(r)] + v=[z3.Bool(f'v_{step}_{i}') for i in range(r)] + solver.add(xor(z3.And(u[i],v[i]) for i in range(r))) + if pinned is not None: + solver.add(*[v[i]==z3.BoolVal(bool((pinned[step]['v']>>i)&1)) for i in range(r)]) + solver.add(*[u[i]==z3.BoolVal(bool((pinned[step]['u']>>i)&1)) for i in range(r)]) + projectors.append((u,v)) + g=A if label=='a' else B + contracted=[[xor(z3.And(state[h][i][k],u[k]) for k in range(r)) for i in range(r)] for h in range(6)] + new=[[[z3.Bool(f's_{step}_{h}_{i}_{j}') for j in range(r)] for i in range(r)] for h in range(6)] + for h in range(6): + predecessor=INDEX[mm(GROUP[h],g)] + for i in range(r): + value=z3.Xor(contracted[h][i],contracted[predecessor][i]) + for j in range(r):solver.add(new[h][i][j]==z3.Xor(state[h][i][j],z3.And(value,v[j]))) + state=new + expected=target(r) + for h in range(6): + for i in range(r): + for j in range(r):solver.add(state[h][i][j]==z3.BoolVal(bool((expected[i][j]>>h)&1))) + # Redundant sign-quotient consequences improve propagation. + for i in range(r): + for j in range(r):solver.add(xor(z3.And(u[i],v[j]) for u,v in projectors)==z3.BoolVal(i==j and i<3)) + return solver,projectors + +def solve(labels,timeout_ms): + started=time.monotonic();solver,projectors=encode(labels,timeout_ms) + answer=solver.check();out={'labels':labels,'status':str(answer),'elapsed_seconds':round(time.monotonic()-started,6)} + if answer==z3.sat: + model=solver.model();word=[] + for label,(u,v) in zip(labels,projectors): + word.append({'u':sum(int(z3.is_true(model.eval(x,model_completion=True)))<>i&1];database=Database(2,clauses) + for choices in itertools.product((-1,0,1),repeat=2): + assumptions=[(i+1)*sign for i,sign in enumerate(choices) if sign] + require(database.conflict(assumptions)==slow_conflict(clauses,assumptions),'watched/slow propagation mismatch') + comparisons+=1 + return failures,comparisons + +def group_controls(): + # Independently construct the coordinate action on nonzero binary vectors. + def action(g): + values=[] + for v in (1,2,3): + x=((g&1)*(v&1)^((g>>1)&1)*((v>>1)&1)) + y=(((g>>2)&1)*(v&1)^((g>>3)&1)*((v>>1)&1)) + values.append((1,2,3).index(x+2*y)) + return tuple(values) + groups=[g for g in range(16) if ((g&1)*((g>>3)&1)^((g>>1)&1)*((g>>2)&1))==1] + require(set(map(action,groups))==set(cnf.GROUP),'GL2/S3 isomorphism mismatch') + for left,right in itertools.product(groups,repeat=2): + product=sum((sum(((left>>(2*i+k))&1)*((right>>(2*k+j))&1) for k in range(2))%2)<<(2*i+j) for i in range(2) for j in range(2)) + require(cnf.INDEX[action(product)]==cnf.MUL[cnf.INDEX[action(left)]][cnf.INDEX[action(right)]],'GL2/S3 multiplication mismatch') + require(action(11)==cnf.GROUP[cnf.A] and action(13)==cnf.GROUP[cnf.B] and action(6)==cnf.GROUP[cnf.SWAP],'group label mismatch') + for a,b,c in itertools.product(range(6),repeat=3):require(cnf.MUL[cnf.MUL[a][b]][c]==cnf.MUL[a][cnf.MUL[b][c]],'group associativity') + require(cnf.MUL[cnf.MUL[cnf.A][cnf.B]][cnf.A]==cnf.SWAP,'ABA witness failed') + +def main(): + started=time.monotonic();group_controls();failures,comparisons=gadget_controls() + payload=gzip.decompress((ROOT/'CERTIFICATES.json.gz').read_bytes());d=json.loads(payload) + require(d['format']=='CNF-and-DRUP-v1' and len(d['results'])==35,'missing pattern certificates') + require([x['index'] for x in d['results']]==list(range(35)),'duplicate or missing pattern') + additions=deletions=clauses=0 + for record,labels in zip(d['results'],cnf.patterns()): + require(record['labels']==labels,'label domain mismatch');formula=cnf.encode(labels) + require(record['variables']==formula.variables and record['clauses']==formula.clauses,'CNF differs from fresh exact encoding') + checked=check_proof(formula.variables,formula.clauses,record['proof']) + additions+=checked['rup_additions'];deletions+=checked['ignored_deletions'];clauses+=len(formula.clauses) + # Full arbitrary-dirty nine-call upper bound, represented by all 24 regular columns. + word=[{'u':1<0 else not assignment[abs(literal)] + for gate,(u,v) in zip(word,positive.projectors): + for name,literals in [('u',u),('v',v)]: + for i,literal in enumerate(literals): + bit=bool(gate[name]>>i&1) + if abs(literal)==1:require(value(literal)==bit,'pinned positive constant mismatch') + else:assignment[abs(literal)]=bit if literal>0 else not bit + for variable,operation,a,b in positive.operations: + assignment[variable]=(value(a) and value(b)) if operation=='and' else (value(a)!=value(b)) + require(all(any(value(x) for x in row) for row in positive.clauses),'positive construction fails the actual CNF clauses') + corrupt=[x.copy() for x in word];corrupt[0]['label']='a';require(cnf.concrete(corrupt)!=target,'wrong paid-label control is vacuous') + print(json.dumps({'status':'PASS_THREE_SWAP_COMPRESSION','patterns':35,'registers':4,'active_swaps':3,'excluded_calls':7,'attaining_calls':9,'cnf_clauses':clauses,'rup_additions':additions,'ignored_deletions':deletions,'rup_negative_controls':failures,'watched_vs_slow_cases':comparisons,'payload_sha256':hashlib.sha256(payload).hexdigest(),'elapsed_seconds':round(time.monotonic()-started,6)},sort_keys=True)) +if __name__=='__main__':main()