diff --git a/research/spectator-three-cycle-additivity/README.md b/research/spectator-three-cycle-additivity/README.md new file mode 100644 index 0000000000..7365c5defa --- /dev/null +++ b/research/spectator-three-cycle-additivity/README.md @@ -0,0 +1,131 @@ +# A spectator coordinate does not help two 3-cycles + +**Exact computer-assisted result in a formal model. No new κ.** +The selected conditional exponent stays 15108879/5000000000 (#4610). + +## Result + +The setting is the formal model `M_R(F2[GL_n(F2)])` of #4939/#4950/#4968 +at `n = 4`, `R = 2`: + +- A paid call is `D(g,N) = I + ([g]+[e])N`, where `g` is one of the 12 + coordinate CNOTs of `GL_4(F2)` and `N = uvᵀ` is one of the 6 rank-one binary + idempotents of `M_2(F2)`. This gives 72 paid factors. +- Free scalar `GL_2(F2)` maps are allowed. +- Equality is formal, on arbitrary inputs. + +Let `c` be the coordinate 3-cycle on coordinates 0, 1, 2. Address coordinate 3 +is a spectator: the endpoint fixes it, but calls may write it. Then + +```text +diag([c],[c]) has no realizing word of length ≤ 11, so its cost is exactly 12. +``` + +The upper bound is #5005's word: a shortest 3-cycle word on each register. +So a spectator coordinate gives two 3-cycles no shared paid work, just as at +`n = 3` (#5005). This answers the `n ≥ 4` part of #5005's open question for its +smallest case. A single 3-cycle already costs 6 with any spectators +(`research/three-cycle-address-floor`). + +| Check | Outcome | +|---|---| +| Upper bound | 12 calls | +| Length ≤ 9 | excluded in the registered replay (depth 4 + 5) | +| Length ≤ 10 | excluded in a recorded **local** run (depth 4 + 6) | +| Length ≤ 11 | excluded in a recorded **local** run (depth 5 + 6, 721,626,127 forward states) | + +## Method + +`search.c` is an exact meet-in-the-middle search with a **sparse** state. +Each of the four matrix entries is a sorted set of `GL_4(F2)` indices with F2 +coefficients. A product of `L` calls has at most `2^L` terms per entry, so the +20,160-element group needs no dense bitsets. The search structure is the same +as in #5005 and #5292: + +- **Cancellation.** Adjacent equal letters cancel. +- **Commutation order.** 1,584 of the 5,112 ordered pairs of distinct calls + commute (an exact algebra test). Adjacent commuting letters are kept only in + increasing order. +- **Symmetry.** The target and the generator set are fixed by 36 maps: + conjugation of `GL_4` by the coordinate permutations commuting with `c`, + optionally composed with inverse-transpose, times `GL_2(F2)` register + conjugation. The first two backward letters are the lexicographically least + pair of their orbit, which leaves 142 of 5,112 pairs. The commutation order + applies only from the fourth backward letter on. +- **Exact check of key matches.** A state at distance ≤ 5 is `A·B`, with `A` + in the exact radius-two ball (4,297 stored states) and `|B| ≤ 3`. Every key + match is tested this way. The final run recorded one key match, and the exact + test rejected it. An earlier length-11 run used a build whose exact test only + reached distance 4. It was discarded and rerun with the final source. + +The distinct-state counts are 73, 4,297, 240,565, 13,231,207 and 721,626,127 +at depth ≤ 1, …, 5. + +## Evidence + +`verify.py` uses the standard library and a C11 compiler. In default mode it +checks: + +1. **Compilation.** `search.c` compiles with `-Wall -Wextra -Werror`. +2. **Semantics.** The C products agree with the merged Python formal model at + `n = 4`, `R = 2` on 36 random words of length 0–5, as exact group-algebra + states. +3. **Engine self-test.** There are 1,584 commuting pairs and the exact + radius-two ball. Twelve random words of length 3–5 verify within their + length, and `diag(c,c)` is rejected at distance ≤ 5. +4. **State counts.** The distinct states at depth ≤ 1, 2, 3, 4 are as listed + above. +5. **Positive controls,** with and without symmetry: + - `diag([c],[e])` (cost 6, as in `three-cycle-address-floor`); + - two swaps `diag([s01],[s01])` (cost 6, as in #4950). + Each has nothing at length ≤ 5, and its length 6 is found. +6. **Mixed target.** `diag([c],[s01])` has nothing at length ≤ 8. A recorded + local depth 4 + 5 run finds its length 9. +7. **Upper bound.** The 12-call word is checked in Python. +8. **Main search.** Nothing at length ≤ 6 without symmetry, and nothing at + length ≤ 9 with it. + +`verify.py --full` reruns the local depth 4 + 6 and 5 + 6 runs. The second needs +about 8 GB of memory. `RESULT.json` records their outputs, times, machine and +the hash of the compiled source. + +Changing `search.c` fails the hash binding to the recorded runs. Dropping one +column update in the generator product fails the semantic binding. + +## Scope + +Card `bit-new-register-model`, scope **changed** (see `TASK.json`). This covers +only `n = 4` (one spectator) with `R = 2`. It does **not** settle: +- `n ≥ 5`; +- a dirty third register (#5292 leaves length 11 open at `R = 3`); +- other targets; +- native operations, tariffs or κ. + +Base: canonical main `1ec1119972c9aefe42525172d07b332fcff81cb4`, priority +revision 7. + +## Reproduce + +```sh +python3.12 -I -B research/spectator-three-cycle-additivity/verify.py +python3.12 -I -B research/spectator-three-cycle-additivity/verify.py --full # local, about 8 GB +python3.12 -B scripts/research_package.py --package research/spectator-three-cycle-additivity +``` + +## Open next questions + +1. **Every `n ≥ 4`.** *First step:* adapt the written-spectator reduction of + `three-cycle-address-floor`. A short word can write only a few spectator + rows. Restrict the unwritten ones to their zero subspace, which reduces the + question to finitely many `n`, including this one. *Blocked by:* a written + argument for two targets. + +## Credit + +- Mihir Srivastava (#4939), for the formal model. +- JoyboyBrian (#4974, `three-cycle-address-floor`), for the single-cycle + spectator theorem. +- The predecessors credited in #4950/#4968/#5005/#5292. + +Prepared by James Reed with substantial Anthropic Claude (Claude Code) +assistance. Apache-2.0. No independent human review is claimed. diff --git a/research/spectator-three-cycle-additivity/RESULT.json b/research/spectator-three-cycle-additivity/RESULT.json new file mode 100644 index 0000000000..3a7958a6de --- /dev/null +++ b/research/spectator-three-cycle-additivity/RESULT.json @@ -0,0 +1,63 @@ +{ + "schema_version": 1, + "target": "diag([c],[c]) in M_2(F2[GL_4(F2)]), c the 3-cycle on coordinates 0,1,2, coordinate 3 a spectator", + "upper_bound": 12, + "excluded_lengths_registered": "<= 9", + "excluded_lengths_local": "<= 11", + "exact_cost": 12, + "new_kappa": false, + "note": "Every key match is checked exactly (distance <= 5 via the stored radius-two ball and words of length <= 3); the single key match of the length-11 run is a fingerprint collision. An earlier length-11 run used a build whose exact check only covered distance <= 4; it was discarded and rerun with this source.", + "local_runs": [ + { + "search_c_sha256": "6111e6a9f12f5aba5fd0841332fc660305306eaa9670a5f25d0313c77e08b890", + "compile": "cc -std=c11 -O3 -march=native -Wall -Wextra -Werror -o search search.c", + "compiler": "cc (GCC) 16.2.1 20260810", + "machine": "AMD Ryzen 9 7940HS w/ Radeon 780M Graphics, 16 threads, 25 GB RAM, Linux 7.2.8-9-omarchy", + "label": "local-only receipt; not replayed by the registered harness", + "name": "c3c3 length <= 11", + "command": "search c3c3 5 6 sym 16 30", + "max_length": 11, + "started_utc": "2026-10-23T20:23:00Z", + "finished_utc": "2026-10-23T20:32:54Z", + "output": [ + "target=c3c3 symmetries=36 pairs=142 mode=sym", + "forward_depth=5 distinct=721626127 ball2=4297", + "RESULT target=c3c3 max_length=11 shortest=-1 key_matches=1 backward_nodes=2177858439" + ] + }, + { + "search_c_sha256": "6111e6a9f12f5aba5fd0841332fc660305306eaa9670a5f25d0313c77e08b890", + "compile": "cc -std=c11 -O3 -march=native -Wall -Wextra -Werror -o search search.c", + "compiler": "cc (GCC) 16.2.1 20260810", + "machine": "AMD Ryzen 9 7940HS w/ Radeon 780M Graphics, 16 threads, 25 GB RAM, Linux 7.2.8-9-omarchy", + "label": "local-only receipt; not replayed by the registered harness", + "name": "c3c3 length <= 10", + "command": "search c3c3 4 6 sym 16 27", + "max_length": 10, + "started_utc": "2026-10-23T20:33:04Z", + "finished_utc": "2026-10-23T20:34:05Z", + "output": [ + "target=c3c3 symmetries=36 pairs=142 mode=sym", + "forward_depth=4 distinct=13231207 ball2=4297", + "RESULT target=c3c3 max_length=10 shortest=-1 key_matches=0 backward_nodes=2177858439" + ] + }, + { + "search_c_sha256": "6111e6a9f12f5aba5fd0841332fc660305306eaa9670a5f25d0313c77e08b890", + "compile": "cc -std=c11 -O3 -march=native -Wall -Wextra -Werror -o search search.c", + "compiler": "cc (GCC) 16.2.1 20260810", + "machine": "AMD Ryzen 9 7940HS w/ Radeon 780M Graphics, 16 threads, 25 GB RAM, Linux 7.2.8-9-omarchy", + "label": "local-only receipt; not replayed by the registered harness", + "name": "c3s01 shortest 9", + "command": "search c3s01 4 5 sym 16 27", + "max_length": 9, + "started_utc": "2026-10-23T20:34:05Z", + "finished_utc": "2026-10-23T20:34:28Z", + "output": [ + "target=c3s01 symmetries=2 pairs=2556 mode=sym", + "forward_depth=4 distinct=13231207 ball2=4297", + "RESULT target=c3s01 max_length=9 shortest=9 key_matches=2241 backward_nodes=658795849" + ] + } + ] +} diff --git a/research/spectator-three-cycle-additivity/SOURCES.json b/research/spectator-three-cycle-additivity/SOURCES.json new file mode 100644 index 0000000000..ec325a697c --- /dev/null +++ b/research/spectator-three-cycle-additivity/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "1ec1119972c9aefe42525172d07b332fcff81cb4", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b288ae44032fd84dd5564243422836cbcd29835e", + "sha256": "f9ed52bb642cd1e1486cf2743557ac5fa23cf1514a3277d786a644e39a565038" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/swap-component-cut/formal.py", + "usage": "input", + "git_blob": "eb3058c3593e3373a417f9b6c2d566ca409b591d", + "sha256": "e23c71e52a52ee6466a8d07c3608ebe38015cdc959c92f9e8a57557c9ef68628" + }, + { + "path": "research/two-three-cycle-additivity/README.md", + "usage": "provenance", + "git_blob": "6bbd51f92adebdf1e5ca8141251cc35f5990af7c", + "sha256": "b292e40966b928f26b407ae5c59b4ed9b8d4687d28076efbc759a8afdf62cdfb" + }, + { + "path": "research/three-register-three-cycles/README.md", + "usage": "provenance", + "git_blob": "555f72cae779edc92e9f89f5c87047aec6429e95", + "sha256": "ff1433a69b5be638dd93cdf299ef2f94b0260bdfae86aae9f2616e6f537285ae" + }, + { + "path": "research/three-cycle-address-floor/README.md", + "usage": "provenance", + "git_blob": "6a65c91f29e5b226cebd32d0c1d6963a60a98761", + "sha256": "a63c4ea4c874cac1fb064e1aff07f8ef791391eb795aec22a2154eb44a8fa81e" + }, + { + "path": "research/swap-component-cut/README.md", + "usage": "provenance", + "git_blob": "19eaadc4ea40e312d202c917e2f1914d98ca224a", + "sha256": "7fe7efcb948a71af664d8f7828c8f4a056de3c6c3aa2cb82e420ec6ae7bd0106" + } + ] +} diff --git a/research/spectator-three-cycle-additivity/TASK.json b/research/spectator-three-cycle-additivity/TASK.json new file mode 100644 index 0000000000..e921aa088c --- /dev/null +++ b/research/spectator-three-cycle-additivity/TASK.json @@ -0,0 +1,64 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "1ec1119972c9aefe42525172d07b332fcff81cb4", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "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. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "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": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "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.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Decide by exact search the cost of diag([c],[c]) in M_2(F2[GL_4(F2)]): two coordinate 3-cycles on coordinates 0,1,2 with one spectator address coordinate that must be restored (the n >= 4 open question of research/two-three-cycle-additivity).", + "scope_change_reason": "PR #5005 settled n = 3, R = 2 (exactly twelve) and PR #5292 bounded R = 3 below by eleven. Spectators are known not to help a single 3-cycle (#4974) or swaps (#4950). This package settles the smallest spectator case for two 3-cycles exactly. It does not cover n >= 5, R >= 3 or other targets.", + "bottleneck_link": "A spectator address coordinate cannot make two 3-cycles share paid work in this formal model at n = 4, R = 2; any saving needs a changed operation or tariff.", + "budget_minutes": 60, + "stop_rule": "Stop at the exact length-11 exclusion with positive controls. Do not extend to n = 5 or R = 3 in this package.", + "outcome": "completed", + "evidence": "python3.12 -B scripts/research_package.py --package research/spectator-three-cycle-additivity", + "author": "James Reed", + "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code, Opus 5.5).", + "open_questions": [ + { + "question": "Does the n = 4 answer extend to every n >= 4 (all spectators), and does it combine with a dirty third register?", + "why_it_matters": "Together with #4974's uniform single-cycle argument, an all-n statement would close the spectator direction for two 3-cycles; the R = 3 length-11 case (#5292) is still open.", + "first_step": "Adapt #4974's written-spectator reduction: a word of length <= 11 can write at most a bounded number of spectator rows; restrict unwritten spectators to the zero subspace and reduce to this n = 4 search.", + "blocked_by": "A written argument for the reduction; the n = 5 search alone is much larger." + } + ] +} diff --git a/research/spectator-three-cycle-additivity/VERIFY.json b/research/spectator-three-cycle-additivity/VERIFY.json new file mode 100644 index 0000000000..9877b11500 --- /dev/null +++ b/research/spectator-three-cycle-additivity/VERIFY.json @@ -0,0 +1,21 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/swap-component-cut/formal.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Compile search.c (-Wall -Wextra -Werror); bind the sparse C engine to the Python formal model at n = 4, R = 2 on 36 random words; 1,584 commuting pairs and the exact 4,297-state radius-two ball; distinct-state counts 73/4297/240565/13231207; twelve-call attaining word in Python; positive controls c3e and s01s01 with and without symmetry (nothing at length <= 5, shortest 6); c3c3 nothing at length <= 6 without symmetry; c3s01 nothing at length <= 8; c3c3 nothing at length <= 9 with symmetry (36 symmetries, 142 pairs). Lengths <= 10 and <= 11 are recorded local receipts in RESULT.json (verify.py --full)." + } + ] +} diff --git a/research/spectator-three-cycle-additivity/search.c b/research/spectator-three-cycle-additivity/search.c new file mode 100644 index 0000000000..85804d1b09 --- /dev/null +++ b/research/spectator-three-cycle-additivity/search.c @@ -0,0 +1,412 @@ +/* Exact meet-in-the-middle search in M_2(F2[GL_4(F2)]): two coordinate + * 3-cycles on coordinates 0,1,2 with spectator coordinate 3. + * + * Paid call D(g,N) = I + ([g]+[e]) N, g one of the 12 coordinate CNOTs of + * GL_4(F2), N one of the 6 rank-one idempotents u v^T of M_2(F2): 72 + * generators, numbered 6*cnot + projector. States are kept sparsely: each of + * the four entries is a sorted set of group-element indices (F2 coefficients). + * A product of at most L calls has at most 2^L terms per entry. + * + * Reductions (sound for a shortest word): no adjacent equal letters; adjacent + * commuting letters only in increasing order; in sym mode the first two + * backward letters are the lexicographically least pair of their orbit under + * the symmetries fixing the target and generator set (commutation order then + * applies from the fourth backward letter on, never across the chosen pair). + * + * Usage: + * search count [bits] + * search dump + * search selftest + * search [sym|nosym] [workers] [bits] + * targets: c3c3 c3e s01s01 c3s01 + * A key match is checked exactly: distance <= 5 iff X * B lies in the stored + * exact radius-two ball for some word B of length <= 3. + */ +#define _POSIX_C_SOURCE 200809L +#include +#include +#include +#include +#include +#include +#include + +#define NG 20160 +#define R 2 +#define NP 6 +#define NC 12 +#define NGEN (NC * NP) +#define CAP 256 +typedef struct { uint16_t n; uint16_t e[CAP]; } Set; +typedef struct { Set s[R][R]; } State; + +static uint16_t idx_of[65536]; +static uint16_t elem[NG]; +static uint16_t rmul[NC][NG]; +static int gen_u[NP], gen_v[NP]; +static uint16_t cn[NC]; + +static void need(int ok, const char *m) { if (!ok) { fprintf(stderr, "FAIL: %s\n", m); exit(9); } } +static int mat_mul(int a, int b) { /* rows: 4 bits each, row i at bits 4i */ + int r = 0; + for (int i = 0; i < 4; i++) { + int row = 0, ai = (a >> (4 * i)) & 15; + for (int k = 0; k < 4; k++) if (ai >> k & 1) row ^= (b >> (4 * k)) & 15; + r |= row << (4 * i); + } + return r; +} +static int invertible(int m) { + int rows[4], r = 0; + for (int i = 0; i < 4; i++) rows[i] = (m >> (4 * i)) & 15; + for (int bit = 0; bit < 4; bit++) { + int p = -1; + for (int i = r; i < 4; i++) if (rows[i] >> bit & 1) { p = i; break; } + if (p < 0) continue; + int t = rows[r]; rows[r] = rows[p]; rows[p] = t; + for (int i = 0; i < 4; i++) if (i != r && (rows[i] >> bit & 1)) rows[i] ^= rows[r]; + r++; + } + return r == 4; +} +static int identity4(void) { return 1 | (2 << 4) | (4 << 8) | (8 << 12); } +static int rowperm(const int *s) { int m = 0; for (int a = 0; a < 4; a++) m |= (1 << s[a]) << (4 * a); return m; } +static int transpose4(int a) { int r = 0; for (int i = 0; i < 4; i++) for (int j = 0; j < 4; j++) if ((a >> (4*i+j)) & 1) r |= 1 << (4*j+i); return r; } +static int inverse4(int a) { /* Gauss-Jordan on [A | I] */ + int rows[4], inv[4]; + for (int i = 0; i < 4; i++) { rows[i] = (a >> (4 * i)) & 15; inv[i] = 1 << i; } + for (int c = 0; c < 4; c++) { + int p = -1; + for (int i = c; i < 4; i++) if (rows[i] >> c & 1) { p = i; break; } + if (p < 0) abort(); + int t = rows[c]; rows[c] = rows[p]; rows[p] = t; t = inv[c]; inv[c] = inv[p]; inv[p] = t; + for (int i = 0; i < 4; i++) if (i != c && (rows[i] >> c & 1)) { rows[i] ^= rows[c]; inv[i] ^= inv[c]; } + } + int r = 0; for (int i = 0; i < 4; i++) r |= inv[i] << (4 * i); + if (mat_mul(a, r) != identity4()) abort(); + return r; +} + +/* sparse F2 set operations */ +static void sym_into(Set *out, const Set *a, const Set *b) { /* out = a xor b (sorted) */ + int i = 0, j = 0, n = 0; + while (i < a->n && j < b->n) { + if (a->e[i] < b->e[j]) out->e[n++] = a->e[i++]; + else if (a->e[i] > b->e[j]) out->e[n++] = b->e[j++]; + else { i++; j++; } + } + while (i < a->n) out->e[n++] = a->e[i++]; + while (j < b->n) out->e[n++] = b->e[j++]; + need(n <= CAP, "set capacity"); + out->n = (uint16_t)n; +} +static int cmp16(const void *a, const void *b) { return (int)*(const uint16_t *)a - (int)*(const uint16_t *)b; } +static void translate(Set *out, const Set *a, int gi) { /* out = a * [g] */ + out->n = a->n; + for (int i = 0; i < a->n; i++) out->e[i] = rmul[gi][a->e[i]]; + /* insertion sort (small) */ + for (int i = 1; i < out->n; i++) { uint16_t v = out->e[i]; int j = i - 1; while (j >= 0 && out->e[j] > v) { out->e[j+1] = out->e[j]; j--; } out->e[j+1] = v; } +} +static State apply(const State *x, int gen) { /* x * D(g, u v^T) */ + int gi = gen / NP, ni = gen % NP, u = gen_u[ni], v = gen_v[ni]; + State r = *x; + for (int i = 0; i < R; i++) { + Set z, t, w, tmp; + z.n = 0; + for (int k = 0; k < R; k++) if (u >> k & 1) { sym_into(&tmp, &z, &x->s[i][k]); z = tmp; } + translate(&t, &z, gi); + sym_into(&w, &t, &z); + for (int j = 0; j < R; j++) if (v >> j & 1) { sym_into(&tmp, &r.s[i][j], &w); r.s[i][j] = tmp; } + } + return r; +} +static int steq(const State *a, const State *b) { + for (int i = 0; i < R; i++) for (int j = 0; j < R; j++) { + if (a->s[i][j].n != b->s[i][j].n) return 0; + if (memcmp(a->s[i][j].e, b->s[i][j].e, 2 * a->s[i][j].n)) return 0; + } + return 1; +} +static uint64_t mix(uint64_t z) { z ^= z >> 33; z *= 0xFF51AFD7ED558CCDULL; z ^= z >> 33; z *= 0xC4CEB9FE1A85EC53ULL; z ^= z >> 33; return z; } +static uint64_t fp(const State *x) { + uint64_t h = 0x9E3779B97F4A7C15ULL; + for (int i = 0; i < R; i++) for (int j = 0; j < R; j++) { + const Set *s = &x->s[i][j]; + h = mix(h ^ (0x1000ULL * (uint64_t)(2*i+j+1) + s->n)); + for (int k = 0; k < s->n; k++) h = mix(h + s->e[k] + 0x9E37ULL); + } + return h | 8; +} + +static uint64_t *table, tmask; static long distinct; +static void alloc_table(int bits) { + size_t n = (size_t)1 << bits; + table = mmap(NULL, n * 8, PROT_READ | PROT_WRITE, MAP_PRIVATE | MAP_ANONYMOUS, -1, 0); + need(table != MAP_FAILED, "table allocation"); tmask = n - 1; +} +static void insert(uint64_t h, int d) { + uint64_t key = h & ~7ULL, i = (h >> 7) & tmask; + for (;;) { uint64_t t = table[i]; + if (!t) { table[i] = key | (uint64_t)d; distinct++; return; } + if ((t & ~7ULL) == key) { if ((int)(t & 7) > d) table[i] = key | (uint64_t)d; return; } + i = (i + 1) & tmask; } +} +static int lookup(uint64_t h) { + uint64_t key = h & ~7ULL, i = (h >> 7) & tmask; + for (;;) { uint64_t t = table[i]; if (!t) return -1; if ((t & ~7ULL) == key) return (int)(t & 7); i = (i + 1) & tmask; } +} + +static unsigned char comm[NGEN][NGEN]; +static int follows(int last, int g) { return last < 0 || (g != last && !(comm[last][g] && last > g)); } +static State identity_state(void) { + State s; memset(&s, 0, sizeof s); + for (int i = 0; i < R; i++) { s.s[i][i].n = 1; s.s[i][i].e[0] = idx_of[identity4()]; } + return s; +} + +/* exact radius-two ball for verification */ +#define B2N 8192 +static State *b2s; static signed char *b2d; static long b2n; +static uint64_t b2h[B2N * 2]; /* open addressing: index into b2s, +1 */ +static int b2_find(const State *x) { + uint64_t i = (fp(x) >> 7) & (B2N * 2 - 1); + while (b2h[i]) { if (steq(&b2s[b2h[i]-1], x)) return (int)b2h[i]-1; i = (i + 1) & (B2N * 2 - 1); } + return -1; +} +static void b2_add(const State *x, int d) { + if (b2_find(x) >= 0) return; + need(b2n < B2N, "ball2 capacity"); + uint64_t i = (fp(x) >> 7) & (B2N * 2 - 1); + while (b2h[i]) i = (i + 1) & (B2N * 2 - 1); + b2s[b2n] = *x; b2d[b2n] = (signed char)d; b2h[i] = (uint64_t)(++b2n); +} +static void build_b2(void) { + b2s = malloc(sizeof(State) * B2N); b2d = malloc(B2N); need(b2s && b2d, "ball2 memory"); + State I = identity_state(); b2_add(&I, 0); + State one[NGEN]; + for (int a = 0; a < NGEN; a++) { one[a] = apply(&I, a); b2_add(&one[a], 1); } + for (int a = 0; a < NGEN; a++) for (int b = 0; b < NGEN; b++) { State y = apply(&one[a], b); b2_add(&y, 2); } +} +static int verify_exact(const State *x, int maxd) { /* exact distance when <= maxd <= 5 */ + need(maxd <= 5, "exact verification covers distance <= 5"); + int best = 99, k = b2_find(x); + if (k >= 0) best = b2d[k]; + for (int a = 0; a < NGEN; a++) { + State y = apply(x, a); k = b2_find(&y); + if (k >= 0 && b2d[k] + 1 < best) best = b2d[k] + 1; + for (int b = 0; b < NGEN; b++) { + State z = apply(&y, b); k = b2_find(&z); + if (k >= 0 && b2d[k] + 2 < best) best = b2d[k] + 2; + if (maxd >= 5 && best > 5) for (int c = 0; c < NGEN; c++) { + State w = apply(&z, c); k = b2_find(&w); + if (k >= 0 && b2d[k] + 3 < best) best = b2d[k] + 3; + } + } + } + return best <= maxd ? best : -1; +} + +static int fwd_max; +static void fdfs(const State *x, int depth, int last) { + insert(fp(x), depth); + if (depth == fwd_max) return; + for (int g = 0; g < NGEN; g++) if (follows(last, g)) { State y = apply(x, g); fdfs(&y, depth + 1, g); } +} + +/* symmetries: alpha (automorphism of GL_4 preserving the CNOT set) x conjugation by S in GL_2(F2) */ +#define NA 48 +static uint16_t *amap[NA]; static int nalpha; +static int S2[6][2], S2i[6][2]; +static State phi(const State *x, int a, int s) { + State t, u, r; memset(&t, 0, sizeof t); memset(&u, 0, sizeof u); memset(&r, 0, sizeof r); + for (int i = 0; i < R; i++) for (int j = 0; j < R; j++) { + Set *o = &t.s[i][j]; o->n = x->s[i][j].n; + for (int k = 0; k < o->n; k++) o->e[k] = amap[a][x->s[i][j].e[k]]; + qsort(o->e, o->n, 2, cmp16); + } + Set tmp; + for (int i = 0; i < R; i++) for (int j = 0; j < R; j++) for (int k = 0; k < R; k++) + if (S2[s][i] >> k & 1) { sym_into(&tmp, &u.s[i][j], &t.s[k][j]); u.s[i][j] = tmp; } + for (int i = 0; i < R; i++) for (int j = 0; j < R; j++) for (int k = 0; k < R; k++) + if (S2i[s][k] >> j & 1) { sym_into(&tmp, &r.s[i][j], &u.s[i][k]); r.s[i][j] = tmp; } + return r; +} + +static void setup(void) { + int n = 0; + for (int m = 0; m < 65536; m++) { idx_of[m] = 0xFFFF; if (invertible(m)) { idx_of[m] = (uint16_t)n; elem[n++] = (uint16_t)m; } } + need(n == NG, "GL_4(F2) order"); + int c = 0; + for (int i = 0; i < 4; i++) for (int j = 0; j < 4; j++) if (i != j) { int g = identity4() ^ ((1 << j) << (4 * i)); cn[c++] = idx_of[g]; } + for (int gi = 0; gi < NC; gi++) for (int x = 0; x < NG; x++) rmul[gi][x] = idx_of[mat_mul(elem[x], elem[cn[gi]])]; + int p = 0; + for (int u = 1; u < 4; u++) for (int v = 1; v < 4; v++) if (__builtin_popcount((unsigned)(u & v)) & 1) { gen_u[p] = u; gen_v[p] = v; p++; } + need(p == NP, "projectors"); + /* automorphisms: conjugation by the 24 coordinate permutations, optionally composed with inverse-transpose */ + int perm[4] = {0, 1, 2, 3}; nalpha = 0; + for (int a0 = 0; a0 < 4; a0++) for (int a1 = 0; a1 < 4; a1++) for (int a2 = 0; a2 < 4; a2++) for (int a3 = 0; a3 < 4; a3++) { + if ((1<> k & 1) o0 ^= (k ? q1 : q0); if (r1 >> k & 1) o1 ^= (k ? q1 : q0); } + if (o0 == 1 && o1 == 2) { S2i[ns][0] = q0; S2i[ns][1] = q1; } + } + ns++; + } + State I = identity_state(), ga[NGEN]; + for (int a = 0; a < NGEN; a++) ga[a] = apply(&I, a); + for (int a = 0; a < NGEN; a++) for (int b = 0; b < NGEN; b++) { State x = apply(&ga[a], b), y = apply(&ga[b], a); comm[a][b] = (unsigned char)steq(&x, &y); } +} + +typedef struct { long key_matches, nodes; int best; } Report; +static int bword[16]; +static void visit(const State *x, int d, Report *rep) { + rep->nodes++; + int k = lookup(fp(x)); + if (k >= 0) { rep->key_matches++; if (k + d < rep->best) { int e = verify_exact(x, k); if (e >= 0 && e + d < rep->best) rep->best = e + d; } } +} +static void bdfs(const State *x, int d, int maxd, Report *rep) { + visit(x, d, rep); + if (d == maxd) return; + for (int g = 0; g < NGEN; g++) { + if (g == bword[d - 1] || (d >= 3 && !follows(bword[d - 1], g))) continue; + bword[d] = g; State y = apply(x, g); bdfs(&y, d + 1, maxd, rep); + } +} + +int main(int argc, char **argv) { + setup(); + if (argc < 2) return 2; + if (!strcmp(argv[1], "count")) { + int dmax = atoi(argv[2]), bits = argc > 3 ? atoi(argv[3]) : 24; + alloc_table(bits); + for (fwd_max = 1; fwd_max <= dmax; fwd_max++) { + memset(table, 0, (tmask + 1) * 8); distinct = 0; + State s = identity_state(); fdfs(&s, 0, -1); + printf("depth<=%d distinct=%ld\n", fwd_max, distinct); fflush(stdout); + } + return 0; + } + if (!strcmp(argv[1], "dump")) { + State s = identity_state(); + for (int i = 2; i < argc; i++) s = apply(&s, atoi(argv[i])); + for (int i = 0; i < R; i++) for (int j = 0; j < R; j++) { + printf("entry %d %d:", i, j); + for (int k = 0; k < s.s[i][j].n; k++) printf(" %d", elem[s.s[i][j].e[k]]); + printf("\n"); + } + return 0; + } + if (!strcmp(argv[1], "selftest")) { + long pairs = 0; for (int a = 0; a < NGEN; a++) for (int b = 0; b < NGEN; b++) pairs += a != b && comm[a][b]; + build_b2(); + /* exact verification: random words of length 3..5 verify at distance <= length; the target is rejected */ + unsigned seed = 4974; long verified = 0; + for (int trial = 0; trial < 12; trial++) { + int len = 3 + trial % 3; State y = identity_state(); + for (int i = 0; i < len; i++) { seed = seed * 1103515245u + 12345u; y = apply(&y, (int)((seed >> 8) % NGEN)); } + int e = verify_exact(&y, 5); + need(e >= 0 && e <= len, "random word verified within its length"); + verified++; + } + int c3[4] = {1, 2, 0, 3}; State T; memset(&T, 0, sizeof T); + T.s[0][0].n = 1; T.s[0][0].e[0] = idx_of[rowperm(c3)]; T.s[1][1].n = 1; T.s[1][1].e[0] = idx_of[rowperm(c3)]; + need(verify_exact(&T, 5) == -1, "c3c3 is not within distance five"); + printf("selftest commuting_ordered_pairs=%ld ball2=%ld verified_words=%ld\n", pairs, b2n, verified); + return 0; + } + if (argc < 4) return 2; + int c3[4] = {1, 2, 0, 3}, s01[4] = {1, 0, 2, 3}, e4[4] = {0, 1, 2, 3}; + int a, b; + if (!strcmp(argv[1], "c3c3")) { a = rowperm(c3); b = rowperm(c3); } + else if (!strcmp(argv[1], "c3e")) { a = rowperm(c3); b = rowperm(e4); } + else if (!strcmp(argv[1], "s01s01")) { a = rowperm(s01); b = rowperm(s01); } + else if (!strcmp(argv[1], "c3s01")) { a = rowperm(c3); b = rowperm(s01); } + else return 2; + fwd_max = atoi(argv[2]); + int bwd_max = atoi(argv[3]); + need(fwd_max >= 0 && fwd_max <= 5 && bwd_max >= 0 && bwd_max <= 8, "depth range (exact verification covers forward depth <= 5)"); + int use_sym = !(argc > 4 && !strcmp(argv[4], "nosym")); + int workers = argc > 5 ? atoi(argv[5]) : 1, bits = argc > 6 ? atoi(argv[6]) : 24; + State T; memset(&T, 0, sizeof T); + T.s[0][0].n = 1; T.s[0][0].e[0] = idx_of[a]; T.s[1][1].n = 1; T.s[1][1].e[0] = idx_of[b]; + + State I = identity_state(), gstate[NGEN]; + for (int g = 0; g < NGEN; g++) gstate[g] = apply(&I, g); + static int img[NA * 6][NGEN]; int nsym = 0; + if (use_sym) for (int al = 0; al < nalpha; al++) for (int s = 0; s < 6; s++) { + State pt = phi(&T, al, s); + if (!steq(&pt, &T)) continue; + int ok = 1; + for (int g = 0; g < NGEN && ok; g++) { + State pg = phi(&gstate[g], al, s); img[nsym][g] = -1; + for (int h = 0; h < NGEN; h++) if (steq(&pg, &gstate[h])) { img[nsym][g] = h; break; } + if (img[nsym][g] < 0) ok = 0; + } + if (ok) nsym++; + } + static unsigned char pair_ok[NGEN * NGEN]; long npairs = 0; + for (int x = 0; x < NGEN; x++) for (int y = 0; y < NGEN; y++) { + int ok = x != y; + for (int s = 0; s < nsym && ok; s++) { int p2 = img[s][x], q2 = img[s][y]; if (p2 < x || (p2 == x && q2 < y)) ok = 0; } + pair_ok[x * NGEN + y] = (unsigned char)ok; npairs += ok; + } + printf("target=%s symmetries=%d pairs=%ld mode=%s\n", argv[1], use_sym ? nsym : 1, npairs, use_sym ? "sym" : "nosym"); fflush(stdout); + build_b2(); + alloc_table(bits); + State s0 = identity_state(); fdfs(&s0, 0, -1); + printf("forward_depth=%d distinct=%ld ball2=%ld\n", fwd_max, distinct, b2n); fflush(stdout); + Report total = {0, 0, 99}; + { int k = lookup(fp(&T)); total.nodes++; + if (k >= 0) { total.key_matches++; int e = verify_exact(&T, k); if (e >= 0) total.best = e; } + for (int x = 0; x < NGEN; x++) { + int any = 0; for (int y = 0; y < NGEN; y++) any |= pair_ok[x * NGEN + y]; + if (!any) continue; + State y1 = apply(&T, x); total.nodes++; k = lookup(fp(&y1)); + if (k >= 0) { total.key_matches++; int e = verify_exact(&y1, k); if (e >= 0 && e + 1 < total.best) total.best = e + 1; } + } } + if (bwd_max >= 2) { + int pipes[64][2]; + need(workers >= 1 && workers <= 64, "workers"); + for (int w = 0; w < workers; w++) { + need(!pipe(pipes[w]), "pipe"); + pid_t pid = fork(); need(pid >= 0, "fork"); + if (pid == 0) { + close(pipes[w][0]); + Report rep = {0, 0, 99}; long pi = -1; + for (int x = 0; x < NGEN; x++) { + State yx = apply(&T, x); + for (int y = 0; y < NGEN; y++) { + if (!pair_ok[x * NGEN + y]) continue; + if (++pi % workers != w) continue; + bword[0] = x; bword[1] = y; + State yy = apply(&yx, y); + bdfs(&yy, 2, bwd_max, &rep); + } + } + if (write(pipes[w][1], &rep, sizeof rep) != (ssize_t)sizeof rep) _exit(5); + _exit(0); + } + close(pipes[w][1]); + } + for (int w = 0; w < workers; w++) { + Report rep; need(read(pipes[w][0], &rep, sizeof rep) == (ssize_t)sizeof rep, "worker report"); + int st; wait(&st); need(WIFEXITED(st) && !WEXITSTATUS(st), "worker exit"); + total.key_matches += rep.key_matches; total.nodes += rep.nodes; if (rep.best < total.best) total.best = rep.best; + } + } + printf("RESULT target=%s max_length=%d shortest=%d key_matches=%ld backward_nodes=%ld\n", + argv[1], fwd_max + bwd_max, total.best == 99 ? -1 : total.best, total.key_matches, total.nodes); + return 0; +} diff --git a/research/spectator-three-cycle-additivity/verify.py b/research/spectator-three-cycle-additivity/verify.py new file mode 100644 index 0000000000..dc408d52ec --- /dev/null +++ b/research/spectator-three-cycle-additivity/verify.py @@ -0,0 +1,168 @@ +#!/usr/bin/env python3 +"""Two coordinate 3-cycles with a spectator address coordinate cost twelve calls. + +Standard library only. Needs a C compiler (cc) for the exact search. +The sparse C engine for M_2(F2[GL_4(F2)]) is bound to the merged Python +formal model (research/swap-component-cut/formal.py, n = 4, R = 2) by exact +state comparison on random words. It then reproduces distinct-state counts +and known minima before the main search. + +Default mode (the registered replay) proves the length <= 9 exclusion +(depth 4 + 5). `--full` reruns the recorded local receipts: depth 4 + 6 +(length <= 10, about a minute on 16 cores) and depth 5 + 6 (length <= 11, +the exact result; about 8 GB of memory). No new kappa is claimed. +""" + +from __future__ import annotations + +import hashlib +import json +import os +import random +import re +import shutil +import subprocess +import sys +import tempfile +from itertools import product +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = ROOT / "research" / "spectator-three-cycle-additivity" +sys.path.insert(0, str(ROOT / "research" / "swap-component-cut")) + +import formal # noqa: E402 + +COUNTS = {1: 73, 2: 4297, 3: 240565, 4: 13231207} +CONTROLS = (("c3e", 6), ("s01s01", 6)) + + +def need(condition: bool, message: str) -> None: + if not condition: + raise SystemExit("FAIL: " + message) + + +def pins() -> None: + sources = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + for row in sources["files"]: + digest = hashlib.sha256((ROOT / row["path"]).read_bytes()).hexdigest() + need(digest == row["sha256"], "pin " + row["path"]) + selected = json.loads((ROOT / "certificates/selected-result.json").read_text(encoding="utf-8")) + need(selected["kappa"] == "15108879/5000000000", "selected kappa (PR4610 frontier)") + result = json.loads((PACKAGE / "RESULT.json").read_text(encoding="utf-8")) + source = hashlib.sha256((PACKAGE / "search.c").read_bytes()).hexdigest() + need(all(run["search_c_sha256"] == source for run in result["local_runs"]), + "recorded local runs used this search.c") + + +def compile_engine(directory: Path) -> Path: + compiler = shutil.which(os.environ.get("CC", "cc")) or shutil.which("gcc") + need(compiler is not None, "a C11 compiler is required") + binary = directory / "search" + done = subprocess.run([compiler, "-std=c11", "-O3", "-Wall", "-Wextra", "-Werror", "-o", str(binary), + str(PACKAGE / "search.c")], capture_output=True, text=True) + need(done.returncode == 0, "compile failed:\n" + done.stderr) + return binary + + +def run(binary: Path, *args: str, timeout: int = 4 * 3600) -> str: + done = subprocess.run([str(binary), *args], capture_output=True, text=True, timeout=timeout) + need(done.returncode == 0, f"engine {' '.join(args)} exited {done.returncode}: {done.stderr}") + return done.stdout + + +def c_int(group_element) -> int: + return sum(row << (4 * i) for i, row in enumerate(group_element)) + + +def bind_semantics(binary: Path) -> int: + model = formal.Model(4, 2) + need(len(model.generators) == 72, "72 paid factors") + rng = random.Random(4974) + checked = 0 + for length in list(range(0, 6)) * 6: + word = [rng.randrange(72) for _ in range(length)] + state = model.diagonal([]) + for g in word: + state = formal.matrix_product(state, model.generators[g], 2, 4) + expected = {(i, j): sorted(c_int(x) for x in state[i][j]) for i in range(2) for j in range(2)} + got = {} + for line in run(binary, "dump", *map(str, word)).splitlines(): + match = re.fullmatch(r"entry (\d) (\d):(.*)", line) + need(match is not None, "dump format") + got[(int(match[1]), int(match[2]))] = sorted(int(t) for t in match[3].split()) + need(got == expected, f"C and Python products differ on word {word}") + checked += 1 + return checked + + +def upper_bound_word() -> None: + """Twelve calls: a shortest 3-cycle CNOT word on register 0, then on register 1.""" + model = formal.Model(4, 2) + c3 = formal.row_permutation(4, (1, 2, 0, 3)) + cnots = formal.cnots(4) + need(formal.word_lengths(4)[c3] == 6, "3-cycle has CNOT length six in GL_4") + word = None + for w in product(range(12), repeat=6): + g = formal.identity(4) + for k in w: + g = formal.mul(g, cnots[k], 4) + if g == c3: + word = w + break + need(word is not None, "six-letter 3-cycle word") + projectors = [(u, v) for u in range(1, 4) for v in range(1, 4) if bin(u & v).count("1") % 2] + e00, e11 = projectors.index((1, 1)), projectors.index((2, 2)) + calls = [6 * g + e00 for g in word] + [6 * g + e11 for g in word] + state = model.diagonal([]) + for g in calls: + state = formal.matrix_product(state, model.generators[g], 2, 4) + need(state == model.diagonal([c3, c3]) and len(calls) == 12, "twelve-call attaining word") + + +def parse_result(text: str) -> dict: + match = re.search(r"RESULT target=(\S+) max_length=(\d+) shortest=(-?\d+) key_matches=(\d+) backward_nodes=(\d+)", text) + need(match is not None, "result line") + return dict(target=match[1], max_length=int(match[2]), shortest=int(match[3]), + key_matches=int(match[4]), nodes=int(match[5])) + + +def main() -> None: + full = "--full" in sys.argv[1:] + workers = str(min(16, max(1, os.cpu_count() or 1))) + pins() + upper_bound_word() + with tempfile.TemporaryDirectory() as tmp: + binary = compile_engine(Path(tmp)) + bound = bind_semantics(binary) + need("selftest commuting_ordered_pairs=1584 ball2=4297 verified_words=12" in run(binary, "selftest"), + "commuting pairs, exact radius-two ball and distance-five verification") + counts = run(binary, "count", "4", "26") + for depth, value in COUNTS.items(): + need(f"depth<={depth} distinct={value}" in counts, f"distinct states at depth <= {depth}") + for target, cost in CONTROLS: + for mode in ("sym", "nosym"): + short = parse_result(run(binary, target, "3", "2", mode, workers, "24")) + need(short["shortest"] == -1 and short["key_matches"] == 0, f"{target} {mode}: nothing at length <= 5") + found = parse_result(run(binary, target, "3", "3", mode, workers, "24")) + need(found["shortest"] == cost, f"{target} {mode}: shortest length {cost} found") + nosym = parse_result(run(binary, "c3c3", "3", "3", "nosym", workers, "24")) + need(nosym["shortest"] == -1 and nosym["key_matches"] == 0, "c3c3: nothing at length <= 6 without symmetry") + mixed = parse_result(run(binary, "c3s01", "4", "4", "sym", workers, "26")) + need(mixed["shortest"] == -1, "c3s01: nothing at length <= 8") + main_run = run(binary, "c3c3", "4", "5", "sym", workers, "26") + need("symmetries=36 pairs=142 mode=sym" in main_run, "symmetry group and pair representatives") + need(f"forward_depth=4 distinct={COUNTS[4]}" in main_run, "forward depth-four ball") + need(parse_result(main_run)["shortest"] == -1, "no word of length <= 9") + proved = 9 + if full: + for fwd, bwd, length, bits in (("4", "6", 10, "27"), ("5", "6", 11, "30")): + out = parse_result(run(binary, "c3c3", fwd, bwd, "sym", workers, bits)) + need(out["shortest"] == -1, f"no word of length <= {length}") + proved = length + print(f"PASS_SPECTATOR_THREE_CYCLE_ADDITIVITY upper=12 no_word_le_{proved} semantics_bound={bound} " + f"recorded_local_no_word_le_11 no_new_kappa") + + +if __name__ == "__main__": + main()