diff --git a/research/right-vector-diagonal-free-basis/PROOF.md b/research/right-vector-diagonal-free-basis/PROOF.md new file mode 100644 index 0000000000..0964deb343 --- /dev/null +++ b/research/right-vector-diagonal-free-basis/PROOF.md @@ -0,0 +1,127 @@ +# Free basis changes do not shorten a right-vector diagonal + +## Model + +Let `K` be a field and `R` an associative unital `K`-algebra with `K` central. +`R` need not be commutative, finite or local. Fix a register count `n >= 0`. +A paid factor is + +```text +F = I + u y^T, u in R^n, y in K^n. +``` + +A free map is any `S` in `GL_n(K)`. A word is + +```text +W = S_0 F_1 S_1 F_2 S_2 ... F_L S_L, +``` + +with `L` paid factors and free maps anywhere, including at both ends. Its +target is `diag(d_1, ..., d_n)` with `d_i` in `R`. Put + +```text +t_K(d) = #{ i : d_i is not in K^x }. +``` + +For `K = F_2` the unit group is `{1}`, so `t_K(d)` is the count `t` of entries +different from 1 used by `research/f2-right-vector-diagonal-minimum`. + +**Theorem.** The minimum number of paid factors in a word equal to +`diag(d)` is exactly `t_K(d)`, for every `n` and every `d` in `R^n`. + +This answers that package's first open question: free `GL_n(F_2)` changes of +basis between paid factors never realize a diagonal with fewer than `t` factors. + +## Normal form + +Put `A_j = S_0 S_1 ... S_{j-1}` and `S = S_0 S_1 ... S_L`. Then + +```text +W = F'_1 F'_2 ... F'_L S, F'_j = A_j F_j A_j^{-1}. +``` + +Since `A_j` has entries in `K`, + +```text +F'_j = I + (A_j u_j) (A_j^{-T} y_j)^T, +``` + +and `A_j^{-T} y_j` lies in `K^n`. So each `F'_j` is again a paid factor. +Conversely every product `F'_1 ... F'_L S` is a word. Thus the reachable +endpoints of length `L` are exactly `Q S`, with `Q` a product of `L` paid +factors and `S` in `GL_n(K)`. + +## Column bound + +Let `Q = F'_1 ... F'_L` and `Q_j = F'_1 ... F'_j`, `Q_0 = I`. Telescoping, + +```text +Q - I = sum_j Q_{j-1} (F'_j - I) = sum_j c_j y'_j^T, c_j = Q_{j-1} u'_j in R^n, +``` + +where `y'_j` lies in `K^n`. For `w` in `K^n`, `(Q - I) w = sum_j (y'_j . w) c_j` +is a `K`-combination of the `L` fixed vectors `c_j`. The `K`-linear map +`w -> (Q - I) w` from `K^n` to `R^n` therefore has image of `K`-dimension at +most `L`. This is the column argument of `research/f2-right-vector-diagonal-minimum`, +written for an arbitrary field. Note the right-hand factor `y'^T` multiplies +`w` before `c_j`; `K` central makes `(y' . w) c_j = c_j (y' . w)`. + +## Kernel lemma + +Suppose `W = D = diag(d)`. Then `Q = D T` with `T = S^{-1}` in `GL_n(K)`. +Let `w` in `K^n` satisfy `(D T - I) w = 0`, that is, + +```text +d_i (T w)_i = w_i for every i. +``` + +Both `(T w)_i` and `w_i` lie in `K`. Fix `i` with `d_i` not in `K^x`. + +* If `(T w)_i != 0`, then `d_i = w_i (T w)_i^{-1}` lies in `K`. Since `d_i` + is not in `K^x`, `d_i = 0`, and then `w_i = d_i (T w)_i = 0`. +* If `(T w)_i = 0`, the equation gives `w_i = 0`. + +So the kernel lies in the coordinate subspace `{ w : w_i = 0 for d_i not in K^x }`, +whose dimension is `n - t_K(d)`. Rank-nullity over `K` gives + +```text +dim_K (D T - I) K^n >= t_K(d). +``` + +## Lower bound + +Combining the two displays, `t_K(d) <= dim_K (Q - I) K^n <= L`. + +## Matching construction + +Let `E = diag(e)` with `e_i = d_i` when `d_i` is in `K^x` and `e_i = 1` +otherwise. `E` is a free map. For each `i` with `d_i` not in `K^x`, the factor +`I + (d_i - 1) e_i e_i^T` is paid: its right vector `e_i` is in `K^n`. +Increments on distinct matrix units multiply to zero, so the product of these +`t_K(d)` factors is `diag(f)` with `f_i = d_i` off `K^x` and `f_i = 1` on it. +Then `diag(f) E = diag(d)`. The word has `t_K(d)` paid factors. + +## Corollaries and boundaries + +* `K = F_2`, any `F_2`-algebra: the exact minimum is `t`, with or without free + `GL_n(F_2)` maps. This includes every group algebra `F_2[G]` and the narrower + legal alphabet `I + (g - 1) x y^T` with binary `x, y`, `y^T x = 1`, of the + `elementary-abelian-diagonal-minimum` and Q8 lineages. Free scalar mixing + does not lower the diagonal count in the full nonidentity-label alphabet. + Restricted label sets (for example only `{i, j}` in `F_2[Q8]`) can force + more factors; that is outside this statement. +* Over a larger field, free maps absorb scalar diagonal entries. Over `F_3`, + `diag(2, 2)` is itself a free map and costs no factor. +* The `K`-valued right vector is necessary. In `F_2[z_1, z_2]/(z_1^2, z_2^2)` + the single factor `I + (z_1, z_2)^T (z_2, z_1)` equals + `diag(1 + z_1 z_2, 1 + z_1 z_2)`, so `t = 2` drops to one factor + (the witness of `research/f2-right-vector-diagonal-minimum`). +* Free maps must have entries in `K`. The kernel lemma uses that `T w` is + `K`-valued; with `R`-valued free maps the statement is not asserted. + +No native frame, hosting, routing, precision or recursive cost is priced. The +selected multiplication exponent is unchanged. + +Produced by Nick Petalas. The column expansion, the right-vector alphabet and +the sharpness witness are Wentao Li's `research/f2-right-vector-diagonal-minimum`. +Apache-2.0. diff --git a/research/right-vector-diagonal-free-basis/README.md b/research/right-vector-diagonal-free-basis/README.md new file mode 100644 index 0000000000..50a1cbeea5 --- /dev/null +++ b/research/right-vector-diagonal-free-basis/README.md @@ -0,0 +1,113 @@ +# Free basis changes do not shorten a right-vector diagonal + +**Scoped proof, with finite controls. No new κ.** Selected κ stays +`0.001672660197076918`. + +Factors are `I + u y^T` with `u` in `R^n` and `y` in `K^n`, over any field `K` +and any associative `K`-algebra `R`. Free maps are arbitrary `GL_n(K)` changes +of basis, placed anywhere in the word. The exact number of factors needed for +`diag(d_1, ..., d_n)` is + +```text +t_K(d) = #{ i : d_i is not in K^x }. +``` + +For `K = F_2` this is the count `t` of entries different from 1. So free +`GL_n(F_2)` mixing never realizes a diagonal with fewer than `t` factors. That +answers open question 1 of +[`research/f2-right-vector-diagonal-minimum`](../f2-right-vector-diagonal-minimum/README.md), +which proved the count without free maps and named the missing invariant as +the blocker. + +## Argument + +The written proof is [PROOF.md](PROOF.md). It has three steps: + +1. **Normal form.** Conjugating a factor by a free map gives a factor, so every + word equals `Q S` with `Q` a product of the same number of factors and `S` + one free map. +2. **Column bound** (from the predecessor). `Q - I` maps `K^n` onto a + `K`-space spanned by `L` vectors. +3. **Kernel lemma** (new). For a diagonal `D` and any `T` in `GL_n(K)`, every + kernel vector of `D T - I` on `K^n` vanishes at each `i` with `d_i` not in + `K^x`. So the image of `D T - I` has dimension at least `t_K(d)`. Apply it + with `Q = D S^{-1}`. + +The coordinate factors, followed by one free diagonal map for the entries in +`K^x`, attain the bound. + +Corollaries: every group algebra `F_2[G]`, abelian or not, has exact diagonal +minimum `t` in the full nonidentity-label alphabet `I + (g - 1) x y^T`, with +free scalar mixing allowed. Over `F_3`, `diag(2, 2)` costs nothing, because it +is a free map. Restricted label alphabets, such as `{i, j}` only in `F_2[Q8]`, +can need more factors. They are outside this statement. + +## Finite controls + +`verify.py` uses the standard library and writes nothing. It checks: + +| Ring | n | Word length | Factors | Free maps | Diagonals reached, each first at length `t_K` | +|---|---:|---:|---:|---:|---:| +| `F_2[C_2 x C_2]` | 2 | ≤ 2 | 766 | 6 | 256 of 256 | +| `F_2[S_3]` (nonabelian) | 2 | ≤ 1 | 12,286 | 6 | 127 (all with `t ≤ 1`) | +| `F_3[x]/(x^2)` | 2 | ≤ 1 | 321 | 48 | 32 (all with `t_K ≤ 1`) | + +It also checks: + +- Every conjugate of every factor stays in the alphabet: 93,720 checks. +- The kernel lemma for every diagonal and every free map: 718,128 cases over + the three rings at `n = 2` and the Klein ring at `n = 3`. +- Over `F_3`, `diag(2, 2)` is reached at length 0. +- Sharpness of the `K`-valued right vector: the predecessor's ring-valued factor + is outside the alphabet and gives `t = 2` from one factor. + +These are corroboration, not the proof. + +## Reproduce + +From the repository root: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/right-vector-diagonal-free-basis/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/right-vector-diagonal-free-basis/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/right-vector-diagonal-free-basis +``` + +Expected final line of `verify.py`: + +```text +PASS_RIGHT_VECTOR_DIAGONAL_FREE_BASIS F2[C2xC2]:n2:L2=256 F2[S3]:n2:L1=127 F3[x]/(x^2):n2:L1=32 no_new_kappa +``` + +Each run takes about 20 seconds. The script prints a receipt digest bound to +its own bytes and to the declared input. + +## 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. +Free maps must have entries in `K`. With `R`-valued free maps the statement is +not asserted. Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +1. **General targets.** For a non-diagonal target `M`, is the minimum + `min_T dim_K (M T - I) K^n` over `T` in `GL_n(K)`? The lower bound follows + from the same normal form. The upper bound needs a factorization + `I + C Y^T` into factors whose prefixes stay invertible. A first step is a + permutation target over `F_2[C_2]` at `n = 2`. +2. **Restricted labels with free mixing.** Which part of the Q8 `{i, j}` lower + bounds survives when the alphabet adds one paid label outside `{i, j}`? + This package shows that the full label set gives `t`. Start with a single + `[zi]` target. +3. **Native price.** Bind one coordinate word to an existing supplier meter. + This note has no physical schedule. + +## Credit + +Produced by Nick Petalas. The right-vector alphabet, the column expansion and +the ring-valued sharpness witness are Wentao Li's +`research/f2-right-vector-diagonal-minimum` (#4099), which builds on +`research/bit-cyclic-root-barrier` (#2513). The graded diagonal argument for +elementary abelian groups is `research/elementary-abelian-diagonal-minimum` +(#4098). Apache-2.0. diff --git a/research/right-vector-diagonal-free-basis/SOURCES.json b/research/right-vector-diagonal-free-basis/SOURCES.json new file mode 100644 index 0000000000..86e1910e4f --- /dev/null +++ b/research/right-vector-diagonal-free-basis/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-diagonal-free-basis/TASK.json b/research/right-vector-diagonal-free-basis/TASK.json new file mode 100644 index 0000000000..2731dc4065 --- /dev/null +++ b/research/right-vector-diagonal-free-basis/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 diagonal minimum for factors I + u y^T (u in R^n, y in K^n) over any K-algebra R when free GL_n(K) maps may appear anywhere in the word: t_K(d), the number of entries outside K^x. Answers open question 1 of research/f2-right-vector-diagonal-minimum.", + "scope_change_reason": "The card asks whether a larger or nonabelian register model escapes the scoped three-register obstruction. This package settles a narrower open question left by research/f2-right-vector-diagonal-minimum: whether free scalar basis changes lower the right-vector diagonal count. The answer covers every group algebra F2[G] in the full nonidentity-label alphabet, so no nonabelian group gives a shorter diagonal there.", + "bottleneck_link": "A legal diagonal shorter than t would be a new bit primitive. Free scalar mixing does not supply one in this alphabet; this is a side result and kappa is unchanged.", + "budget_minutes": 60, + "stop_rule": "Prove the normal form, the kernel lemma and the matching construction; corroborate on three small rings (one nonabelian, one over F3) with exhaustive free-map searches; then stop.", + "outcome": "completed", + "evidence": "PROOF.md is the argument. verify.py exhausts words of length at most 2 over F2[C2xC2] and at most 1 over F2[S3] and F3[x]/(x^2) at n=2, with every free map, checks every conjugate stays in the alphabet (93720 checks), checks the kernel lemma in 718128 cases, and checks the ring-valued sharpness witness.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "For a non-diagonal target M, is the minimum min over T in GL_n(K) of dim_K (M T - I) K^n?", + "why_it_matters": "It would give the exact cost of every target in this alphabet, not only diagonals.", + "first_step": "Test a permutation target over F2[C2] at n=2 against an exhaustive word search.", + "blocked_by": "The upper bound needs a factorization of I + C Y^T whose prefixes stay invertible; none is proved here." + }, + { + "question": "Which restricted label sets keep a count above t once free scalar mixing is allowed?", + "why_it_matters": "The Q8 {i,j} lower bounds use restricted labels; this package shows the full label set gives exactly t.", + "first_step": "Add one paid label outside {i,j} in F2[Q8] and recompute the single [zi] target.", + "blocked_by": "Nothing for the formal statement; native conversion remains unpriced." + }, + { + "question": "What native frame, hosting and precision bill does one coordinate word pay?", + "why_it_matters": "An exact formal call count is not a supplier invoice.", + "first_step": "Price one coordinate word on an existing supplier meter.", + "blocked_by": "No physical schedule is supplied here." + } + ] +} diff --git a/research/right-vector-diagonal-free-basis/VERIFY.json b/research/right-vector-diagonal-free-basis/VERIFY.json new file mode 100644 index 0000000000..1c20e478cf --- /dev/null +++ b/research/right-vector-diagonal-free-basis/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/f2-right-vector-diagonal-minimum/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Exhaustive free-map word searches on three rings, normal-form closure, kernel lemma, sharpness witness; read-only." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 240, + "checks": "Same checks under -O; admission uses need(), not assert." + } + ] +} diff --git a/research/right-vector-diagonal-free-basis/verify.py b/research/right-vector-diagonal-free-basis/verify.py new file mode 100644 index 0000000000..9ac56e4874 --- /dev/null +++ b/research/right-vector-diagonal-free-basis/verify.py @@ -0,0 +1,337 @@ +#!/usr/bin/env python3 +"""Finite controls for the free-basis-change diagonal minimum. + +PROOF.md is the argument. This script checks its finite consequences on small +rings, with free invertible scalar maps placed anywhere in the word: + +* Klein ring F2[C2 x C2], n = 2: every word S0 F1 S1 F2 S2 with at most two + factors I + u y^T (u in R^2, y in F2^2). Each diagonal endpoint is reached + first at length t(d), and every diagonal with t(d) <= 2 is reached. +* F2[S3] (nonabelian), n = 2: every word with at most one factor. +* F3[x]/(x^2), n = 2: every word with at most one factor and free GL2(F3) + maps. The first length is the number of entries outside F3^x. +* The kernel lemma: dim_K (D T - I) K^n >= t_K(D) for every diagonal D and + every T in GL_n(K), over the three rings at n = 2 and the Klein ring at n = 3. +* The normal form: conjugating a factor by a free map gives a factor. + +Standard library only. Read-only. Prints a receipt digest bound to this file +and to the declared input. +""" + +from __future__ import annotations + +import hashlib +import itertools +import json +import sys +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent +INPUT = ROOT / "research/f2-right-vector-diagonal-minimum/PROOF.md" + + +def need(cond: bool, msg: str) -> None: + """Fail closed; unlike assert, this survives python -O.""" + if not cond: + raise SystemExit(f"FAIL: {msg}") + + +class Ring: + """A finite K-algebra given by element tables. Elements are ints 0..size-1.""" + + def __init__(self, name, size, add, mul, one, zero, scalars, units): + self.name = name + self.size = size + self.add = add # add[a][b] + self.mul = mul # mul[a][b] + self.one = one + self.zero = zero + self.scalars = scalars # embedded field K, as ring elements, index = field value + self.units = units # embedded K^x + self.neg = [next(b for b in range(size) if add[a][b] == zero) for a in range(size)] + + def sub(self, a, b): + return self.add[a][self.neg[b]] + + +def klein_ring() -> Ring: + # F2[C2 x C2]: group elements g = (a,b) in F2^2 index 0..3; ring element = 4-bit mask. + def gmul(g, h): + return g ^ h + + add = [[a ^ b for b in range(16)] for a in range(16)] + mul = [[0] * 16 for _ in range(16)] + for a in range(16): + for b in range(16): + r = 0 + for g in range(4): + if a >> g & 1: + for h in range(4): + if b >> h & 1: + r ^= 1 << gmul(g, h) + mul[a][b] = r + return Ring("F2[C2xC2]", 16, add, mul, one=1, zero=0, scalars=[0, 1], units=[1]) + + +def s3_ring() -> Ring: + perms = list(itertools.permutations(range(3))) + index = {p: i for i, p in enumerate(perms)} + ident = index[(0, 1, 2)] + + def gmul(g, h): + p, q = perms[g], perms[h] + return index[tuple(p[q[k]] for k in range(3))] + + size = 1 << 6 + add = [[a ^ b for b in range(size)] for a in range(size)] + mul = [[0] * size for _ in range(size)] + for a in range(size): + for b in range(size): + r = 0 + for g in range(6): + if a >> g & 1: + for h in range(6): + if b >> h & 1: + r ^= 1 << gmul(g, h) + mul[a][b] = r + one = 1 << ident + return Ring("F2[S3]", size, add, mul, one=one, zero=0, scalars=[0, one], units=[one]) + + +def dual_f3_ring() -> Ring: + # F3[x]/(x^2): element a + b x encoded as a + 3 b. + def dec(e): + return e % 3, e // 3 + + def enc(a, b): + return (a % 3) + 3 * (b % 3) + + add = [[0] * 9 for _ in range(9)] + mul = [[0] * 9 for _ in range(9)] + for e in range(9): + a, b = dec(e) + for f in range(9): + c, d = dec(f) + add[e][f] = enc(a + c, b + d) + mul[e][f] = enc(a * c, a * d + b * c) + return Ring("F3[x]/(x^2)", 9, add, mul, one=1, zero=0, scalars=[0, 1, 2], units=[1, 2]) + + +# --------------------------------------------------------------------------- +# n x n matrices over a Ring, stored as flat tuples in row-major order. + + +def mat_mul(R: Ring, A, B, n): + out = [] + for i in range(n): + for j in range(n): + acc = R.zero + for k in range(n): + acc = R.add[acc][R.mul[A[i * n + k]][B[k * n + j]]] + out.append(acc) + return tuple(out) + + +def identity(R: Ring, n): + return tuple(R.one if i == j else R.zero for i in range(n) for j in range(n)) + + +def is_diagonal(R: Ring, M, n): + return all(M[i * n + j] == R.zero for i in range(n) for j in range(n) if i != j) + + +def t_count(R: Ring, M, n): + """Number of diagonal entries outside the embedded unit group K^x.""" + return sum(1 for i in range(n) if M[i * n + i] not in R.units) + + +def scalar_gl(R: Ring, n): + """All invertible n x n matrices with entries in the embedded field K.""" + ident = identity(R, n) + mats = list(itertools.product(R.scalars, repeat=n * n)) + out = [] + for A in mats: + for B in mats: + if mat_mul(R, A, B, n) == ident: + out.append(A) + break + return out + + +def factors(R: Ring, n): + """All matrices I + u y^T with u in R^n and y in K^n, y nonzero.""" + ident = identity(R, n) + out = set() + for u in itertools.product(range(R.size), repeat=n): + for y in itertools.product(R.scalars, repeat=n): + if all(c == R.zero for c in y): + continue + M = list(ident) + for i in range(n): + for j in range(n): + M[i * n + j] = R.add[M[i * n + j]][R.mul[u[i]][y[j]]] + out.add(tuple(M)) + return out + + +def inverse_in(R, S, group, n): + ident = identity(R, n) + return next(T for T in group if mat_mul(R, S, T, n) == ident) + + +def check_normal_form(R: Ring, n, facs, group): + """S F S^{-1} is again a factor for every free map S and factor F.""" + for S in group: + Si = inverse_in(R, S, group, n) + for F in facs: + need(mat_mul(R, mat_mul(R, S, F, n), Si, n) in facs, f"{R.name}: conjugate left the alphabet") + return len(group) * len(facs) + + +def first_lengths(R: Ring, n, max_len, facs, group): + """Map each diagonal endpoint of a word S0 F1 S1 ... FL SL (L <= max_len) + to its first length L. + + By the normal form every such word equals F'1 ... F'L S with factors F' + and one free map S, and conversely. The search uses that form; the + normal-form premise is checked separately by check_normal_form. + """ + first = {} + layer = {identity(R, n)} + seen = set(layer) + for length in range(max_len + 1): + for Q in layer: + for S in group: + P = mat_mul(R, Q, S, n) + if is_diagonal(R, P, n) and P not in first: + first[P] = length + if length == max_len: + break + nxt = set() + for Q in layer: + for F in facs: + P = mat_mul(R, Q, F, n) + if P not in seen: + nxt.add(P) + seen |= nxt + layer = nxt + return first + + +def check_first_lengths(R: Ring, n, max_len): + facs = factors(R, n) + group = scalar_gl(R, n) + conj = check_normal_form(R, n, facs, group) + first = first_lengths(R, n, max_len, facs, group) + for P, length in first.items(): + need(length >= t_count(R, P, n), f"{R.name}: diagonal below its count at length {length}") + need(length == t_count(R, P, n), f"{R.name}: first length differs from t_K") + diagonals = 0 + for entries in itertools.product(range(R.size), repeat=n): + D = tuple(entries[i] if i == j else R.zero for i in range(n) for j in range(n)) + if t_count(R, D, n) <= max_len: + diagonals += 1 + need(D in first, f"{R.name}: diagonal with t <= {max_len} not reached") + return { + "ring": R.name, + "n": n, + "max_factors": max_len, + "factor_alphabet": len(facs), + "free_maps": len(group), + "conjugations_checked": conj, + "diagonals_reached": len(first), + "diagonals_with_t_le_max": diagonals, + } + + +def kernel_lemma(R: Ring, n): + """dim_K of the image of w -> (D T - I) w on K^n is at least t_K(D).""" + group = scalar_gl(R, n) + ident = identity(R, n) + vectors = list(itertools.product(R.scalars, repeat=n)) + q = len(R.scalars) + cases = 0 + tight = 0 + for entries in itertools.product(range(R.size), repeat=n): + D = tuple(entries[i] if i == j else R.zero for i in range(n) for j in range(n)) + t = t_count(R, D, n) + for T in group: + M = mat_mul(R, D, T, n) + M = tuple(R.sub(M[k], ident[k]) for k in range(n * n)) + image = set() + for w in vectors: + image.add(tuple( + _row_dot(R, M, w, i, n) for i in range(n) + )) + # The image is a K-subspace; its size is q^dim. + dim = 0 + while q ** dim < len(image): + dim += 1 + need(q ** dim == len(image), f"{R.name}: image is not a K-subspace") + need(dim >= t, f"{R.name}: kernel lemma fails") + cases += 1 + tight += dim == t + return {"ring": R.name, "n": n, "cases": cases, "tight_cases": tight} + + +def _row_dot(R, M, w, i, n): + acc = R.zero + for k in range(n): + acc = R.add[acc][R.mul[M[i * n + k]][w[k]]] + return acc + + +def sha256(path: Path) -> str: + return hashlib.sha256(path.read_bytes()).hexdigest() + + +def main() -> int: + need(INPUT.is_file(), f"missing declared input {INPUT}") + klein, s3, dual = klein_ring(), s3_ring(), dual_f3_ring() + + # Sanity: S3 ring is nonabelian, the dual-number ring has K = F3. + need(any(s3.mul[a][b] != s3.mul[b][a] for a in range(64) for b in range(64)), "F2[S3] commutes") + + searches = [ + check_first_lengths(klein, 2, 2), + check_first_lengths(s3, 2, 1), + check_first_lengths(dual, 2, 1), + ] + lemmas = [kernel_lemma(klein, 2), kernel_lemma(s3, 2), kernel_lemma(dual, 2), kernel_lemma(klein, 3)] + + # Free maps can absorb entries in K^x: over F3, diag(2,2) needs no factor. + dual_first = first_lengths(dual, 2, 0, factors(dual, 2), scalar_gl(dual, 2)) + need(dual_first.get((2, 0, 0, 2)) == 0, "F3: diag(2,2) should be free") + + # Sharpness control (#4099's witness): an R-valued right vector breaks the + # count. With u = (z1, z2) and y = (z2, z1), one factor is diag(1+z1z2, 1+z1z2). + z1, z2 = 0b0011, 0b0101 + witness = tuple( + klein.add[klein.one if i == j else 0][klein.mul[(z1, z2)[i]][(z2, z1)[j]]] + for i in range(2) for j in range(2) + ) + need(is_diagonal(klein, witness, 2) and t_count(klein, witness, 2) == 2, "witness control") + need(witness not in factors(klein, 2), "witness must lie outside the K-valued alphabet") + + result = {"searches": searches, "kernel_lemma": lemmas} + blob = json.dumps(result, sort_keys=True).encode() + receipt = hashlib.sha256( + blob + sha256(Path(__file__)).encode() + sha256(INPUT).encode() + ).hexdigest() + for row in searches: + print(json.dumps(row, sort_keys=True)) + for row in lemmas: + print(json.dumps(row, sort_keys=True)) + print(f"input_sha256={sha256(INPUT)}") + print(f"receipt_sha256={receipt}") + print( + "PASS_RIGHT_VECTOR_DIAGONAL_FREE_BASIS " + + " ".join(f"{r['ring']}:n{r['n']}:L{r['max_factors']}={r['diagonals_reached']}" for r in searches) + + " no_new_kappa" + ) + return 0 + + +if __name__ == "__main__": + sys.exit(main())