diff --git a/research/right-vector-two-factor-criterion/PROOF.md b/research/right-vector-two-factor-criterion/PROOF.md new file mode 100644 index 0000000000..71888afa0d --- /dev/null +++ b/research/right-vector-two-factor-criterion/PROOF.md @@ -0,0 +1,93 @@ +# Proofs + +`K` is a field and `R` an associative unital `K`-algebra with `K` central. A +paid factor is `P(u, y) = I + u y^T` with `u` in `R^n` and `y` in `K^n`; a free +map is any `S` in `GL_n(K)`, used anywhere in a word. `cost(M)` is the least +number of paid factors in a word equal to `M` (infinite if none exists), and + +```text +delta(M) = min over T in GL_n(K) of dim_K (M T - I) K^n. +``` + +Facts used from #4243 and #4099: `cost(M) >= delta(M)`, and every word can be +rewritten as `Q S` with `Q` a product of the same number of paid factors, +because `S P(u, y) S^{-1} = P(S u, S^{-T} y)`. + +## Lemma 1 (merging) + +`P(u, y) P(v, c y) = P(u + c v + c u (y^T v), y)` for `c` in `K`. Expand: +`(I + u y^T)(I + c v y^T) = I + u y^T + c v y^T + c u (y^T v) y^T`, and +`y^T v` is an element of `R`. Also `P(u, 0) = P(0, y) = I`. + +## Theorem A (one factor, every n, every R) + +`cost(M) <= 1` if and only if `delta(M) <= 1`, and then `cost(M) = delta(M)`. + +*Proof.* `cost >= delta` gives one direction. If `delta(M) = 0`, then +`M T = I` and `M = T^{-1}` costs 0. If `delta(M) = 1`, then +`(M T - I) K^n = K w` for some `w` in `R^n`, so `(M T - I) e_j = c_j w` with +`c` in `K^n`, that is `M T = I + w c^T = P(w, c)`, and `M = P(w, c) T^{-1}`. + +## Theorem B (two factors, n = 2, every R) + +`cost(M) <= 2` if and only if some `G, H` in `GL_2(K)` give `N = G M H` with +`N12` in the right ideal `N11 R`. + +*Proof.* (If.) Write `N12 = N11 C` and put `A = N11`, `B = N21`, +`D = N22 - N21 C`. Then + +```text +F1 = P((A - 1, B), e1) = [[A, 0], [B, 1]], +F2 = P((C, D - 1), e2) = [[1, C], [0, D]], +F1 F2 = [[A, A C], [B, B C + D]] = N, +``` + +so `M = (G^{-1} F1 G)(G^{-1} F2 G) G^{-1} H^{-1}`, and each conjugate is a +paid factor. + +(Only if.) Write `M = P(u1, y1) P(u2, y2) S`, padding with `P(0, y) = I`. If +`y1, y2` are dependent, Lemma 1 merges the two factors into one with a nonzero +`y` (or both are `I`); replace the second by `P(0, y2')` with `y2'` +independent. So `y1, y2` is a basis. Choose `G` with `G^{-T} y_i = e_i`. Then +`G M S^{-1} G^{-1} = P(u1', e1) P(u2', e2)`, which is +`[[A, 0], [B, 1]] [[1, C], [0, D]] = [[A, A C], [B, B C + D]]` for some +`A, B, C, D` in `R`. Its `(1, 2)` entry is `A C`, in `A R`. Take +`H = S^{-1} G^{-1}`. + +## Corollary C (matrix algebras) + +Let `R = M_m(K)` and view `M` as a `2m x 2m` matrix. Then `cost(M) <= 2` if +and only if there are nonzero `phi` in `(K^2)^*` and `t` in `K^2` with + +```text +rank (phi ⊗ I_m) M = rank (phi ⊗ I_m) M (t ⊗ I_m). +``` + +*Proof.* In `M_m(K)`, `Z` lies in `A M_m(K)` exactly when the column space of +`Z` lies in that of `A`. Let `phi` be the first row of `G` and `t, s` the +columns of `H`. Then `N11 = (phi ⊗ I) M (t ⊗ I)`, +`N12 = (phi ⊗ I) M (s ⊗ I)`, and since `H` is invertible the column space of +`[N11 N12]` is that of `(phi ⊗ I) M`. So `col N12 ⊆ col N11` is the stated +rank equality. Every nonzero `phi` is a first row and every nonzero `t` a first +column. + +## Theorem D (local algebras, n = 2) + +Let the non-units of `R` form an ideal `J`. Every target `M` with an entry +outside `J` (in particular every invertible `M`) has `cost(M) = delta(M)`. + +*Proof.* Permutation matrices `G, H` move a unit to position `(1, 1)`. Then +`N11 R = R`, so Theorem B gives `cost(M) <= 2`. If `delta(M) <= 1`, Theorem A +gives equality. Otherwise `2 = delta(M) <= cost(M) <= 2`. + +## Corollary E (quotients and F2[S3]) + +If `rho: R -> R'` is a unital `K`-algebra homomorphism, then +`cost_R(M) >= cost_R'(rho(M))`, because `rho` maps paid factors to paid factors +and free maps to free maps. Since `delta(M) <= n` always, every target over +`F2[S3]` whose image under the surjection `rho: F2[S3] -> M_2(F_2)` is one of +the 72 cost-3 targets of #4265 costs at least 3 while `delta <= 2`. `rho` +extends the isomorphism `S3 = GL_2(F_2)` given by the action on the three +nonzero vectors of `F_2^2`; `verify.py` checks that it is a surjective unital +algebra map and lifts a three-factor word to an explicit target of cost +exactly 3. diff --git a/research/right-vector-two-factor-criterion/README.md b/research/right-vector-two-factor-criterion/README.md new file mode 100644 index 0000000000..8952fc9ae8 --- /dev/null +++ b/research/right-vector-two-factor-criterion/README.md @@ -0,0 +1,124 @@ +# Exact two-factor criterion for right-vector targets + +**Scoped proofs with finite certificates. 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 (#4099, #4243). #4243 proved +`cost(M) >= delta(M) = min_T dim_K (M T - I) K^n` and equality on diagonal +targets. #4265 showed equality fails over `M2(F2)` at `n = 2` (72 targets cost +3 against `delta = 2`) and asked what the exact cost is over noncommutative +algebras, whether the failure lifts to `F2[S3]`, and whether `delta` is exact +over commutative or local algebras. + +## Result + +Proofs are in [PROOF.md](PROOF.md). + +1. **One factor, every `n` and every algebra:** `cost(M) <= 1` exactly when + `delta(M) <= 1`, and then the two are equal. +2. **Two factors at `n = 2`, every algebra:** `cost(M) <= 2` exactly when some + `G, H` in `GL_2(K)` give `N = G M H` with `N12` in the right ideal `N11 R`. + With item 1, this decides `cost(M)` in {0, 1, 2, ≥3} for every target. +3. **Matrix algebras.** Over `R = M_m(K)` the condition reads: some nonzero + `phi`, `t` in `K^2` give + `rank (phi ⊗ I_m) M = rank (phi ⊗ I_m) M (t ⊗ I_m)`. This answers #4265's + question 3 at `n = 2`. +4. **Local algebras.** If the non-units of `R` form an ideal `J`, every target + with an entry outside `J`, in particular every invertible target, costs + exactly `delta(M)`. This answers #4265's question 1 at `n = 2` for local + algebras and invertible targets. It cannot be extended to every target: + over the commutative local algebra `F2[x,y]/(x,y)^2`, 12 targets in + `M_2(J)` are unreachable while `delta <= 2`, for example + `[[x + y, y], [y, x]]`. +5. **`F2[S3]`.** The failure lifts. A unital surjection + `F2[S3] -> M_2(F_2)` maps words to words, so every lift of a #4265 + failure costs at least 3 while `delta <= 2`. `verify.py` builds one target + of cost exactly 3. Over all `2^24` targets at `n = 2`, exactly **120,060** + fail the criterion, so they cost at least 3 against `delta <= 2`. Of these, + 18,432 = 72 · 4^4 are lifts of `M2(F2)` failures. The rest fail because one + pair `(G, H)` must work in both blocks. +6. **A smaller noncommutative failure.** Over the 3-dimensional algebra + `UT2(F2)` of upper triangular matrices, 12 of 4,096 targets cost 3 with + `delta = 2`. + +| Algebra `R` | Targets (n = 2) | Cost histogram 0/1/2/3 | Unreachable | Criterion failures | +|---|---:|---|---:|---:| +| `F2[x,y]/(x,y)^2` (local) | 4,096 | 6 / 549 / 3,529 / 0 | 12 | 12 | +| `F2 x F2` | 256 | 6 / 117 / 133 / 0 | 0 | 0 | +| `F2[C3]` | 4,096 | 6 / 549 / 3,541 / 0 | 0 | 0 | +| `UT2(F2)` | 4,096 | 6 / 549 / 3,529 / 12 | 0 | 12 | +| `M2(F2)` | 65,536 | 6 / 2,277 / 63,181 / 72 | 0 | 72 | +| `F2[S3]` (criterion only) | 16,777,216 | — | — | 120,060 | + +In every exhaustively searched algebra, the criterion holds exactly on the +targets of cost at most 2, and every criterion failure costs 3 or is +unreachable. The 72 `M2(F2)` failures agree with #4265. + +Claim types: items 1–4 and the lift in item 5 are proofs for every algebra in +scope. The counts in the table and items 5–6 are finite certificates. Cost 3 as +an upper bound is only checked by search on the listed algebras; no general +three-factor theorem is claimed. + +## Method + +`verify.py` builds each algebra from a structure table and checks that it is +associative with `K` central. It precomputes right-ideal membership `z ∈ a R` +by `F_p`-rank. Stage `main` computes the exact minimum on every target by +breadth-first search over words `Q S`, computes `delta` over every `T`, and +asserts: the criterion equals `cost <= 2`, Theorem A, the local statement on +`F2[x,y]/(x,y)^2` (non-units checked to form an ideal), the rank form over +`M2(F2)`, and the expected counts. It also checks that `rho` is a surjective +unital algebra map, lifts a three-factor `M2(F2)` word to `F2[S3]`, and +asserts that the lifted target fails the criterion. Stage `s3` evaluates the +criterion on all `2^24` targets over `F2[S3]`. The script writes nothing. + +## Reproduce + +From the repository root: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/right-vector-two-factor-criterion/verify.py --stage main +~/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/right-vector-two-factor-criterion/verify.py --stage s3 +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/right-vector-two-factor-criterion +``` + +Expected final lines: + +```text +PASS_RIGHT_VECTOR_TWO_FACTOR_CRITERION F2[x,y]/(x,y)^2:4096:12 F2xF2:256:0 F2[C3]:4096:0 UT2(F2):4096:12 M2(F2):65536:72 m2_rank_form=ok f2s3_lift=cost3 no_new_kappa +PASS_RIGHT_VECTOR_TWO_FACTOR_S3 targets=16777216 three_or_more=120060 no_new_kappa +``` + +Each stage takes under 40 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 a formal alphabet. Native frames, hosting, routing, precision and +recursive cost are not priced, and no supplier changes. Theorems B–D are for +`n = 2` only. Whether every reachable target at `n = 2` costs at most 3 is +not proved. The `F2[S3]` count gives cost at least 3; exact costs there are not +searched. Independent human and formal proof-kernel review are unclaimed. + +## Open next questions + +1. **Three factors.** Is every reachable target at `n = 2` reachable with + three factors, over every algebra? Characterise the three-factor set as + Theorem B does for two; with it, the cost at `n = 2` would be exact. +2. **Larger `n`.** With `y_1, ..., y_k` a basis, `k` factors are block column + operations. Write the `n = 3`, `k = 2` condition as a flag of right + ideals and test it by search over `F2[C2]` or `UT2(F2)`. +3. **Commutative non-local algebras.** Is `delta` exact for invertible + targets over every commutative algebra at `n = 2`? A product of local + algebras needs one `(G, H)` that works in every factor. Count criterion + failures over `F3 x F3 x F3` first. + +## Credit + +Produced by Nick Petalas. The alphabet, normal form and lower bound come from +#4243 (`research/right-vector-diagonal-free-basis`); the open questions and the +`M2(F2)` counts come from #4265 (`research/right-vector-general-target`). 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-two-factor-criterion/SOURCES.json b/research/right-vector-two-factor-criterion/SOURCES.json new file mode 100644 index 0000000000..86e1910e4f --- /dev/null +++ b/research/right-vector-two-factor-criterion/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-two-factor-criterion/TASK.json b/research/right-vector-two-factor-criterion/TASK.json new file mode 100644 index 0000000000..1aab7a001b --- /dev/null +++ b/research/right-vector-two-factor-criterion/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 counts in the right-vector alphabet I + u y^T (u in R^n, y in K^n) with free GL_n(K) maps: cost <= 1 for every n and every K-algebra R, an exact two-factor criterion at n = 2 for every R, and its consequences over M_m(K), local algebras and F2[S3]. Answers open questions 2 and 3 of #4265 at n = 2, and open question 1 at n = 2 for local algebras.", + "scope_change_reason": "The card asks whether a larger or nonabelian register model escapes the scoped three-register obstruction. This package answers narrower open questions left by #4243 and #4265 about the exact cost in the right-vector alphabet over nonabelian and non-field coefficient algebras.", + "bottleneck_link": "Side result in a formal alphabet. It decides which targets cost two right-vector factors at n = 2; it prices no native frame or supplier, and kappa is unchanged.", + "budget_minutes": 60, + "stop_rule": "Prove the two-factor criterion, check it against exhaustive search on every target of small algebras, settle the F2[S3] lift, then stop.", + "outcome": "completed", + "evidence": "PROOF.md proves Theorems A-D. verify.py --stage main checks the criterion against breadth-first search on all 77,824 targets over five algebras (agreement everywhere; 12 + 72 cost-3 targets over UT2(F2) and M2(F2); 12 unreachable targets over F2[x,y]/(x,y)^2), the local statement, the M_m(K) rank form over M2(F2), and an explicit cost-3 target over F2[S3]. --stage s3 counts 120,060 criterion failures among all 2^24 targets over F2[S3].", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Is every reachable target at n = 2 reachable with three factors, for every K-algebra?", + "why_it_matters": "Together with Theorem B it would give the exact cost at n = 2. Search finds maximum reachable cost 3 on all five algebras here.", + "first_step": "Characterise the three-factor set (G x I)[[A, 0], [B, 1]][[1, C], [0, D]][[E, 0], [F, 1]](H x I) as Theorem B does for two factors.", + "blocked_by": "Only the two-factor set is characterised here." + }, + { + "question": "What is the cost <= k criterion for n >= 3?", + "why_it_matters": "The right-ideal condition of Theorem B should generalise to a flag condition on block-triangular factorizations.", + "first_step": "With y_1..y_k a basis, products of k factors are block column operations; write the n = 3, k = 2 condition and test it by search over F2[C2] or UT2(F2).", + "blocked_by": "Only n = 2 is proved." + }, + { + "question": "Is delta exact for invertible targets over every commutative K-algebra at n = 2?", + "why_it_matters": "Theorem D proves it for local algebras; products such as F2 x F2 need one (G, H) that works in every factor at once.", + "first_step": "Prove the criterion for invertible M over a product of local algebras with residue field K, or find a counterexample by criterion counting over F3 x F3 x F3.", + "blocked_by": "Non-local commutative algebras are only checked on F2 x F2 and F2[C3] (here and in #4265)." + } + ] +} diff --git a/research/right-vector-two-factor-criterion/VERIFY.json b/research/right-vector-two-factor-criterion/VERIFY.json new file mode 100644 index 0000000000..044e7f9752 --- /dev/null +++ b/research/right-vector-two-factor-criterion/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": 300, + "checks": "Exact minimum by breadth-first search versus the Theorem B criterion on every target over F2[x,y]/(x,y)^2, F2 x F2, F2[C3], UT2(F2) and M2(F2) at n = 2 (77,824 targets); asserts agreement, Theorem A, the local statement, failure counts 12/0/0/12/72, the M_m(K) rank form over M2(F2), and an explicit F2[S3] target of cost 3." + }, + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py", + "--stage", + "s3" + ], + "timeout_seconds": 300, + "checks": "Criterion on all 2^24 targets over F2[S3] at n = 2: exactly 120,060 fail (cost >= 3, delta <= 2), including all 18,432 lifts of the 72 M2(F2) failures." + } + ] +} diff --git a/research/right-vector-two-factor-criterion/verify.py b/research/right-vector-two-factor-criterion/verify.py new file mode 100644 index 0000000000..356dddab35 --- /dev/null +++ b/research/right-vector-two-factor-criterion/verify.py @@ -0,0 +1,382 @@ +"""Exact two-factor criterion for right-vector targets at n = 2. + +Alphabet (research/f2-right-vector-diagonal-minimum, #4243, #4265): paid +factors I + u y^T with u in R^2, y in K^2; free maps GL_2(K) anywhere. +PROOF.md shows, for every K-algebra R, + + cost(M) <= 2 iff some G, H in GL_2(K) give N = G M H with N12 in N11 R, + cost(M) <= 1 iff delta(M) <= 1, and then cost(M) = delta(M). + +For local R, every target with a unit entry then costs delta(M). +Stage "main" compares this criterion with the exact minimum found by +breadth-first search on every target over five algebras (cost 99 means +unreachable), checks the local statement, checks the rank form of the +criterion over M2(F2), and lifts a 3-factor M2(F2) target to F2[S3]. +Stage "s3" counts criterion failures on all 2^24 targets over F2[S3]. +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 == "F2xF2": + return 2, 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,y]/(x,y)^2": # basis 1, x, y; commutative and local + return 2, 3, lambda i, j: {i + j: 1} if i == 0 or j == 0 else {}, [1, 0, 0] + if name == "UT2(F2)": # basis E00, E01, E11 at indices 0, 1, 2 + pos = [(0, 0), (0, 1), (1, 1)] + + def mul(i, j): + (a, b), (c, d) = pos[i], pos[j] + return {pos.index((a, d)): 1} if b == c else {} + return 2, 3, mul, [1, 0, 1] + if name == "M2(F2)": # basis E_ab at index 2a+b + 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] + if name == "F2[S3]": # basis = S3 as permutation tuples, identity first + g = sorted(itertools.permutations(range(3))) + + def mul(i, j): + return {g.index(tuple(g[i][g[j][k]] for k in range(3))): 1} + return 2, 6, mul, [1, 0, 0, 0, 0, 0] + 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)] + m = self.mul + assert all(m[self.one, a] == a == m[a, self.one] for a in range(q)) + 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" + # in_ideal[a, z]: z lies in the right ideal a R = span_K {a b_k} + basis = [self.enc([int(i == k) for i in range(r)]) for k in range(r)] + span = np.array([[self.dec(int(m[a, b])) for b in basis] for a in range(q)]) + base = rank_mod_p(span, p) + ext = np.concatenate([np.repeat(span[:, None], q, 1), + np.array([self.dec(z) for z in range(q)])[None, :, None, :] + .repeat(q, 0)], axis=2).reshape(q * q, r + 1, r) + self.in_ideal = (rank_mod_p(ext, p).reshape(q, q) == base[:, None]) + + 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 gl2(p): + return [t for t in itertools.product(range(p), repeat=4) + if (t[0] * t[3] - t[1] * t[2]) % p] + + +def matmul(R, A, B): + """Row-wise product of 2x2 matrices over R stored as (S, 4) code arrays.""" + C = np.zeros(np.broadcast_shapes(A.shape, B.shape), dtype=np.int64) + for i in range(2): + for j in range(2): + C[:, 2 * i + j] = R.add[R.mul[A[:, 2 * i], B[:, j]], R.mul[A[:, 2 * i + 1], B[:, 2 + j]]] + return C + + +def lift(R, t): + return np.array([[R.scal[x] for x in t]], dtype=np.int64) + + +def criterion(R, M): + """True where some G, H in GL_2(K) give N = G M H with N12 in N11 R.""" + ok = np.zeros(len(M), dtype=bool) + gls = [lift(R, t) for t in gl2(R.p)] + for G in gls: + GM = matmul(R, G, M) + for H in gls: + N = matmul(R, GM, H) + ok |= R.in_ideal[N[:, 0], N[:, 1]] + return ok + + +def all_targets(q): + size = q ** 4 + return np.stack([(np.arange(size) // q ** k) % q for k in range(4)], axis=1) + + +UNREACHABLE = 99 +LOCAL = ("F2[x,y]/(x,y)^2",) + + +def exact_costs(R, allM): + """Exact minimum number of paid factors by BFS over words Q S (#4243).""" + q, p = R.q, R.p + pw = q ** np.arange(4) + ident = np.array([R.one, 0, 0, R.one]) + ys = [(1, 0)] + [(x, 1) for x in range(p)] + facs = np.unique(np.array([[R.add[ident[2 * i + j], R.mul[u[i], R.scal[y[j]]]] + for i in range(2) for j in range(2)] + for u in itertools.product(range(q), repeat=2) for y in ys]), axis=0) + level = np.full(len(allM), -1, dtype=np.int64) + front = np.concatenate([lift(R, t) for t in gl2(p)]) + level[front @ pw] = 0 + L = 0 + while len(front): + L += 1 + new = [] + for F in facs: + P = matmul(R, F[None], 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) + level[level < 0] = UNREACHABLE + return level + + +def delta(R, allM): + """min over T in GL_2(K) of dim_K (M T - I) K^2.""" + p, r = R.p, R.r + best = np.full(len(allM), 9, dtype=np.int64) + ident = np.array([R.one, 0, 0, R.one]) + for t in gl2(p): + D = R.add[matmul(R, allM, lift(R, t)), R.neg[ident][None, :]] + V = np.zeros((len(allM), 2, 2 * r), dtype=np.int64) + for j in range(2): + for i in range(2): + for k in range(r): + V[:, j, i * r + k] = (D[:, 2 * i + j] // p ** k) % p + best = np.minimum(best, rank_mod_p(V, p)) + return best + + +def compare(name): + R = Ring(name) + allM = all_targets(R.q) + cost = exact_costs(R, allM) + dlt = delta(R, allM) + crit = criterion(R, allM) + assert (cost >= dlt).all(), "lower bound of #4243 violated" + assert ((cost <= 2) == crit).all(), "two-factor criterion disagrees with search" + assert ((cost <= 1) == (dlt <= 1)).all() and (cost[dlt <= 1] == dlt[dlt <= 1]).all() + unit = R.in_ideal[:, R.one] + if name in LOCAL: # the non-units form an ideal J + nonunit = np.nonzero(~unit)[0] + assert np.isin(R.add[nonunit[:, None], nonunit[None, :]], nonunit).all() + assert np.isin(R.mul[nonunit[:, None], np.arange(R.q)[None, :]], nonunit).all() + has_unit = unit[allM].any(1) + assert (cost[has_unit] == dlt[has_unit]).all(), "local theorem violated" + assert not (~crit & has_unit).any() + return R, allM, cost, crit, {"ring": name, "targets": len(allM), + "cost_hist": np.bincount(cost[cost < UNREACHABLE]).tolist(), + "unreachable": int((cost == UNREACHABLE).sum()), + "criterion_failures": int((~crit).sum()), + "delta_gaps": int((cost != dlt).sum())} + + +def m2_rank_form(R, allM, crit): + """Over M2(F2): criterion iff some phi, t != 0 give rank (phi x I) M = rank (phi x I) M (t x I).""" + bits = ((allM[:, :, None] >> np.arange(4)[None, None, :]) & 1).reshape(-1, 2, 2, 2, 2) + big = bits.transpose(0, 1, 3, 2, 4).reshape(-1, 4, 4) # [2i+a, 2j+b] = bit 2a+b of entry (i,j) + vecs = [np.array(v) for v in ((1, 0), (0, 1), (1, 1))] + I2 = np.eye(2, dtype=np.int64) + ok = np.zeros(len(allM), dtype=bool) + for phi in vecs: + top = np.einsum("ij,sjk->sik", np.kron(phi[None, :], I2), big) % 2 + rk = rank_mod_p(top, 2) + for t in vecs: + ok |= rank_mod_p(top @ np.kron(t[:, None], I2) % 2, 2) == rk + assert (ok == crit).all(), "rank form disagrees" + + +def s3_rep(): + """Unital K-algebra map rho: F2[S3] -> M2(F2) from S3 = GL_2(F_2) on nonzero vectors.""" + S, M = Ring("F2[S3]"), Ring("M2(F2)") + g = sorted(itertools.permutations(range(3))) + v = [(1, 0), (0, 1), (1, 1)] + mats = [M.enc([v[s[0]][0], v[s[1]][0], v[s[0]][1], v[s[1]][1]]) for s in g] + rho = np.array([0] * S.q, dtype=np.int64) + for x in range(S.q): + acc = 0 + for k, c in enumerate(S.dec(x)): + if c: + acc = M.add[acc, mats[k]] + rho[x] = acc + assert rho[S.one] == M.one + assert (rho[S.mul] == M.mul[rho[:, None], rho[None, :]]).all(), "rho not multiplicative" + assert (rho[S.add] == M.add[rho[:, None], rho[None, :]]).all() + assert len(set(rho.tolist())) == M.q, "rho not surjective" + return S, M, rho + + +def s3_witness(M, cost_m2): + """Lift a 3-factor M2(F2) word to F2[S3]; its image costs 3, so it costs 3.""" + S, Mr, rho = s3_rep() + section = {int(rho[x]): x for x in range(S.q - 1, -1, -1)} + pw = Mr.q ** np.arange(4) + target = np.array([Mr.enc([0, 0, 0, 1]), Mr.enc([0, 1, 0, 0]), + Mr.enc([0, 0, 1, 0]), Mr.enc([1, 0, 0, 0])]) # [[E11, E01], [E10, E00]] + assert cost_m2[target @ pw] == 3 + # find a 3-factor word over M2(F2) ending in a free map that hits the target + ys = [(1, 0), (0, 1), (1, 1)] + ident_m = np.array([Mr.one, 0, 0, Mr.one]) + words = [(u, y) for u in itertools.product(range(Mr.q), repeat=2) for y in ys] + + def fac(R, u, y): + return np.array([[R.add[[R.one, 0, 0, R.one][2 * i + j], R.mul[u[i], R.scal[y[j]]]] + for i in range(2) for j in range(2)]]) + gls = gl2(2) + want = {} + for t in gls: # target T^{-1} + X = target[None] + for s in gls: + if (matmul(Mr, lift(Mr, t), lift(Mr, s)) == ident_m).all(): + want[int(matmul(Mr, X, lift(Mr, s))[0] @ pw)] = t + found = None + for w1 in words: + A = fac(Mr, *w1) + for w2 in words: + AB = matmul(Mr, A, fac(Mr, *w2)) + for w3 in words: + code = int(matmul(Mr, AB, fac(Mr, *w3))[0] @ pw) + if code in want: + found = (w1, w2, w3, want[code]) + break + if found: + break + if found: + break + assert found, "no three-factor word" + *ws, t = found + W = lift(S, (1, 0, 0, 1)) + for u, y in ws: + W = matmul(S, W, fac(S, (section[u[0]], section[u[1]]), y)) + W = matmul(S, W, lift(S, t)) + assert (rho[W[0]] == target).all() + assert not criterion(S, W)[0], "lifted witness passes the criterion" + return [S.dec(int(x)) for x in W[0]], [ws, t] + + +def s3_count(): + S, _, rho = s3_rep() + q = S.q + fails = 0 + proj_fails = 0 + m2 = Ring("M2(F2)") + m2_crit = criterion(m2, all_targets(m2.q)) + chunk = q ** 3 + M = np.zeros((chunk, 4), dtype=np.int64) + for k in range(3): + M[:, k] = (np.arange(chunk) // q ** k) % q + for hi in range(q): + M[:, 3] = hi + c = criterion(S, M) + fails += int((~c).sum()) + img = rho[M] @ (m2.q ** np.arange(4)) + proj_fails += int((~m2_crit[img]).sum()) + assert not (c & ~m2_crit[img]).any(), "projection failure without lift failure" + return {"targets": q ** 4, "criterion_failures": fails, + "projected_m2_failures": proj_fails} + + +EXPECTED = {"F2[x,y]/(x,y)^2": (4096, 12), "F2xF2": (256, 0), "F2[C3]": (4096, 0), "UT2(F2)": (4096, 12), "M2(F2)": (65536, 72)} + + +def main(): + stage = sys.argv[sys.argv.index("--stage") + 1] if "--stage" in sys.argv else "main" + assert stage in ("main", "s3"), stage + with open(__file__, "rb") as fh: + digest = hashlib.sha256(fh.read()) + digest.update(stage.encode()) + if stage == "s3": + res = s3_count() + print(res, flush=True) + assert res["criterion_failures"] == 120060 + assert res["projected_m2_failures"] == 72 * 4 ** 4 # kernel of rho has 4 elements + digest.update(repr(res).encode()) + print("receipt", digest.hexdigest()) + print("PASS_RIGHT_VECTOR_TWO_FACTOR_S3", f"targets={res['targets']}", + f"three_or_more={res['criterion_failures']}", "no_new_kappa") + return 0 + parts = [] + for name in EXPECTED: + R, allM, cost, crit, res = compare(name) + print(res, flush=True) + assert (res["targets"], res["criterion_failures"]) == EXPECTED[name], name + fail_costs = sorted(set(cost[~crit].tolist())) + assert fail_costs == ([UNREACHABLE] if name in LOCAL else [3] if res["criterion_failures"] else []) + assert res["unreachable"] == (12 if name in LOCAL else 0) + digest.update(repr(res).encode()) + parts.append(f"{name}:{res['targets']}:{res['criterion_failures']}") + if name == "M2(F2)": + m2_rank_form(R, allM, crit) + wit, word = s3_witness(R, cost) + print("F2[S3] witness (entries in group basis):", wit, "word:", word, flush=True) + digest.update(repr((wit, word)).encode()) + print("receipt", digest.hexdigest()) + print("PASS_RIGHT_VECTOR_TWO_FACTOR_CRITERION", " ".join(parts), + "m2_rank_form=ok f2s3_lift=cost3 no_new_kappa") + return 0 + + +if __name__ == "__main__": + sys.exit(main())