diff --git a/research/ut4-two-target-r2/README.md b/research/ut4-two-target-r2/README.md new file mode 100644 index 0000000000..9a3814549a --- /dev/null +++ b/research/ut4-two-target-r2/README.md @@ -0,0 +1,115 @@ +# No fourteen-call two-target UT4 word on two roles + +**Exhaustive finite negative result in one explicit alphabet. No new κ; the selected record is unchanged.** + +[CrocSwap/integer-mult-bounds#1662](https://github.com/CrocSwap/integer-mult-bounds/pull/1662) (@ToikY, head +`01cc02b164ecc4f9d84df3f56a1fe65b88daf390`) proves that two central targets need at least 14 paid calls +in its `F2[UT4(F2)]` alphabet, and the direct word `(abcb)^2` per target uses 16. Its open next question +asks whether 14 is attainable. This package answers it for words with **no extra roles**: + +> With r = w = 2, no word of 14 paid factors `I+([g]+1)xy^T` (g in {a,b,c}, x, y nonzero in F2^2) +> equals `I+([z]+1)I_2`. No such word even reaches the degree-three quotient endpoint. + +**With CrocSwap/integer-mult-bounds#1680, this covers every workspace size.** @ToikY's concurrent +[CrocSwap/integer-mult-bounds#1680](https://github.com/CrocSwap/integer-mult-bounds/pull/1680) (head +`a281330e84e64ad357e35b338796c96144a345ce`) proves in writing that every 14- or 15-call two-target word with +any finite r ≥ 2 compresses to a word on exactly two roles. Factors are dropped, never added, and +CrocSwap/integer-mult-bounds#1662 excludes 13 calls or fewer. Together the two give: **two central targets need at least 15 calls +for every finite r**, so the tariff interval is 15..16. That corollary is conditional on CrocSwap/integer-mult-bounds#1680's written +lemma, which this package does not re-derive or audit. + +## Model and what is relied on + +The alphabet, target and counting rules are CrocSwap/integer-mult-bounds#1662's: every factor is counted, scalar mixing is free, and +there is no COPY, ERASE or clean workspace. With r = 2 there are nine couplings `xy^T` per letter. +CrocSwap/integer-mult-bounds#1662's written theorem (`n_a, n_c ≥ 2w`, `n_b ≥ 3w`) forces the counts (4,6,4) on a 14-call word. That +theorem is cited, not re-derived here. Everything else is checked in this package. + +## Method + +Let `Q = F2/(a², b², c², ac−ca, degree ≥ 4)`, the quotient CrocSwap/integer-mult-bounds#1662 uses. `verify.py` independently +checks that `g ↦ 1+g` extends to a multiplicative map `UT4(F2) → Q` on all 4,096 pairs, with +`z ↦ 1+abc+acb+bac+cba`. Every coefficient of the target's image in `M_2(Q)` is therefore a necessary +condition. + +1. **Middle sequences.** These are the six b-couplings with zero sum (33,489 sequences). Conjugation by + GL2(F2) fixes the target, so only the 5,582 conjugation-minimal ones are searched; their orbits are + checked to cover all 33,489. +2. **Profiles.** Write `P_j` for the sum of a-couplings before the j-th b-call and `Q_j` for the sum of + c-couplings after it. With zero a- and c-totals, the a/b-only coefficients + `ab = Σ P_j N_j`, `ba = Σ N_j P_j`, `aba = Σ P_j N_j P_j` and + `bab = Σ_{j=3 (49 couplings per factor) in this session.", + "outcome": "negative-result", + "evidence": "verify.py: quotient map multiplicative on all 4096 UT4(F2) pairs; GL2(F2) orbit representatives (5582) cover all 33489 zero-sum middle sequences; direct 16-call word passes and its 16 omissions fail; exhaustive search over 20791 profiles per side leaves 208 profile pairs and 3248 words, none of which passes the degree-three quotient or the full formal endpoint. test_package.py adds random formula cross-checks, indexed-versus-brute-force key pairing, planted-word completeness and r=1 driver controls. With https://github.com/CrocSwap/integer-mult-bounds/pull/1680 (head a281330e84e64ad357e35b338796c96144a345ce; written lemma: every 14/15-call two-target word with r>=2 compresses to two roles), this excludes 14 calls for every finite r; that corollary is conditional on CrocSwap/integer-mult-bounds#1680 and not re-derived here.", + "author": "Aaron Wang / navinor", + "ai_assistance": "Substantial AI assistance from Claude Code in derivation, implementation, verification and writing; no independent human review.", + "open_questions": [ + { + "question": "Is 15 attainable for two central targets at r=2 (and therefore, by CrocSwap/integer-mult-bounds#1680, for every r)?", + "why_it_matters": "It fixes the exact two-target cost at 15 or shows the direct 16-call word is optimal for every workspace size.", + "first_step": "Run this pipeline on the splits (5,6,4), (4,7,4) and (4,6,5) allowed by CrocSwap/integer-mult-bounds#1662's bound.", + "blocked_by": "fast_search is specialised to (4,6,4); it needs separate a/c profile sets for unequal counts and seven middle calls (9^7 sequences before symmetry)." + }, + { + "question": "Does CrocSwap/integer-mult-bounds#1680's compression lemma survive an independent check?", + "why_it_matters": "The every-r corollary of this package rests on it.", + "first_step": "Replay CrocSwap/integer-mult-bounds#1680's compression fixtures through this package's separately written formal checker (formal_ok).", + "blocked_by": "The lemma is a written argument; finite fixtures corroborate it but cannot replace proof review." + } + ] +} diff --git a/research/ut4-two-target-r2/VERIFY.json b/research/ut4-two-target-r2/VERIFY.json new file mode 100644 index 0000000000..f963cd35d6 --- /dev/null +++ b/research/ut4-two-target-r2/VERIFY.json @@ -0,0 +1,27 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "quotient homomorphism on all 4096 pairs, GL2 orbit coverage, direct 16-call positive control and 16 omissions, exhaustive r=2 (4,6,4) search with recorded counts and no formal solution (~3 min)" + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 400, + "checks": "random cross-checks of profile and key formulas against direct quotient products, indexed versus brute-force key pairing, planted-word enumeration completeness, r=1 driver positive and negative controls (~1-2 min)" + } + ] +} diff --git a/research/ut4-two-target-r2/search.py b/research/ut4-two-target-r2/search.py new file mode 100644 index 0000000000..62c56bd121 --- /dev/null +++ b/research/ut4-two-target-r2/search.py @@ -0,0 +1,465 @@ +#!/usr/bin/env python3 +"""Exhaustive search for short two-target UT4(F2) central words without extra roles. + +Model (CrocSwap/integer-mult-bounds#1662): paid factors I + ([g]+1) x y^T over F2[UT4(F2)], g in {a,b,c}; +target I + ([z]+1) diag(I_w, 0). Words are lists of (label, x, y) in product order; +x, y are nonzero bit vectors over the r roles. Standard library only. + +Aaron Wang / navinor, with help from Claude Code. Apache-2.0. +""" +import itertools + +# ---------- UT4(F2) and its group algebra (elements are 64-bit masks) ---------- +POS = ((0, 1), (1, 2), (2, 3), (0, 2), (1, 3), (0, 3)) + + +def mat(bits): + rows = [1 << i for i in range(4)] # row i, bit j = entry (i, j) + for k, (i, j) in enumerate(POS): + if bits >> k & 1: + rows[i] |= 1 << j + return tuple(rows) + + +def mmul4(A, B): + out = [] + for i in range(4): + row = 0 + for k in range(4): + if A[i] >> k & 1: + row ^= B[k] + out.append(row) + return tuple(out) + + +G = [mat(b) for b in range(64)] +idx = {g: i for i, g in enumerate(G)} +assert len(idx) == 64 +MUL = [[idx[mmul4(g, h)] for h in G] for g in G] +E = idx[mat(0)] +GEN = {'a': idx[mat(1)], 'b': idx[mat(2)], 'c': idx[mat(4)]} +Z = mat(32) + + +def amul(u, v): + out = 0 + while u: + g = (u & -u).bit_length() - 1 + u &= u - 1 + row, w = MUL[g], v + while w: + h = (w & -w).bit_length() - 1 + w &= w - 1 + out ^= 1 << row[h] + return out + + +def formal(word, r): + M = [[(1 << E) if i == j else 0 for j in range(r)] for i in range(r)] + for g, x, y in word: + d = (1 << GEN[g]) | (1 << E) # [g] + 1 + for i in range(r): + s = 0 + for k in range(r): + if x >> k & 1: + s ^= amul(M[i][k], d) # (M x)(g+1) + if s: + for j in range(r): + if y >> j & 1: + M[i][j] ^= s + return M + + +def formal_ok(word, r, w): + zz = 1 << idx[Z] + T = [[(zz if i < w else 1 << E) if i == j else 0 for j in range(r)] for i in range(r)] + return formal(word, r) == T + + +# ---------- r x r binary matrices as bit masks (bit i*r+j) ---------- +def mm(A, B, r): + out = 0 + for i in range(r): + for j in range(r): + s = 0 + for k in range(r): + s ^= (A >> (i * r + k)) & (B >> (k * r + j)) & 1 + out |= s << (i * r + j) + return out + + +def rank_one(x, y, r=2): + return sum(1 << (i * r + j) for i in range(r) for j in range(r) if x >> i & 1 and y >> j & 1) + + +def split(N, r=2): + rows = [(N >> (i * r)) & ((1 << r) - 1) for i in range(r)] + y = next(v for v in rows if v) + x = sum(1 << i for i, v in enumerate(rows) if v) + assert all(v in (0, y) for v in rows) and rank_one(x, y, r) == N + return x, y + + +def diag(w, r): + return sum(1 << (i * r + i) for i in range(w)) + + +# ---------- degree-three quotient Q = F2/(a^2,b^2,c^2,ac-ca,deg>=4) ---------- +def reduce(m): + if len(m) > 3: + return None + while 'ca' in m: + m = m.replace('ca', 'ac') + return None if any(m[i] == m[i + 1] for i in range(len(m) - 1)) else m + + +def q_image(word, r): + st = {'': diag(r, r)} + for g, x, y in word: + N = rank_one(x, y, r) + new = dict(st) + for m, M in st.items(): + m2 = reduce(m + g) + if m2 is not None: + new[m2] = new.get(m2, 0) ^ mm(M, N, r) + st = {m: M for m, M in new.items() if M} + return st + + +def q_ok(word, r, w): + P = diag(w, r) + return q_image(word, r) == {'': diag(r, r), **({m: P for m in ('abc', 'acb', 'bac', 'cba')} if P else {})} + + +def prefix_profile(word, g): + """Sum of g-couplings before each b, in product order.""" + out, s = [], 0 + for h, x, y in word: + if h == g: + s ^= rank_one(x, y) + elif h == 'b': + out.append(s) + return out + + +def suffix_profile(word, g): + return prefix_profile(word[::-1], g)[::-1] + + +def side_coeffs(bseq, P, r=2): + """(ab, ba, aba, bab) for an a-profile P with zero a-total; the same formula gives + (cb, bc, cbc, bcb) for a c-suffix profile with zero c-total (characteristic two).""" + ab = ba = aba = bab = 0 + for j, (N, p) in enumerate(zip(bseq, P)): + pn = mm(p, N, r) + ab ^= pn + ba ^= mm(N, p, r) + aba ^= mm(pn, p, r) + for k in range(j + 1, len(bseq)): + bab ^= mm(mm(N, P[k] ^ p, r), bseq[k], r) + return ab, ba, aba, bab + + +def cross_coeffs(bseq, P, Q, r=2): + """(abc, cba) for zero a- and c-totals.""" + abc = cba = 0 + for N, p, q in zip(bseq, P, Q): + abc ^= mm(mm(p, N, r), q, r) + cba ^= mm(mm(q, N, r), p, r) + return abc, cba + + +# ---------- fast r = 2 screen: per-position tables and profile keys ---------- +PAR = [bin(m).count('1') & 1 for m in range(64)] + + +def side_tables(bseq, r=2): + """tab[j][p] packs (ab, ba, aba, bab) contributions of position j when P_j = p. + bab = sum_{j j: + R ^= M + tab.append([mm(p, N, r) | mm(N, p, r) << 4 | mm(mm(p, N, r), p, r) << 8 + | (mm(mm(L, p, r), N, r) ^ mm(mm(N, p, r), R, r)) << 12 for p in range(16)]) + return tab + + +def side_value(tab, P): + v = 0 + for t, p in zip(tab, P): + v ^= t[p] + return v + + +def key(bseq, P): + """(U0, U1, W0, W1): bit j of U_s is (P_j x_j)_s, bit j of W_t is (y_j^T P_j)_t.""" + U, W = [0, 0], [0, 0] + for j, (N, p) in enumerate(zip(bseq, P)): + x, y = split(N) + for s in range(2): + u = w = 0 + for k in range(2): + u ^= (p >> (2 * s + k)) & (x >> k) & 1 # (P x)_s + w ^= (y >> k) & (p >> (2 * k + s)) & 1 # (y^T P)_s + U[s] |= u << j + W[s] |= w << j + return U[0], U[1], W[0], W[1] + + +def key_cross(kp, kq): + """(abc, cba) from keys: abc_st = sum_j u_j(P)_s w_j(Q)_t, cba_st = sum_j u_j(Q)_s w_j(P)_t.""" + abc = cba = 0 + for s in range(2): + for t in range(2): + abc |= PAR[kp[s] & kq[2 + t]] << (2 * s + t) + cba |= PAR[kq[s] & kp[2 + t]] << (2 * s + t) + return abc, cba + + +_SOL = {} + + +def _sol(u0, u1, e0, e1): + """6-bit masks m with parity(u0 & m) = e0 and parity(u1 & m) = e1.""" + k = (u0, u1, e0, e1) + if k not in _SOL: + _SOL[k] = [m for m in range(64) if PAR[u0 & m] == e0 and PAR[u1 & m] == e1] + return _SOL[k] + + +def key_pairs(akeys, ckeys=None, target=(9, 9)): + """All (ka, kc) with key_cross(ka, kc) == target. The abc half fixes kc's W masks to an + affine solution set of ka's U masks, so look kc up by (W0, W1) and confirm the cba half.""" + ckeys = akeys if ckeys is None else ckeys + abc = target[0] + byW = {} + for k in ckeys: + byW.setdefault(k[2:], []).append(k) + for ka in akeys: + for m0 in _sol(ka[0], ka[1], abc & 1, abc >> 2 & 1): + for m1 in _sol(ka[0], ka[1], abc >> 1 & 1, abc >> 3 & 1): + for kc in byW.get((m0, m1), ()): + if key_cross(ka, kc) == target: + yield ka, kc + + +def check_quotient_homomorphism(): + """Define phi on UT4(F2) by BFS words in a, b, c with phi(g) = 1 + g, and check + phi(g) phi(h) = phi(gh) for all 4096 pairs in Q, plus phi(z) = 1+abc+acb+bac+cba.""" + def qmul(u, v): + out = set() + for m in u: + for n in v: + k = reduce(m + n) + if k is not None: + out ^= {k} + return frozenset(out) + + phi, frontier = {E: frozenset({''})}, [E] + while frontier: + nxt = [] + for g in frontier: + for letter, s in GEN.items(): + h = MUL[g][s] + if h not in phi: + phi[h] = qmul(phi[g], frozenset({'', letter})) + nxt.append(h) + frontier = nxt + assert len(phi) == 64 + assert all(phi[GEN[x]] == frozenset({'', x}) for x in 'abc') + assert phi[idx[Z]] == frozenset({'', 'abc', 'acb', 'bac', 'cba'}) + n = 0 + for g in range(64): + for h in range(64): + assert qmul(phi[g], phi[h]) == phi[MUL[g][h]], (g, h) + n += 1 + return n + + +# ---------- shared enumeration helpers ---------- +def couplings(r): + return [(x, y) for x in range(1, 1 << r) for y in range(1, 1 << r)] + + +def make_seqs(r, kmax): + """seqs[k][d]: ordered k-tuples of couplings summing to d.""" + seqs = [dict() for _ in range(kmax + 1)] + for k in range(kmax + 1): + for t in itertools.product(couplings(r), repeat=k): + d = 0 + for x, y in t: + d ^= rank_one(x, y, r) + seqs[k].setdefault(d, []).append(t) + return seqs + + +def profiles(nb, n, seqs): + """All prefix-sum profiles (P_1..P_nb) of n couplings in nb+1 gaps with zero total.""" + out = set() + + def rec(gap, left, s, acc): + if gap == nb: # last gap must cancel the running sum + if s in seqs[left]: + out.add(tuple(acc)) + return + for k in range(left + 1): + for d in seqs[k]: + rec(gap + 1, left - k, s ^ d, acc + [s ^ d]) + rec(0, n, 0, []) + return sorted(out) + + +def gap_choices(P, n, seqs): + """All per-gap coupling tuples realising prefix profile P with n couplings in total.""" + sums = [P[0]] + [P[j] ^ P[j - 1] for j in range(1, len(P))] + [P[-1]] if P else [0] + res = [] + + def rec(g, left, acc): + if g == len(sums): + if left == 0: + res.append(acc) + return + for k in range(left + 1): + for t in seqs[k].get(sums[g], ()): + rec(g + 1, left - k, acc + [t]) + rec(0, n, []) + return res + + +def shuffles(A, C): + """All interleavings of a-tuple A and c-tuple C within one gap.""" + n = len(A) + len(C) + out = [] + for pos in itertools.combinations(range(n), len(A)): + ia, ic, w = iter(A), iter(C), [] + for i in range(n): + w.append(('a',) + next(ia) if i in pos else ('c',) + next(ic)) + out.append(w) + return out + + +def expand(bt, P, Q, na, nc, seqs, r, w, stats, sols, seen=None): + """Every word with b-sequence bt, a-prefix profile P and c-suffix profile Q. Each is + checked against the full quotient and, independently, the full formal endpoint; + with `seen`, words are only collected (completeness tests).""" + nb = len(bt) + for ga in gap_choices(list(P), na, seqs): + for gc in gap_choices(list(Q), nc, seqs): # zero total: suffix sums equal prefix sums + for parts in itertools.product(*[shuffles(ga[j], gc[j]) for j in range(nb + 1)]): + word = [] + for j in range(nb + 1): + word += parts[j] + if j < nb: + word.append(('b',) + split(bt[j], r)) + stats['words'] += 1 + if seen is not None: + seen.append(word) + continue + stats['q_pass'] += q_ok(word, r, w) + if formal_ok(word, r, w): + stats['formal_pass'] += 1 + sols.append(tuple(word)) + + +def gl(r): + I = diag(r, r) + inv = {} + for g in range(1 << (r * r)): + for h in range(1 << (r * r)): + if mm(g, h, r) == I: + inv[g] = h + return inv + + +def middle_sequences(r, nb, symmetric): + """Zero-sum b-sequences; with symmetric=True only GL_r-conjugation-minimal ones.""" + inv = gl(r) + R1 = sorted(rank_one(x, y, r) for x, y in couplings(r)) + for bt in itertools.product(R1, repeat=nb): + tot = 0 + for N in bt: + tot ^= N + if tot: + continue + if symmetric and any(tuple(mm(mm(g, N, r), h, r) for N in bt) < bt for g, h in inv.items()): + continue + yield bt + + +# ---------- reference driver (any small r, slow formulas) ---------- +def search(r, w, counts, log=None): + na, nb, nc = counts + seqs = make_seqs(r, max(na, nc)) + PA, PC = profiles(nb, na, seqs), profiles(nb, nc, seqs) + target = diag(w, r) + stats = dict(canonical=0, a_pass=0, c_pass=0, pairs=0, words=0, q_pass=0, formal_pass=0) + sols = [] + for bt in middle_sequences(r, nb, w == r): # conjugation fixes the target only if P = I + stats['canonical'] += 1 + SA = [P for P in PA if side_coeffs(bt, P, r) == (0, 0, 0, 0)] + SC = [Q for Q in PC if side_coeffs(bt, Q, r) == (0, 0, 0, 0)] + stats['a_pass'] += len(SA) + stats['c_pass'] += len(SC) + for P in SA: + for Q in SC: + if cross_coeffs(bt, P, Q, r) == (target, target): + stats['pairs'] += 1 + expand(bt, P, Q, na, nc, seqs, r, w, stats, sols) + if log is not None: + log.update(stats) + return sols + + +# ---------- fast driver for r = w = 2, counts (4, 6, 4) ---------- +def fast_search(log=None, limit=None, bseqs=None, want=None, seen=None): + """want = (a-side value, c-side value, (abc, cba)); the default is the two-target + endpoint. Other `want`/`bseqs` values exist only for the completeness tests.""" + r = w = 2 + na, nb, nc = 4, 6, 4 + seqs = make_seqs(r, 4) + PA = profiles(nb, na, seqs) # c-suffix profiles form the same set + wa, wc, cross = want or (0, 0, (9, 9)) + stats = dict(canonical=0, profiles=len(PA), side_pass=0, keys=0, key_pairs=0, pairs=0, + words=0, q_pass=0, formal_pass=0) + sols = [] + for n, bt in enumerate(bseqs or middle_sequences(r, nb, True)): + if limit is not None and n >= limit: + break + stats['canonical'] += 1 + tab = side_tables(bt) + ga, gc = {}, {} + for P in PA: + v = side_value(tab, P) # same formula serves the c side (see side_coeffs) + if v == wa: + ga.setdefault(key(bt, P), []).append(P) + if v == wc: + gc.setdefault(key(bt, P), []).append(P) + stats['side_pass'] += sum(map(len, ga.values())) + stats['keys'] += len(ga) + for ka, kc in key_pairs(ga, gc, cross): + stats['key_pairs'] += 1 + for P in ga[ka]: + for Q in gc[kc]: + stats['pairs'] += 1 + expand(bt, P, Q, na, nc, seqs, r, w, stats, sols, seen) + if log is not None: + log.update(stats) + return sols + + +if __name__ == '__main__': + import json, sys, time + t = time.time() + stats = {} + lim = int(sys.argv[1]) if len(sys.argv) > 1 else None + sols = fast_search(stats, lim) + stats['solutions'] = len(sols) + stats['seconds'] = round(time.time() - t, 1) + print(json.dumps(stats)) + for s in sols[:5]: + print(s) diff --git a/research/ut4-two-target-r2/test_package.py b/research/ut4-two-target-r2/test_package.py new file mode 100644 index 0000000000..e6e4df1e7a --- /dev/null +++ b/research/ut4-two-target-r2/test_package.py @@ -0,0 +1,145 @@ +"""Focused tests for the r=2 two-target UT4 search (stdlib; run from anywhere).""" +import random, sys, unittest +from pathlib import Path +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import search as S + + +def direct_word(r, w): + """CrocSwap/integer-mult-bounds#1662's direct word: (abcb)^2 on each target coordinate projector.""" + word = [] + for i in range(w): + e = 1 << i + word += [(g, e, e) for g in 'abcbabcb'] + return word + + +class Formal(unittest.TestCase): + def test_group_has_64_elements_and_central_z(self): + self.assertEqual(len(S.G), 64) + z = S.idx[S.Z] + for g in range(64): + self.assertEqual(S.MUL[g][z], S.MUL[z][g]) + + def test_formal_product_is_in_word_order(self): + """On one role a factor is just [g]; the word (a, b) must give [a][b], not [b][a].""" + a, b = S.GEN['a'], S.GEN['b'] + self.assertNotEqual(S.MUL[a][b], S.MUL[b][a]) + self.assertEqual(S.formal([('a', 1, 1), ('b', 1, 1)], 1), [[1 << S.MUL[a][b]]]) + + def test_direct_sixteen_call_word_hits_target(self): + self.assertTrue(S.formal_ok(direct_word(2, 2), 2, 2)) + + def test_every_single_omission_fails(self): + word = direct_word(2, 2) + for i in range(len(word)): + self.assertFalse(S.formal_ok(word[:i] + word[i + 1:], 2, 2)) + + def test_pr1662_failed_twelve_call_trial_fails(self): + trial = [('a', 1, 1), ('b', 1, 1), ('c', 1, 3), ('a', 3, 1), ('b', 1, 1), ('c', 1, 2)] * 2 + self.assertFalse(S.formal_ok(trial, 2, 2)) + + +class Quotient(unittest.TestCase): + def test_formal_hit_implies_quotient_hit(self): + self.assertTrue(S.q_ok(direct_word(2, 2), 2, 2)) + + def test_profile_formulas_match_direct_quotient_products(self): + """The search's profile formulas assume zero a- and c-totals (the degree-one + coefficients); compare them with direct quotient products in exactly that case.""" + rng = random.Random(1662) + seen = {'a': 0, 'c': 0, 'both': 0} + for _ in range(6000): + nb = rng.randint(1, 6) + bseq = [S.rank_one(rng.randint(1, 3), rng.randint(1, 3)) for _ in range(nb)] + word = [] + for j in range(nb + 1): + gap = [(rng.choice('ac'), rng.randint(1, 3), rng.randint(1, 3)) for _ in range(rng.randint(0, 3))] + word += gap + if j < nb: + word.append(('b',) + S.split(bseq[j])) + coef = S.q_image(word, 2) + P, Q = S.prefix_profile(word, 'a'), S.suffix_profile(word, 'c') + ta, tc = coef.get('a', 0), coef.get('c', 0) + if ta == 0: + seen['a'] += 1 + self.assertEqual(S.side_coeffs(bseq, P), tuple(coef.get(m, 0) for m in ('ab', 'ba', 'aba', 'bab'))) + if tc == 0: + seen['c'] += 1 + self.assertEqual(S.side_coeffs(bseq, Q), tuple(coef.get(m, 0) for m in ('cb', 'bc', 'cbc', 'bcb'))) + if ta == 0 and tc == 0: + seen['both'] += 1 + self.assertEqual(S.cross_coeffs(bseq, P, Q), (coef.get('abc', 0), coef.get('cba', 0))) + self.assertGreater(min(seen.values()), 50, seen) + + +class FastPath(unittest.TestCase): + def setUp(self): + self.rng = random.Random(14) + + def random_bseq(self): + return [S.rank_one(self.rng.randint(1, 3), self.rng.randint(1, 3)) for _ in range(6)] + + def test_side_tables_match_side_coeffs(self): + for _ in range(200): + bseq = self.random_bseq() + tab = S.side_tables(bseq) + P = [self.rng.randrange(16) for _ in range(6)] + ab, ba, aba, bab = S.side_coeffs(bseq, P) + self.assertEqual(S.side_value(tab, P), ab | ba << 4 | aba << 8 | bab << 12) + + def test_key_cross_matches_cross_coeffs(self): + for _ in range(500): + bseq = self.random_bseq() + P = [self.rng.randrange(16) for _ in range(6)] + Q = [self.rng.randrange(16) for _ in range(6)] + self.assertEqual(S.key_cross(S.key(bseq, P), S.key(bseq, Q)), S.cross_coeffs(bseq, P, Q)) + + + def test_indexed_key_pairs_equal_brute_force(self): + hits = 0 + for _ in range(40): + keys = {tuple(self.rng.randrange(64) for _ in range(4)) for _ in range(300)} + brute = {(ka, kc) for ka in keys for kc in keys if S.key_cross(ka, kc) == (9, 9)} + self.assertEqual(set(S.key_pairs(keys)), brute) + hits += len(brute) + self.assertGreater(hits, 0) + + +class Completeness(unittest.TestCase): + def planted(self, rng): + """Random (4,6,4) word on two roles with zero a- and c-totals.""" + while True: + labels = list('aaaabbbbbbcccc') + rng.shuffle(labels) + word = [(g, rng.randint(1, 3), rng.randint(1, 3)) for g in labels] + if not S.q_image(word, 2).get('a') and not S.q_image(word, 2).get('c'): + return word + + def test_enumeration_regenerates_planted_words(self): + rng = random.Random(964) + for _ in range(2): + word = self.planted(rng) + bt = tuple(S.rank_one(x, y) for g, x, y in word if g == 'b') + tab = S.side_tables(bt) + P, Q = S.prefix_profile(word, 'a'), S.suffix_profile(word, 'c') + want = (S.side_value(tab, P), S.side_value(tab, Q), S.key_cross(S.key(bt, P), S.key(bt, Q))) + seen = [] + S.fast_search(bseqs=[bt], want=want, seen=seen) + self.assertIn(word, seen) + + def test_quotient_map_is_multiplicative(self): + self.assertEqual(S.check_quotient_homomorphism(), 4096) + + +class Driver(unittest.TestCase): + def test_one_target_eight_calls_found_at_r1(self): + sols = S.search(1, 1, (2, 4, 2)) + self.assertIn(tuple(direct_word(1, 1)), sols) + + def test_one_target_seven_calls_impossible_at_r1(self): + self.assertEqual(S.search(1, 1, (2, 3, 2)), []) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/ut4-two-target-r2/verify.py b/research/ut4-two-target-r2/verify.py new file mode 100644 index 0000000000..0ec49836c8 --- /dev/null +++ b/research/ut4-two-target-r2/verify.py @@ -0,0 +1,52 @@ +#!/usr/bin/env python3 +"""Replay the r = w = 2 fourteen-call search for two UT4(F2) central targets. + +Checks, in order: the quotient map Q is multiplicative on UT4(F2); the GL2(F2) orbit +representatives cover every zero-sum middle sequence; CrocSwap/integer-mult-bounds#1662's direct 16-call word passes +the formal endpoint and each one-call omission fails; then the exhaustive (4,6,4) search +reproduces the recorded counts with no formal solution. Standard library only, ~3 min. + +Aaron Wang / navinor, with help from Claude Code. Apache-2.0. +""" +import json, sys, time +from pathlib import Path +sys.path.insert(0, str(Path(__file__).resolve().parent)) +import search as S + +EXPECTED = { + 'canonical': 5582, 'profiles': 20791, 'side_pass': 3383566, 'keys': 805712, + 'key_pairs': 184, 'pairs': 208, 'words': 3248, 'q_pass': 0, 'formal_pass': 0, +} + + +def check(cond, msg): + if not cond: + sys.exit('FAIL: ' + msg) + print('PASS', msg) + + +def main(): + t0 = time.time() + check(S.check_quotient_homomorphism() == 4096, 'quotient map multiplicative on all 4096 pairs; phi(z)=1+abc+acb+bac+cba') + + inv = S.gl(2) + total = sum(1 for _ in S.middle_sequences(2, 6, False)) + reps = list(S.middle_sequences(2, 6, True)) + orbit = sum(len({tuple(S.mm(S.mm(g, N, 2), h, 2) for N in bt) for g, h in inv.items()}) for bt in reps) + check(len(inv) == 6 and total == 33489 and orbit == total and len(reps) == EXPECTED['canonical'], + f'GL2 orbits of {len(reps)} representatives cover all {total} zero-sum middle sequences') + + direct = [(g, e, e) for e in (1, 2) for g in 'abcbabcb'] + check(S.formal_ok(direct, 2, 2) and S.q_ok(direct, 2, 2), 'direct 16-call word hits the formal and quotient endpoints') + check(not any(S.formal_ok(direct[:i] + direct[i + 1:], 2, 2) for i in range(16)), 'all 16 one-call omissions fail') + + stats = {} + sols = S.fast_search(stats) + print(json.dumps(stats)) + check(stats == EXPECTED, 'exhaustive (4,6,4) counts match the record') + check(sols == [], 'no 14-call word on two roles reaches the two-target endpoint') + print(f'PASS_UT4_TWO_TARGET_R2_NO_14 seconds={time.time() - t0:.0f}') + + +if __name__ == '__main__': + main()