From 665bfe79d726a0cb3494326d2f63ae81d313302f Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 20 Oct 2026 23:11:21 +0100 Subject: [PATCH] feat(research): refute the right-vector general-target formula over M2(F2) Over M2(F2) at n = 2, 72 targets need 3 paid factors while min_T dim_K (M T - I) K^n is 2. The formula holds on ten commutative domains, and the trailing free map is necessary over F2 x F2 and F2[C3]. --- .../right-vector-general-target/README.md | 115 +++++++ .../right-vector-general-target/SOURCES.json | 24 ++ .../right-vector-general-target/TASK.json | 76 +++++ .../right-vector-general-target/VERIFY.json | 39 +++ .../right-vector-general-target/verify.py | 283 ++++++++++++++++++ 5 files changed, 537 insertions(+) create mode 100644 research/right-vector-general-target/README.md create mode 100644 research/right-vector-general-target/SOURCES.json create mode 100644 research/right-vector-general-target/TASK.json create mode 100644 research/right-vector-general-target/VERIFY.json create mode 100644 research/right-vector-general-target/verify.py diff --git a/research/right-vector-general-target/README.md b/research/right-vector-general-target/README.md new file mode 100644 index 0000000000..3134451a6d --- /dev/null +++ b/research/right-vector-general-target/README.md @@ -0,0 +1,115 @@ +# The right-vector column bound is not exact for every target + +**Finite certificate with a sharp counterexample. No new κ.** Selected κ stays +`0.001672660197076918`. + +Paid factors are `I + u y^T` with `u` in `R^n` and `y` in `K^n`. Free maps are +`GL_n(K)` changes of basis anywhere in a word. #4243 proved that a diagonal +target costs exactly `t_K(d)` factors, and asked in its open question 1 whether +every target `M` costs + +```text +delta(M) = min over T in GL_n(K) of dim_K (M T - I) K^n. +``` + +`delta(M)` is always a lower bound: that is #4243's normal form plus the column +bound of #4099. This package tests the upper bound on every target of eleven +small domains. + +## Result + +| Algebra `R` over `K` | n | Targets | Max cost | Formula failures | Gaps with no free map | +|---|---:|---:|---:|---:|---:| +| `F2` | 2 | 16 | 2 | 0 | 0 | +| `F3` | 2 | 81 | 2 | 0 | 0 | +| `F2` | 3 | 512 | 3 | 0 | 0 | +| `F4` over `F2` | 2 | 256 | 2 | 0 | 0 | +| `F2[C2]` | 2 | 256 | 2 | 0 | 0 | +| `F2 x F2` | 2 | 256 | 2 | 0 | **2** | +| `F3 x F3` | 2 | 6,561 | 2 | 0 | 0 | +| `F2[C3]` | 2 | 4,096 | 2 | 0 | **6** | +| `F2[x]/(x^3)` | 2 | 4,096 | 2 | 0 | 0 | +| `M2(F2)` (noncommutative) | 2 | 65,536 | 3 | **72** | **684** | +| `F2[C2]` | 3 | 262,144 | 3 | 0 | 0 | + +1. **The answer to #4243's question is no in general.** Over the matrix + algebra `M2(F2)` at `n = 2`, exactly 72 of 65,536 targets cost 3 factors + while `delta = 2`. One is the target `[[E11, E01], [E10, E00]]`. In + `M_2(M_2(F_2)) = M_4(F_2)` it is the transposition of coordinates 0 and 3. + A separate enumeration in `M_4(F_2)` confirms that no two-factor word + reaches it, that a three-factor word does, and that `T = I` already gives + image dimension 2. +2. **The formula holds on all ten commutative domains checked**: 278,274 + targets, local and non-local, including `F2[C3] = F2 x F4` and + `F3 x F3 = F3[C2]`. +3. **The minimum over `T` cannot be dropped.** Without any free map, the cost + of `M` exceeds `dim_K (M - I) K^n` on 2 targets over `F2 x F2`, 6 over + `F2[C3]` and 684 over `M2(F2)`; each such target costs 3 against dimension 2. + Over `F2 x F2` the two targets are `(A, A^{-1})` and its swap, with `A` of + order three in `GL_2(F_2)`. The fields and local algebras in the table have + no such gap. + +All counts are enumerated. Statement 1 is a counterexample to the proposed +formula; statements 2 and 3 are finite certificates on the listed domains, not +theorems for every algebra. + +## Method + +`verify.py` builds each algebra from a structure table and checks that it is +associative with `K` central. It computes the exact minimum by breadth-first +search over words in #4243's normal form `Q S`: products of paid factors +followed by one free map. It computes `delta` by enumerating every `T` in +`GL_n(K)` and taking `F_p`-ranks. It asserts `cost >= delta` everywhere and +records every target with `cost != delta`. A second search from `I` alone +gives the no-free-map cost, compared with `dim_K (M - I) K^n`. The script +writes nothing and prints a digest bound to its own bytes and results. + +## Reproduce + +From the repository root: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/right-vector-general-target/verify.py --stage main +~/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/right-vector-general-target/verify.py --stage large +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/right-vector-general-target +``` + +Expected final lines: + +```text +PASS_RIGHT_VECTOR_GENERAL_TARGET F2:n2:16 F3:n2:81 F2:n3:512 F4:n2:256 F2[C2]:n2:256 F2xF2:n2:256 F3xF3:n2:6561 F2[C3]:n2:4096 F2[x]/(x^3):n2:4096 M2(F2):n2:65536 formula_failures=M2(F2):72 no_free_map_gaps=F2xF2:2,F2[C3]:6,M2(F2):684 no_new_kappa +PASS_RIGHT_VECTOR_GENERAL_TARGET_LARGE F2[C2]:n3:262144 formula_failures=0 no_free_map_gaps=0 no_new_kappa +``` + +Each stage takes about 100 seconds on one core (CPython 3.12, NumPy 2.5.4, +macOS arm64). The asserts are the checks, so do not run with `-O`. + +## Limits + +This is an exact count in a formal alphabet. Native frames, hosting, routing, +precision and recursive cost are not priced, and no supplier changes. The +commutative agreement is checked only on the listed domains; no general proof +of the upper bound is claimed. Whether the `M2(F2)` failure transfers to a +nonabelian group algebra is not checked. Independent human and formal +proof-kernel review are unclaimed. + +## Open next questions + +1. **Commutative algebras.** Is `delta(M)` exact for every commutative + `K`-algebra, or every local one with residue field `K`? A one-factor peel + `A = A' (I + u y^T)` with `dim_K (A' - I) K^n = d - 1` exists exactly when + some `y` vanishing on the `K`-kernel of `A - I` and some `x1` with + `y . x1 = 1` give `A x1` in `A (ker y ⊗ R) + x1 R`. Proving this for a + minimizing `T` would settle the question. +2. **Group algebras.** Does the failure lift to `F2[S3]`, which has `M2(F2)` as + a block? Fix an explicit isomorphism and project words onto that block. +3. **Exact noncommutative cost.** What replaces `delta` over `M2(K)`? Compare + the cost with ranks in `M_n(M_2(K)) = M_2n(K)`. + +## Credit + +Produced by Nick Petalas. The alphabet, normal form and lower bound come from +#4243 (`research/right-vector-diagonal-free-basis`), which asked this question. +The column bound and right-vector alphabet are Wentao Li's +`research/f2-right-vector-diagonal-minimum` (#4099), building on +`research/bit-cyclic-root-barrier` (#2513). Apache-2.0. diff --git a/research/right-vector-general-target/SOURCES.json b/research/right-vector-general-target/SOURCES.json new file mode 100644 index 0000000000..86e1910e4f --- /dev/null +++ b/research/right-vector-general-target/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/f2-right-vector-diagonal-minimum/PROOF.md", + "usage": "input", + "git_blob": "274c950b24091733f919c6cdf6d75b1a783efae1", + "sha256": "e2ebc7a25d764cf24b586aa5054ae1e721d24c238eb7fac8eaa39e46e21b15d1" + } + ] +} diff --git a/research/right-vector-general-target/TASK.json b/research/right-vector-general-target/TASK.json new file mode 100644 index 0000000000..394c77a854 --- /dev/null +++ b/research/right-vector-general-target/TASK.json @@ -0,0 +1,76 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "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": "Exact paid-factor minimum for general (non-diagonal) targets in the right-vector alphabet I + u y^T (u in R^n, y in K^n) with free GL_n(K) maps: tests the formula min_T dim_K (M T - I) K^n proposed in open question 1 of #4243 on every target over eleven small (algebra, n) domains.", + "scope_change_reason": "The card asks whether a larger or nonabelian register model escapes the scoped three-register obstruction. This package answers a narrower open question left by #4243: whether its diagonal count extends to all targets. The answer is no for the noncommutative algebra M2(F2), and the trailing free map is necessary even over commutative non-local algebras.", + "bottleneck_link": "A legal target cheaper than its column bound would be a new bit primitive; this package shows the column bound is attained on ten commutative domains and is not attained in general. Kappa is unchanged.", + "budget_minutes": 60, + "stop_rule": "Exhaust every target on small algebras, record each place the formula or its no-free-map form fails, independently confirm one failure, then stop.", + "outcome": "completed", + "evidence": "verify.py --stage main and --stage large compute exact minima by breadth-first search over all words and the formula by enumerating every T in GL_n(K), on 343,810 targets in total. Formula failures: 72, all over M2(F2) at n=2 (cost 3, formula 2). No-free-map gaps: 2 over F2xF2, 6 over F2[C3], 684 over M2(F2). The transposition witness is rechecked in M_4(F_2) by a separate enumeration of all two- and three-factor products.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does the formula hold for every commutative K-algebra, or every local algebra with residue field K?", + "why_it_matters": "It holds on all ten commutative domains checked here, which include the group algebras F2[C2], F2[C3] and F3[C2]-type products.", + "first_step": "Prove the one-step peeling condition A x1 in A(H R) + x1 R for a minimizing T, starting with local R.", + "blocked_by": "No general factorization argument is proved here." + }, + { + "question": "Does the M2(F2) failure lift to a nonabelian group algebra such as F2[S3]?", + "why_it_matters": "#4243 covers diagonals in every F2[G]; a failure inside F2[S3] would bound how far its count extends for nonabelian registers.", + "first_step": "Fix an explicit K-algebra isomorphism F2[S3] = F2[C2] x M2(F2) and project words onto the matrix block.", + "blocked_by": "The isomorphism and projection argument are not checked here." + }, + { + "question": "What is the exact cost for noncommutative algebras?", + "why_it_matters": "The formula undercounts M2(F2) targets by one at n=2.", + "first_step": "Compare cost with the K^2n rank of M - I in the Morita picture M_n(M_2(K)) = M_2n(K).", + "blocked_by": "Only n=2 over M2(F2) is enumerated." + } + ] +} diff --git a/research/right-vector-general-target/VERIFY.json b/research/right-vector-general-target/VERIFY.json new file mode 100644 index 0000000000..8064f378dd --- /dev/null +++ b/research/right-vector-general-target/VERIFY.json @@ -0,0 +1,39 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [ + "numpy==2.5.4" + ], + "inputs": [ + "research/f2-right-vector-diagonal-minimum/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py", + "--stage", + "main" + ], + "timeout_seconds": 420, + "checks": "Exact minimum versus min_T dim_K (M T - I) K^n on every target over ten (algebra, n) domains, including M2(F2) at n=2; asserts the #4243 lower bound everywhere, exactly 72 formula failures (all M2(F2), cost 3 versus 2), the no-free-map gap counts 2, 6 and 684, and an independent M_4(F_2) recheck of the transposition witness." + }, + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py", + "--stage", + "large" + ], + "timeout_seconds": 420, + "checks": "Same comparison on all 262,144 targets over F2[C2] at n=3: no formula failure and no no-free-map gap." + } + ] +} diff --git a/research/right-vector-general-target/verify.py b/research/right-vector-general-target/verify.py new file mode 100644 index 0000000000..2731f6ac9c --- /dev/null +++ b/research/right-vector-general-target/verify.py @@ -0,0 +1,283 @@ +"""Exhaustive check of the right-vector general-target formula on small algebras. + +Alphabet (research/f2-right-vector-diagonal-minimum, #4243): paid factors +I + u y^T with u in R^n, y in K^n; free maps GL_n(K) anywhere in a word. +For every n x n matrix M over each listed K-algebra R this script computes + + cost(M) exact minimum number of paid factors, by breadth-first search + over words Q S (normal form of #4243), + delta(M) min over T in GL_n(K) of dim_K (M T - I) K^n, + +and records every target where cost != delta (cost >= delta is the +#4243 lower bound and is asserted). It also computes the minimum with no +free map (products of factors only) and compares it with dim_K (M - I) K^n, +recording every matrix where the two differ. Writes nothing. +""" +import hashlib +import itertools +import sys + +import numpy as np + + +def algebra(name): + """Return (p, r, basis_mul, one_coords) for a K-algebra with K = F_p.""" + if name == "F2": + return 2, 1, lambda i, j: {0: 1}, [1] + if name == "F3": + return 3, 1, lambda i, j: {0: 1}, [1] + if name == "F4": # F2[w]/(w^2+w+1) + return 2, 2, lambda i, j: {i + j: 1} if i + j < 2 else {0: 1, 1: 1}, [1, 0] + if name == "F2[C2]": + return 2, 2, lambda i, j: {(i + j) % 2: 1}, [1, 0] + if name == "F2xF2": + return 2, 2, lambda i, j: {i: 1} if i == j else {}, [1, 1] + if name == "F3xF3": + return 3, 2, lambda i, j: {i: 1} if i == j else {}, [1, 1] + if name == "F2[C3]": + return 2, 3, lambda i, j: {(i + j) % 3: 1}, [1, 0, 0] + if name == "F2[x]/(x^3)": + return 2, 3, lambda i, j: {i + j: 1} if i + j < 3 else {}, [1, 0, 0] + if name == "M2(F2)": # basis E_ab at index 2a+b, noncommutative + def mul(i, j): + a, b = divmod(i, 2) + c, d = divmod(j, 2) + return {2 * a + d: 1} if b == c else {} + return 2, 4, mul, [1, 0, 0, 1] + raise SystemExit("unknown algebra " + name) + + +class Ring: + def __init__(self, name): + p, r, basis_mul, one = algebra(name) + self.name, self.p, self.r, self.q = name, p, r, p ** r + q = self.q + self.mul = np.zeros((q, q), dtype=np.int64) + self.add = np.zeros((q, q), dtype=np.int64) + for a in range(q): + va = self.dec(a) + for b in range(q): + vb = self.dec(b) + out = [0] * r + for i in range(r): + for j in range(r): + for k, c in basis_mul(i, j).items(): + out[k] += va[i] * vb[j] * c + self.mul[a, b] = self.enc(out) + self.add[a, b] = self.enc([x + y for x, y in zip(va, vb)]) + self.neg = np.array([self.enc([-x for x in self.dec(a)]) for a in range(q)]) + self.one = self.enc(one) + self.scal = [self.enc([s * x for x in one]) for s in range(p)] + e = self.one + assert all(self.mul[e, a] == a == self.mul[a, e] for a in range(q)) + # associativity and K-centrality are checked, not assumed + m = self.mul + trip = m[m[:, :, None], np.arange(q)[None, None, :]] + trip2 = m[np.arange(q)[:, None, None], m[None, :, :]] + assert (trip == trip2).all(), "not associative" + for s in self.scal: + assert (m[s, :] == m[:, s]).all(), "K not central" + + def dec(self, x): + return [(x // self.p ** k) % self.p for k in range(self.r)] + + def enc(self, v): + return sum((v[k] % self.p) * self.p ** k for k in range(self.r)) + + +def rank_mod_p(V, p): + """Row rank over F_p of each matrix V[s] (shape S x rows x cols).""" + V = V.copy() % p + S, rows, cols = V.shape + rk = np.zeros(S, dtype=np.int64) + inv = np.array([pow(x, -1, p) if x else 0 for x in range(p)]) + ar = np.arange(rows) + for c in range(cols): + cand = (V[:, :, c] != 0) & (ar[None, :] >= rk[:, None]) + idx = np.nonzero(cand.any(1))[0] + if len(idx) == 0: + continue + piv = np.argmax(cand, 1)[idx] + top = rk[idx] + a = V[idx, piv].copy() + b = V[idx, top].copy() + V[idx, top] = a + V[idx, piv] = b + prow = V[idx, top] * inv[V[idx, top, c]][:, None] % p + V[idx, top] = prow + for rr in range(rows): + keep = rr != top + sel = idx[keep] + V[sel, rr] = (V[sel, rr] - V[sel, rr, c][:, None] * prow[keep]) % p + rk[idx] += 1 + return rk + + +def gl_n(p, n): + out = [] + for t in itertools.product(range(p), repeat=n * n): + M = np.array(t).reshape(n, n) + if rank_mod_p(M[None], p)[0] == n: + out.append(t) + return out + + +def run(name, n): + R = Ring(name) + p, r, q = R.p, R.r, R.q + N = n * n + size = q ** N + pw = q ** np.arange(N) + + def matmul(A, B): + C = np.zeros_like(A) + for i in range(n): + for j in range(n): + acc = np.zeros(A.shape[0], dtype=np.int64) + for k in range(n): + acc = R.add[acc, R.mul[A[:, i * n + k], B[:, k * n + j]]] + C[:, i * n + j] = acc + return C + + ident = np.array([[R.one if i == j else 0 for i in range(n) for j in range(n)]], dtype=np.int64) + GL = np.array([[R.scal[x] for x in t] for t in gl_n(p, n)], dtype=np.int64) + ys = [y for y in itertools.product(range(p), repeat=n) + if any(y) and y[next(i for i in range(n) if y[i])] == 1] + facs = [] + for u in itertools.product(range(q), repeat=n): + for y in ys: + facs.append([R.add[ident[0, i * n + j], R.mul[u[i], R.scal[y[j]]]] + for i in range(n) for j in range(n)]) + facs = np.unique(np.array(facs, dtype=np.int64), axis=0) + + def bfs(start): + level = np.full(size, -1, dtype=np.int64) + front = start + level[front @ pw] = 0 + L = 0 + while len(front): + L += 1 + new = [] + for F in facs: + P = matmul(np.broadcast_to(F, front.shape).copy(), front) + c = P @ pw + fresh = level[c] == -1 + if fresh.any(): + level[c[fresh]] = L + new.append(P[fresh]) + if not new: + break + front = np.unique(np.concatenate(new), axis=0) + return level + + allM = np.stack([(np.arange(size) // q ** k) % q for k in range(N)], axis=1) + + def image_dim(T): + D = R.add[matmul(allM, np.broadcast_to(T, allM.shape).copy()), R.neg[ident[0]][None, :]] + V = np.zeros((size, n, n * r), dtype=np.int64) + for j in range(n): + for i in range(n): + for k in range(r): + V[:, j, i * r + k] = (D[:, i * n + j] // p ** k) % p + return rank_mod_p(V, p) + + cost = bfs(GL) + delta = np.min(np.stack([image_dim(T) for T in GL]), axis=0) + assert (cost >= 0).all(), "unreachable target" + assert (cost >= delta).all(), "lower bound of #4243 violated" + fails = np.nonzero(cost != delta)[0] + bare = bfs(ident) + raw = image_dim(ident[0]) + assert (bare >= 0).all() + assert (bare >= raw).all(), "column bound violated" + gaps = np.nonzero(bare != raw)[0] + witnesses = [[R.dec(int(x)) for x in allM[g]] for g in gaps] + return { + "ring": name, "n": n, "targets": size, "factors": len(facs), "free_maps": len(GL), + "max_cost": int(cost.max()), + "cost_hist": np.bincount(cost).tolist(), + "formula_failures": len(fails), + "failure_pairs": sorted(set((int(cost[g]), int(delta[g])) for g in fails)), + "failure_examples": [[R.dec(int(x)) for x in allM[g]] for g in fails[:2]], + "no_free_map_gaps": len(gaps), + "gap_examples": witnesses[:2], + "gap_bare_cost": sorted(set(int(bare[g]) for g in gaps)), + "gap_raw_dim": sorted(set(int(raw[g]) for g in gaps)), + } + + +CASES = [("F2", 2), ("F3", 2), ("F2", 3), ("F4", 2), ("F2[C2]", 2), ("F2xF2", 2), + ("F3xF3", 2), ("F2[C3]", 2), ("F2[x]/(x^3)", 2), ("M2(F2)", 2), ("F2[C2]", 3)] +EXPECTED_GAPS = {("F2xF2", 2): 2, ("F2[C3]", 2): 6, ("M2(F2)", 2): 684} +LARGE = ("F2[C2]", 3) +EXPECTED_FAILURES = {("M2(F2)", 2): 72} + + +def m2_permutation_witness(): + """Independent check in M_4(F_2) = M_2(M_2(F_2)). + + The target [[E11, E01], [E10, E00]] is the 4x4 transposition of + coordinates 0 and 3. A factor is I + U (y^T kron I_2) with U a 4x2 + binary matrix and y in F_2^2; a free map is S kron I_2. Check that no + word with two factors reaches it, that one with three does, and that + T = I already gives image dimension 2. + """ + P = np.eye(4, dtype=np.int64)[[3, 1, 2, 0]] + I2 = np.eye(2, dtype=np.int64) + ys = [np.array(y) for y in ((1, 0), (0, 1), (1, 1))] + Us = [np.array(b, dtype=np.int64).reshape(4, 2) for b in itertools.product((0, 1), repeat=8)] + F = np.unique(np.array([(np.eye(4, dtype=np.int64) + U @ np.kron(y[None, :], I2)) % 2 + for U in Us for y in ys]), axis=0) + Ss = [np.kron(np.array(t).reshape(2, 2), I2) for t in gl_n(2, 2)] + pw = 2 ** np.arange(16) + two = (np.einsum("aij,bjk->abik", F, F) % 2).reshape(-1, 16) + two_codes = set(np.unique(two @ pw).tolist()) + hits2 = [S for S in Ss if int(((P @ S) % 2).reshape(16) @ pw) in two_codes] + assert not hits2, "two factors suffice" + three = set() + for A in F: + three.update(np.unique(((np.einsum("ij,bjk->bik", A, two.reshape(-1, 4, 4))) % 2).reshape(-1, 16) @ pw).tolist()) + assert any(int(((P @ S) % 2).reshape(16) @ pw) in three for S in Ss), "three factors fail" + # image of x -> (P - I)(x kron I_2): span of the two 4x2 blocks, rank 2 + cols = np.stack([((P - np.eye(4, dtype=np.int64)) @ np.kron(e[:, None], I2) % 2).reshape(8) + for e in (np.array([1, 0]), np.array([0, 1]))]) + assert rank_mod_p(cols[None], 2)[0] == 2 + return len(F) + + +def main(): + stage = sys.argv[sys.argv.index("--stage") + 1] if "--stage" in sys.argv else "main" + assert stage in ("main", "large"), stage + cases = [c for c in CASES if (c == LARGE) == (stage == "large")] + with open(__file__, "rb") as fh: + digest = hashlib.sha256(fh.read()) + digest.update(stage.encode()) + parts = [] + for name, n in cases: + res = run(name, n) + print(res, flush=True) + assert res["formula_failures"] == EXPECTED_FAILURES.get((name, n), 0), (name, n) + if res["formula_failures"]: + assert res["failure_pairs"] == [(3, 2)] + want = EXPECTED_GAPS.get((name, n), 0) + assert res["no_free_map_gaps"] == want, (name, n, res["no_free_map_gaps"]) + if want and name != "M2(F2)": + assert res["gap_bare_cost"] == [3] and res["gap_raw_dim"] == [2] + digest.update(repr(res).encode()) + parts.append(f"{name}:n{n}:{res['targets']}") + if stage == "large": + print("receipt", digest.hexdigest()) + print("PASS_RIGHT_VECTOR_GENERAL_TARGET_LARGE", " ".join(parts), + "formula_failures=0 no_free_map_gaps=0 no_new_kappa") + return 0 + nf = m2_permutation_witness() + print("independent M_4(F_2) check: transposition (0 3) needs 3 factors, formula 2;", nf, "factors") + digest.update(str(nf).encode()) + print("receipt", digest.hexdigest()) + print("PASS_RIGHT_VECTOR_GENERAL_TARGET", " ".join(parts), + "formula_failures=M2(F2):72 no_free_map_gaps=F2xF2:2,F2[C3]:6,M2(F2):684 no_new_kappa") + return 0 + + +if __name__ == "__main__": + sys.exit(main())