diff --git a/research/two-three-cycle-additivity/README.md b/research/two-three-cycle-additivity/README.md new file mode 100644 index 0000000000..6bbd51f92a --- /dev/null +++ b/research/two-three-cycle-additivity/README.md @@ -0,0 +1,115 @@ +# Two 3-cycles cost twelve calls + +**Exact computer-assisted result in a formal model. No new κ.** +The selected conditional exponent stays 60403/20000000. + +## Result + +The setting is the formal model `M_2(F2[GL_3(F2)])` of #4939/#4950/#4968: + +- A paid call is `D(g,N) = I + ([g]+[e])N`, where `g` is one of the six + coordinate CNOTs and `N = uvᵀ` is a rank-one binary idempotent. +- Free scalar `GL_2(F2)` maps are allowed. +- Equality is formal, on arbitrary inputs. + +Let `c` be a coordinate 3-cycle. Then + +```text +diag([c],[c]) has no realizing word of length ≤ 11, so its cost is exactly 12. +``` + +The upper bound 12 is a shortest 3-cycle word (length 6) on each register. So +two 3-cycles share no paid work across the two registers: the cost is additive. + +This answers the open question of [#4968](https://github.com/CrocSwap/integer-mult-bounds/pull/4968) +for its smallest case. #4974's support lemma gives exactly `ℓ_{GL_n}(g)` for a +single target, but support alone only bounds the largest target. The +permutation cuts of #4968 do not even certify a single 3-cycle; they reach +about 3.5 of 6. + +## Method + +`search.c` is an exact meet-in-the-middle search. Free scalar maps are +normalized away (#4939 step 1). Every paid call is an involution, so a word of +length `L ≤ 11` gives `T·W = X`, with `X` a product of at most 5 calls and `W` +of at most 6 calls. Consecutive equal letters cancel and are skipped. + +- **Forward.** A depth-first search from `I` to depth ≤ 5 stores a 61-bit + fingerprint with the minimum depth for each of the **16,292,362** distinct + states. +- **Backward.** A depth-first search from `T` to depth ≤ 6 looks up every + state. Fingerprints are deterministic, so a real solution always matches its + key. A key match would be re-verified by an exact forward re-search. The + run records **zero key matches**, which excludes every word of length ≤ 11. +- **Symmetry.** The target and the generator set are fixed by 36 maps: + entrywise automorphisms of `GL_3(F2)` that fix `c` (conjugation by powers of + `c`, optionally composed with inverse-transpose), times conjugation by + `GL_2(F2)` on the registers. These maps are algebra automorphisms that fix + `T`. If `T·W = X`, then `T·φ(W) = φ(X)`, and `φ(X)` lies in the same forward + ball. So the backward first letter can range over orbit representatives, and + here all 36 generators form one orbit. The search is also repeated **without + this reduction**, over all 36 first letters in parallel shards, again with + zero key matches. + +## Evidence + +`verify.py` uses the standard library and a C11 compiler. It takes about +75 s locally with 9 parallel shards. It checks: + +1. **Compilation.** `search.c` compiles with `-Wall -Wextra -Werror`. +2. **Semantics.** The C products agree with the merged Python formal model + (`research/swap-component-cut/formal.py`) on 84 random words of length + 0–6, as exact group-algebra states. +3. **State counts.** The distinct states at depth ≤ 1, 2, 3, 4 are 37, 1,033, + 26,551 and 663,496, matching the Python search. +4. **Positive controls.** `diag([c],[e])`, `diag([s01],[s12])` and + `diag([s01],[s01])` have nothing at length ≤ 5, and their shortest length 6 + is found. The two swap cases match #4950/#4968. +5. **Upper bound.** The 12-call attaining word is checked in Python. +6. **Main search.** It runs with symmetry (36 symmetries, one orbit) and + without it (36 first letters). Both give zero key matches. + +Breaking the generator product in `search.c`, or perturbing the forward-ball +count, makes the verifier fail. + +## Scope + +Card `bit-new-register-model`, scope **changed** (see `TASK.json`). This is a +negative formal-model screen. It does not satisfy the card's native +construction gate. + +This package covers only `n = 3` and `R = 2`. It does **not** settle: +- a third dirty, restored register; +- spectator address coordinates (`n ≥ 4`); +- other multi-target cases, such as transposition paths or stars on four or + more coordinates; +- native operations, tariffs or κ. + +Base: canonical main `f259dabc7d70e0db8d6d36bfda888f008bbfecc1`, priority +revision 7. +Claim: [#1166 comment](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19139334). + +## Reproduce + +```sh +python3.12 -I -B research/two-three-cycle-additivity/verify.py +python3.12 -B scripts/research_package.py --package research/two-three-cycle-additivity +``` + +## Open next questions + +1. **Does a dirty third register or a spectator coordinate let two 3-cycles + share work?** For swaps, neither helps. For 3-cycles, only `R = 2`, `n = 3` + is settled here. *First step:* run the same engine at `R = 3`, with 168 + generators. First measure the growth of the ball and add symmetry under + register conjugation fixing `diag(c,c,e)`. *Blocked by:* search size only. + +## Credit + +- Mihir Srivastava (#4939), for the formal model. +- JoyboyBrian (#4974), for the single-target support lemma. +- PR1989, the GL2 corollary, commdata2338 (PR1414/PR1495), PR1541 and Gareth + Davidson (PR1333), as credited in #4950/#4968. + +Prepared by James Reed with substantial Anthropic Claude (Claude Code) +assistance. Apache-2.0. No independent human review is claimed. diff --git a/research/two-three-cycle-additivity/SOURCES.json b/research/two-three-cycle-additivity/SOURCES.json new file mode 100644 index 0000000000..cf302e2288 --- /dev/null +++ b/research/two-three-cycle-additivity/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/swap-component-cut/formal.py", + "usage": "input", + "git_blob": "eb3058c3593e3373a417f9b6c2d566ca409b591d", + "sha256": "e23c71e52a52ee6466a8d07c3608ebe38015cdc959c92f9e8a57557c9ef68628" + }, + { + "path": "research/swap-component-cut/README.md", + "usage": "provenance", + "git_blob": "19eaadc4ea40e312d202c917e2f1914d98ca224a", + "sha256": "7fe7efcb948a71af664d8f7828c8f4a056de3c6c3aa2cb82e420ec6ae7bd0106" + } + ] +} diff --git a/research/two-three-cycle-additivity/TASK.json b/research/two-three-cycle-additivity/TASK.json new file mode 100644 index 0000000000..e9ccfa4f0d --- /dev/null +++ b/research/two-three-cycle-additivity/TASK.json @@ -0,0 +1,64 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "f259dabc7d70e0db8d6d36bfda888f008bbfecc1", + "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 whether two coordinate 3-cycles, diag([c],[c]) at n = 3 with R = 2 registers, can be realized by fewer than twelve paid calls in the formal M_R(F2[GL_n(F2)]) model (the open question of PR #4968).", + "scope_change_reason": "PR #4968 (merged) left additivity across several non-transposition targets open; #4974 settled single targets via support. This package settles the smallest open multi-target case exactly. It does not cover extra dirty registers (R >= 3), address spectators (n >= 4) or other targets.", + "bottleneck_link": "It shows that two 3-cycles share no paid work across registers in this formal model, extending the swap results. Any saving needs a changed operation or tariff.", + "budget_minutes": 60, + "stop_rule": "Stop at the exact length-11 exclusion with positive controls and a symmetry-free confirmation. Do not extend to R = 3 or n = 4 in this package.", + "outcome": "completed", + "evidence": "python3.12 -B scripts/research_package.py --package research/two-three-cycle-additivity", + "author": "James Reed", + "ai_assistance": "Substantial assistance from Anthropic Claude (Claude Code, Opus 5.5).", + "open_questions": [ + { + "question": "Does a third (dirty, restored) register or a spectator address coordinate let two 3-cycles share work, i.e. is diag([c],[c],[e]) at R = 3, or the same target at n = 4, still twelve?", + "why_it_matters": "For swaps, dirty registers and spectators provably do not help (#4950, #4968). For 3-cycles only the R = 2, n = 3 case is now settled; permutation cuts cannot certify it, so the general case needs a new argument.", + "first_step": "Run the same meet-in-the-middle engine at R = 3 (168 generators); the depth-5 ball is far larger, so first measure growth and add symmetry reduction under GL_3(F2) register conjugation fixing diag(c,c,e).", + "blocked_by": "Search size at R = 3; nothing else." + } + ] +} diff --git a/research/two-three-cycle-additivity/VERIFY.json b/research/two-three-cycle-additivity/VERIFY.json new file mode 100644 index 0000000000..8066765400 --- /dev/null +++ b/research/two-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 with -std=c11 -Wall -Wextra -Werror; bind the C engine to the Python formal model on 84 random words by exact state comparison; reproduce distinct-state counts 37/1033/26551/663496; positive controls c3e, s01s12, s01s01 (nothing at length <= 5, shortest 6); twelve-call attaining word in Python; main search for diag([c],[c]) at depth 5+6 with symmetry reduction (36 symmetries, one first-letter orbit, 16,292,362 forward states, zero key matches) and a symmetry-free confirmation over all 36 first letters in parallel shards with zero key matches." + } + ] +} diff --git a/research/two-three-cycle-additivity/search.c b/research/two-three-cycle-additivity/search.c new file mode 100644 index 0000000000..0c979c1942 --- /dev/null +++ b/research/two-three-cycle-additivity/search.c @@ -0,0 +1,354 @@ +/* Exact meet-in-the-middle search in the formal model M_2(F2[GL_3(F2)]). + * + * A paid call is D(g,N) = I + ([g]+[e]) N, with g one of the six coordinate + * CNOTs of GL_3(F2) and N one of the six rank-one binary idempotents u v^T + * (v.u = 1) of M_2(F2). Free scalar maps are normalized away (#4939 step 1), + * so words consist of paid calls only. Every call is an involution, so if + * T * W = X with X a product of k calls, then T = X * reverse(W) has length + * k + |W|. Consecutive equal letters cancel and are skipped. + * + * Usage: + * search count distinct states at depths <= 1..d + * search dump ... print the product state, entry bits + * search [sym|nosym] [lo hi] + * targets: c3c3 c3e s01s12 s01s01 + * sym (default): first backward letter over orbit representatives of the + * generator set under symmetries fixing the target and generator set; + * nosym: every first letter in [lo, hi) (default all 36). + * + * Forward: DFS from I to depth <= fwd, storing fingerprints with minimum + * depth. Backward: DFS from T to depth <= bwd, looking up every state. A + * fingerprint hit is confirmed by an exact forward re-search. Since + * fingerprints are deterministic, a real match always finds its key; the run + * prints the number of key matches, so zero matches excludes every word of + * length <= fwd + bwd. + */ +#include +#include +#include +#include + +#define NG 168 +typedef struct { uint64_t w[3]; } Set; +typedef struct { Set e[2][2]; } State; + +static int elem[NG], idx_of[512]; +static int cn[6]; +static int gen_u[6], gen_v[6]; +static Set trans[6][21][256]; + +static int mat_mul(int a, int b) { + int r = 0; + for (int i = 0; i < 3; i++) { + int row = 0, ai = (a >> (3 * i)) & 7; + for (int k = 0; k < 3; k++) if (ai >> k & 1) row ^= (b >> (3 * k)) & 7; + r |= row << (3 * i); + } + return r; +} +static int transpose3(int a) { + int r = 0; + for (int i = 0; i < 3; i++) for (int j = 0; j < 3; j++) + if ((a >> (3 * i + j)) & 1) r |= 1 << (3 * j + i); + return r; +} +static int identity3(void) { return 1 | (2 << 3) | (4 << 6); } +static int invertible(int m) { + int rows[3] = {m & 7, (m >> 3) & 7, (m >> 6) & 7}, r = 0; + for (int bit = 0; bit < 3; bit++) { + int p = -1; + for (int i = r; i < 3; 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 < 3; i++) if (i != r && (rows[i] >> bit & 1)) rows[i] ^= rows[r]; + r++; + } + return r == 3; +} +static int inverse3(int a) { + for (int i = 0; i < NG; i++) if (mat_mul(a, elem[i]) == identity3()) return elem[i]; + abort(); +} +/* row a of the result is row sigma[a] of the identity */ +static int rowperm(int s0, int s1, int s2) { + int s[3] = {s0, s1, s2}, m = 0; + for (int a = 0; a < 3; a++) m |= (1 << s[a]) << (3 * a); + return m; +} + +static void sxor(Set *a, const Set *b) { a->w[0] ^= b->w[0]; a->w[1] ^= b->w[1]; a->w[2] ^= b->w[2]; } +static void sbit(Set *s, int b) { s->w[b >> 6] |= 1ULL << (b & 63); } +static int gbit(const Set *s, int b) { return (int)((s->w[b >> 6] >> (b & 63)) & 1); } +static int steq(const State *a, const State *b) { return memcmp(a, b, sizeof *a) == 0; } + +static Set translate(int gi, const Set *s) { + Set o = {{0, 0, 0}}; + for (int byte = 0; byte < 21; byte++) { + int v = (int)((s->w[byte >> 3] >> (8 * (byte & 7))) & 255); + if (v) sxor(&o, &trans[gi][byte][v]); + } + return o; +} +static State apply(const State *x, int gen) { /* x * D(g, N) */ + int gi = gen / 6, ni = gen % 6, u = gen_u[ni], v = gen_v[ni]; + State r = *x; + Set y[2][2]; + for (int i = 0; i < 2; i++) for (int k = 0; k < 2; k++) { + y[i][k] = translate(gi, &x->e[i][k]); + sxor(&y[i][k], &x->e[i][k]); + } + for (int i = 0; i < 2; i++) { + Set z = {{0, 0, 0}}; + for (int k = 0; k < 2; k++) if (u >> k & 1) sxor(&z, &y[i][k]); + for (int j = 0; j < 2; j++) if (v >> j & 1) sxor(&r.e[i][j], &z); + } + return r; +} +static uint64_t fp(const State *s) { + uint64_t h = 0x9E3779B97F4A7C15ULL; + for (int i = 0; i < 2; i++) for (int j = 0; j < 2; j++) for (int w = 0; w < 3; w++) { + h ^= s->e[i][j].w[w] + 0x9E3779B97F4A7C15ULL + (h << 6) + (h >> 2); + h *= 0xBF58476D1CE4E5B9ULL; + h ^= h >> 31; + } + return h | 8; +} + +static uint64_t *table, tmask; +static long distinct; +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 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 < 36; g++) if (g != last) { State y = apply(x, g); fdfs(&y, depth + 1, g); } +} +static const State *goal; +static int found_depth; +static void xdfs(const State *x, int depth, int maxd, int last) { + if (steq(x, goal) && depth < found_depth) found_depth = depth; + if (depth == maxd || depth + 1 >= found_depth) return; + for (int g = 0; g < 36; g++) if (g != last) { State y = apply(x, g); xdfs(&y, depth + 1, maxd, g); } +} +static State identity_state(void) { + State s; + memset(&s, 0, sizeof s); + sbit(&s.e[0][0], idx_of[identity3()]); + sbit(&s.e[1][1], idx_of[identity3()]); + return s; +} +static int verify_exact(const State *x, int maxd) { + State s = identity_state(); + goal = x; found_depth = 99; + xdfs(&s, 0, maxd, -1); + return found_depth == 99 ? -1 : found_depth; +} + +/* symmetries: alpha (automorphism of GL_3 applied entrywise) x conjugation by S in GL_2(F2) */ +static int alpha_map[12][NG]; +static int S2[6][2], S2inv[6][2]; +static void m2mul(const int *a, const int *b, int *out) { + for (int i = 0; i < 2; i++) { + int row = 0; + for (int k = 0; k < 2; k++) if (a[i] >> k & 1) row ^= b[k]; + out[i] = row; + } +} +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 < 2; i++) for (int j = 0; j < 2; j++) + for (int b = 0; b < NG; b++) if (gbit(&x->e[i][j], b)) sbit(&t.e[i][j], alpha_map[a][b]); + for (int i = 0; i < 2; i++) for (int j = 0; j < 2; j++) for (int k = 0; k < 2; k++) + if (S2[s][i] >> k & 1) sxor(&u.e[i][j], &t.e[k][j]); + for (int i = 0; i < 2; i++) for (int j = 0; j < 2; j++) for (int k = 0; k < 2; k++) + if (S2inv[s][k] >> j & 1) sxor(&r.e[i][j], &u.e[i][k]); + return r; +} + +static void setup(void) { + int n = 0; + for (int m = 0; m < 512; m++) { + idx_of[m] = -1; + if (invertible(m)) { idx_of[m] = n; elem[n++] = m; } + } + if (n != NG) { fprintf(stderr, "GL_3(F2) order %d\n", n); exit(1); } + int c = 0; + for (int i = 0; i < 3; i++) for (int j = 0; j < 3; j++) if (i != j) { + int g = identity3(); + g ^= (1 << j) << (3 * i); + cn[c++] = idx_of[g]; + } + 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++; } + if (p != 6) exit(1); + for (int gi = 0; gi < 6; gi++) for (int byte = 0; byte < 21; byte++) for (int val = 0; val < 256; val++) { + Set o = {{0, 0, 0}}; + for (int b = 0; b < 8; b++) if (val >> b & 1) { + int x = byte * 8 + b; + if (x < NG) sbit(&o, idx_of[mat_mul(elem[x], elem[cn[gi]])]); + } + trans[gi][byte][val] = o; + } + int perms[6][3] = {{0, 1, 2}, {1, 0, 2}, {0, 2, 1}, {2, 1, 0}, {1, 2, 0}, {2, 0, 1}}; + int na = 0; + for (int pi = 0; pi < 6; pi++) for (int t = 0; t < 2; t++) { + int P = rowperm(perms[pi][0], perms[pi][1], perms[pi][2]), Pinv = inverse3(P); + for (int x = 0; x < NG; x++) { + int y = mat_mul(mat_mul(P, elem[x]), Pinv); + if (t) y = transpose3(inverse3(y)); + alpha_map[na][x] = idx_of[y]; + } + na++; + } + int ns = 0; + for (int r0 = 1; r0 < 4; r0++) for (int r1 = 1; r1 < 4; r1++) if (r0 != r1) { + S2[ns][0] = r0; S2[ns][1] = r1; + for (int q0 = 1; q0 < 4; q0++) for (int q1 = 1; q1 < 4; q1++) { + int qq[2] = {q0, q1}, out[2]; + m2mul(S2[ns], qq, out); + if (out[0] == 1 && out[1] == 2) { S2inv[ns][0] = q0; S2inv[ns][1] = q1; } + } + ns++; + } +} + +static void print_state(const State *s) { + for (int i = 0; i < 2; i++) for (int j = 0; j < 2; j++) { + printf("entry %d %d:", i, j); + for (int b = 0; b < NG; b++) if (gbit(&s->e[i][j], b)) printf(" %d", elem[b]); + printf("\n"); + } +} + +int main(int argc, char **argv) { + setup(); + if (argc < 2) return 2; + if (!strcmp(argv[1], "count")) { + int d = atoi(argv[2]); + table = calloc(1ULL << 26, 8); tmask = (1ULL << 26) - 1; + if (!table) return 3; + for (fwd_max = 1; fwd_max <= d; fwd_max++) { + memset(table, 0, (1ULL << 26) * 8); distinct = 0; + State s = identity_state(); + fdfs(&s, 0, -1); + printf("depth<=%d distinct=%ld\n", fwd_max, distinct); + } + return 0; + } + if (!strcmp(argv[1], "dump")) { + State s = identity_state(); + for (int i = 2; i < argc; i++) s = apply(&s, atoi(argv[i])); + print_state(&s); + return 0; + } + if (argc < 4) return 2; + int a, b; + int C3 = rowperm(1, 2, 0), S01 = rowperm(1, 0, 2), S12 = rowperm(0, 2, 1), E = identity3(); + if (!strcmp(argv[1], "c3c3")) { a = C3; b = C3; } + else if (!strcmp(argv[1], "c3e")) { a = C3; b = E; } + else if (!strcmp(argv[1], "s01s12")) { a = S01; b = S12; } + else if (!strcmp(argv[1], "s01s01")) { a = S01; b = S01; } + else return 2; + fwd_max = atoi(argv[2]); + int bwd_max = atoi(argv[3]); + int use_sym = !(argc > 4 && !strcmp(argv[4], "nosym")); + int lo = argc > 6 ? atoi(argv[5]) : 0, hi = argc > 6 ? atoi(argv[6]) : 36; + State T; + memset(&T, 0, sizeof T); + sbit(&T.e[0][0], idx_of[a]); + sbit(&T.e[1][1], idx_of[b]); + + State gstate[36], I = identity_state(); + for (int g = 0; g < 36; g++) gstate[g] = apply(&I, g); + int parent[36], first_ok[36], nsym = 0; + for (int g = 0; g < 36; g++) parent[g] = g; + for (int al = 0; al < 12; al++) for (int s = 0; s < 6; s++) { + State pt = phi(&T, al, s); + if (!steq(&pt, &T)) continue; + int okset = 1, img[36]; + for (int g = 0; g < 36 && okset; g++) { + State pg = phi(&gstate[g], al, s); + img[g] = -1; + for (int h = 0; h < 36; h++) if (steq(&pg, &gstate[h])) { img[g] = h; break; } + if (img[g] < 0) okset = 0; + } + if (!okset) continue; + nsym++; + for (int g = 0; g < 36; g++) { + int x = g, y = img[g]; + while (parent[x] != x) x = parent[x]; + while (parent[y] != y) y = parent[y]; + if (x != y) parent[y] = x; + } + } + int reps = 0; + for (int g = 0; g < 36; g++) { + int x = g; + while (parent[x] != x) x = parent[x]; + first_ok[g] = use_sym ? (x == g) : (g >= lo && g < hi); + reps += first_ok[g]; + } + printf("target=%s symmetries=%d first_letters=%d mode=%s\n", argv[1], nsym, reps, use_sym ? "sym" : "nosym"); + + table = calloc(1ULL << 26, 8); tmask = (1ULL << 26) - 1; + if (!table) return 3; + State s0 = identity_state(); + fdfs(&s0, 0, -1); + printf("forward_depth=%d distinct=%ld\n", fwd_max, distinct); + + int best = 99, word[16], gnext[16], depth = 0; + long key_matches = 0, nodes = 0; + State stack[16]; + stack[0] = T; gnext[0] = 0; + if (use_sym || lo == 0) { + int k = lookup(fp(&T)); + if (k >= 0) { key_matches++; int e = verify_exact(&T, k); if (e >= 0) best = e; } + } + while (depth >= 0) { + if (depth == bwd_max || gnext[depth] >= 36) { depth--; continue; } + int g = gnext[depth]++; + if (depth > 0 && g == word[depth - 1]) continue; + if (depth == 0 && !first_ok[g]) continue; + word[depth] = g; + stack[depth + 1] = apply(&stack[depth], g); + gnext[depth + 1] = 0; + int d = depth + 1; + nodes++; + int k = lookup(fp(&stack[d])); + if (k >= 0) { + key_matches++; + if (k + d < best) { + int e = verify_exact(&stack[d], k); + if (e >= 0 && e + d < best) { + best = e + d; + printf("hit total=%d forward=%d backward_word=", best, e); + for (int i = 0; i < d; i++) printf("%d%s", word[i], i + 1 < d ? "," : "\n"); + } + } + } + depth = d; + } + printf("RESULT target=%s max_length=%d shortest=%d key_matches=%ld backward_nodes=%ld\n", + argv[1], fwd_max + bwd_max, best == 99 ? -1 : best, key_matches, nodes); + return 0; +} diff --git a/research/two-three-cycle-additivity/verify.py b/research/two-three-cycle-additivity/verify.py new file mode 100644 index 0000000000..f2f3f8ddb2 --- /dev/null +++ b/research/two-three-cycle-additivity/verify.py @@ -0,0 +1,158 @@ +#!/usr/bin/env python3 +"""Two coordinate 3-cycles cost twelve calls in M_2(F2[GL_3(F2)]). + +Standard library only. Needs a C compiler (cc) for the exact search. +The C engine is bound to the merged Python formal model of #4968 +(research/swap-component-cut/formal.py) by exact state comparison on random +words, then reproduces distinct-state counts and three known minima before +the main search. The main search is run twice: with the symmetry reduction, +and without it in parallel first-letter shards. 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 pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +PACKAGE = ROOT / "research" / "two-three-cycle-additivity" +sys.path.insert(0, str(ROOT / "research" / "swap-component-cut")) + +import formal # noqa: E402 + +COUNTS = {1: 37, 2: 1033, 3: 26551, 4: 663496} +FORWARD_DISTINCT = 16292362 + + +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"] == "60403/20000000", "selected kappa") + + +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 = 900) -> 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 << (3 * i) for i, row in enumerate(group_element)) + + +def bind_semantics(binary: Path) -> int: + model = formal.Model(3, 2) + rng = random.Random(4968) + checked = 0 + for length in list(range(0, 7)) * 12: + word = [rng.randrange(36) for _ in range(length)] + product = model.diagonal([]) + for g in word: + product = formal.matrix_product(product, model.generators[g], 2, 3) + expected = {} + for i in range(2): + for j in range(2): + expected[(i, j)] = sorted(c_int(x) for x in product[i][j]) + 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: + """The 12-call word: a shortest 3-cycle word on each register (projectors E00, E11).""" + model = formal.Model(3, 2) + c3 = formal.row_permutation(3, (1, 2, 0)) + cnots = formal.cnots(3) + lengths = formal.word_lengths(3) + need(lengths[c3] == 6, "3-cycle has CNOT length six") + # find a six-letter CNOT word whose formal product is c3 + from itertools import product as words + word = next(w for w in words(range(6), repeat=6) + if formal.mul(formal.mul(formal.mul(cnots[w[0]], cnots[w[1]], 3), formal.mul(cnots[w[2]], cnots[w[3]], 3), 3), + formal.mul(cnots[w[4]], cnots[w[5]], 3), 3) == c3) + e00, e11 = 0, 2 # projector order (1,1),(1,3),(2,2),(2,3),(3,1),(3,2) + calls = [6 * g + e00 for g in word] + [6 * g + e11 for g in word] + product = model.diagonal([]) + for g in calls: + product = formal.matrix_product(product, model.generators[g], 2, 3) + need(product == 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: + pins() + upper_bound_word() + with tempfile.TemporaryDirectory() as tmp: + binary = compile_engine(Path(tmp)) + bound = bind_semantics(binary) + counts = run(binary, "count", "4") + for depth, value in COUNTS.items(): + need(f"depth<={depth} distinct={value}" in counts, f"distinct states at depth <= {depth}") + for target in ("c3e", "s01s12", "s01s01"): + short = parse_result(run(binary, target, "3", "2")) + need(short["shortest"] == -1 and short["key_matches"] == 0, f"{target}: nothing at length <= 5") + six = parse_result(run(binary, target, "3", "3")) + need(six["shortest"] == 6, f"{target}: shortest length six found") + main_run = run(binary, "c3c3", "5", "6", "sym") + need("symmetries=36 first_letters=1 mode=sym" in main_run, "symmetry group and orbit representatives") + need(f"forward_depth=5 distinct={FORWARD_DISTINCT}" in main_run, "forward ball size") + reduced = parse_result(main_run) + need(reduced["shortest"] == -1 and reduced["key_matches"] == 0, "no word of length <= 11 (symmetry-reduced)") + # Symmetry-free confirmation: every first letter, in parallel shards. + shards = min(9, max(1, (os.cpu_count() or 1))) + bounds = [round(36 * k / shards) for k in range(shards + 1)] + processes = [subprocess.Popen([str(binary), "c3c3", "5", "6", "nosym", str(lo), str(hi)], + stdout=subprocess.PIPE, stderr=subprocess.PIPE, text=True) + for lo, hi in zip(bounds, bounds[1:]) if lo < hi] + letters = matches = 0 + for process in processes: + out, err = process.communicate(timeout=1500) + need(process.returncode == 0, "nosym shard failed: " + err) + letters += int(re.search(r"first_letters=(\d+)", out)[1]) + result = parse_result(out) + need(result["shortest"] == -1, "nosym shard found a short word") + matches += result["key_matches"] + need(letters == 36 and matches == 0, "symmetry-free search covers all 36 first letters with no key match") + print(f"PASS_TWO_THREE_CYCLE_ADDITIVITY shortest=12 no_word_le_11 semantics_bound={bound} " + f"forward_distinct={FORWARD_DISTINCT} nosym_shards={len(processes)} no_new_kappa") + + +if __name__ == "__main__": + main()