diff --git a/research/borrowed-shear-general-endpoint/README.md b/research/borrowed-shear-general-endpoint/README.md new file mode 100644 index 0000000000..f909088262 --- /dev/null +++ b/research/borrowed-shear-general-endpoint/README.md @@ -0,0 +1,152 @@ +# Square-zero is necessary for the borrowed-space shear tariff + +**Scoped proof with exact finite census; no new κ.** + +Ali Romman's [PR #5640](https://github.com/CrocSwap/integer-mult-bounds/pull/5640) +(`research/borrowed-space-shear-tariff`) proves that a square-zero update +`diag(I+N, I_q)` of rank r costs exactly `2 ceil(r/q) + 2` cross-bank shears +with q arbitrary dirty borrowed coordinates. Its lower bound holds for every +endpoint `diag(T, I_q)`, but its attaining word needs `N^2 = 0`. This package +answers what happens for a general endpoint. + +**Theorem.** Over any field K, for any n, q >= 1 and any n by n matrix T, if a +word in the PR #5640 alphabet implements `diag(T, I_q)` using at most two +gathers, or at most two scatters, then `(T - I)^2 = 0`. + +**Corollary.** If `(T - I)^2 != 0` and `r = rank(T - I)`, every implementing +word has at least `max(ceil(r/q)+1, 3)` gathers and as many scatters, so at +least + + max(2 ceil(r/q) + 2, 6) shears. + +When `r <= q` the PR #5640 count of four shears cannot be attained by any +non-square-zero T. The extra cost is exactly two shears in every domain +enumerated below. + +**Finite census (exact minima).** A breadth-first search over the whole group +generated by the alphabet gives the exact minimum for every reachable endpoint +in six domains. Every one equals + + tariff(T) = 2 ceil(r/q) + 2 if (T - I)^2 = 0, + tariff(T) = max(2 ceil(r/q) + 2, 6) otherwise. + +| field | n | q | group order | square-zero endpoints | non-square-zero endpoints | +|---|---|---|---:|---:|---:| +| F2 | 2 | 1 | 168 | 3 (min 4) | 2 (min 6) | +| F2 | 2 | 2 | 20,160 | 3 (min 4) | 2 (min 6) | +| F2 | 3 | 1 | 20,160 | 21 (min 4) | 98 (min 6), 48 (min 8) | +| F3 | 2 | 1 | 5,616 | 8 (min 4) | 15 (min 6) | +| F5 | 2 | 1 | 372,000 | 24 (min 4) | 95 (min 6) | +| F2 | 3 | 2 | 9,999,360 | 21 (min 4) | 98 (min 6), 48 (min 6) | + +The last row comes from the opt-in NumPy script; the others come from the +registered standard-library verifier. Each reachable set is all of `SL(n, F_p)`. +The F2, n=q=2 row is the smallest case where the square-zero formula fails: its +two non-square-zero endpoints have `r = 2 = q`, so the rank bound allows 4, but +6 are needed. On F2, n=3, q=2 the rank-3 endpoints meet the rank bound 6 exactly. +So the 6-shear floor and the rank bound both bind there, at different endpoints. + +## Proof + +Write the current state as `x = X x0 + Y z0`, `z = C x0 + D z0`, starting from +`(X,Y,C,D) = (I,0,0,I)`. A gather `G(A)` sets `C += A X`, `D += A Y`. A scatter +`S(B)` sets `X += B C`, `Y += B D`. The endpoint requires `X = T`, `Y = 0`, +`C = 0`, `D = I`. + +Adjacent gates of one kind merge (`G(A)G(A') = G(A+A')`). So every word with at +most two gathers is `S(B0) G(A1) S(B1) G(A2) S(B2)`, with some matrices +possibly zero. Its states are, in order: + + S(B0): X = I, Y = B0 + G(A1): C = A1, D = I + A1 B0 + S(B1): X = I + B1 A1, Y = B0 + B1 (I + A1 B0) + G(A2): C = A1 + A2 (I + B1 A1) + D = I + A1 B0 + A2 Y + S(B2): X = I + B1 A1 + B2 C, Y = Y + B2 D. + +The endpoint gives `C = 0` after `G(A2)`, so `A1 = -A2 (I + B1 A1)` and the +final data block is `T = I + B1 A1`. Expand `A2 Y` with `C = 0`: + + A2 Y = A2 (I + B1 A1) B0 + A2 B1 = -A1 B0 + A2 B1, + +so `D = I` forces `A2 B1 = 0`. Multiply `A1 = -A2 (I + B1 A1)` on the right by +B1: `A1 B1 = -A2 B1 - (A2 B1) A1 B1 = 0`. Hence + + (T - I)^2 = B1 (A1 B1) A1 = 0. + +The final `Y = 0` only fixes B2 and adds no constraint. For words with at most +two scatters, use the PR #5640 transpose-reversal. Transposing the complete +matrix product and reversing its order gives a word for `diag(T^T, I_q)` with +gathers and scatters exchanged. Then `(T^T - I)^2 = ((T - I)^2)^T = 0`. + +The corollary combines this with the PR #5640 bound `k, l >= ceil(r/q)+1`. +The argument uses the restoration of arbitrary dirty borrowed inputs (`D = I`). + +## Evidence and reproduction + +From the repository root, with CPython 3.12 and only the standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/borrowed-shear-general-endpoint +python3.12 -I -W error -B research/borrowed-shear-general-endpoint/verify.py +python3.12 -I -O -W error -B research/borrowed-shear-general-endpoint/verify.py +``` + +The verifier prints a JSON `RESULT` payload and `PASS_BORROWED_SHEAR_GENERAL_ENDPOINT`; +it takes about 21 seconds locally. For each of the five standard-library domains it: + +- enumerates the full group by breadth-first search, so each distance is an + exact minimum over all words; +- checks every endpoint `diag(T, I_q)` against the tariff above; +- replays one shortest witness word per endpoint as a literal (n+q)-square + matrix product and checks it equals `diag(T, I_q)`, including the dirty + borrowed columns; +- checks that every shortest non-square-zero witness has at least three + gathers and three scatters, as the theorem requires. + +Controls: the square-zero-only formula `2 ceil(r/q)+2` is refuted on exactly the +two F2, n=q=2 non-square-zero endpoints, and a witness with one corrupted +coefficient fails to replay. All checks are explicit and survive `-O`. + +The F2, n=3, q=2 row needs NumPy and about 70 seconds and 40 MB of distance table. +It is not registered in VERIFY.json: + +```sh +python3.12 -B -I research/borrowed-shear-general-endpoint/extended_census.py +``` + +It passed locally with NumPy 2.5.4 (`PASS_EXTENDED_CENSUS`, group order 9,999,360, +168 endpoints, 0 mismatches). That row is local evidence only; CI does not run it. + +## Limits + +The theorem is a written proof checked by its author only; human and formal +proof-kernel review are unclaimed. The census covers only the six listed +domains. **No general upper bound is proved for non-square-zero T.** Whether +`max(2 ceil(r/q)+2, 6)` is attainable for every T over every field is open. +The clean-borrowed-coordinate variant, coefficient costs, precision and the +translation-kernel extension of PR #5640 are not treated. This is a side +result in the same alphabet. It changes no κ, selected frontier, physical +supplier or caller bill. + +## Open next questions + +- **Is `max(2 ceil(r/q)+2, 6)` always attainable?** It is exact in every + enumerated domain. A proof would complete the tariff for general endpoints + in this alphabet. First step: build a six-shear word `GSGSGS` for an + arbitrary `T` in `SL(n, K)` when `q >= n`. Then try to splice it with the + grouped PR #5640 word for larger r. Blocker: the PR #5640 cross-products + `L_i V_j = 0` fail for non-square-zero factors, so a new invariant is needed. +- **Which endpoints are reachable at all?** Each shear has determinant one, so + `det T = 1` is necessary. Each census domain reaches all of `SL(n, F_p)`. A + general proof for every field and every q is not supplied here. +- **Does the clean-borrowed tariff `2 ceil(r/q)+1` show the same square-zero + gap?** The transpose argument is unavailable there, as PR #5640 notes. The + one-sided gather argument above may still apply. + +## Credit + +Produced by Nick Petalas. Ali Romman (@aliromman, PR #5640) supplies the +alphabet, the rank lower bound, the transpose-reversal argument and the +square-zero construction that this package extends. Dugongue (PR #5634) +supplies the reader-recoding application that motivated PR #5640. Apache-2.0. diff --git a/research/borrowed-shear-general-endpoint/SOURCES.json b/research/borrowed-shear-general-endpoint/SOURCES.json new file mode 100644 index 0000000000..d596e2e530 --- /dev/null +++ b/research/borrowed-shear-general-endpoint/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + } + ] +} diff --git a/research/borrowed-shear-general-endpoint/TASK.json b/research/borrowed-shear-general-endpoint/TASK.json new file mode 100644 index 0000000000..b1a8e3647b --- /dev/null +++ b/research/borrowed-shear-general-endpoint/TASK.json @@ -0,0 +1,107 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact borrowed-space cross-bank shear tariff for a general endpoint diag(T, I_q) in the PR #5640 alphabet: a written proof that at most two gathers or at most two scatters force (T-I)^2 = 0, so non-square-zero endpoints need at least max(2 ceil(r/q)+2, 6) shears, plus exact breadth-first minima on six small prime-field domains.", + "scope_change_reason": "The card asks for a missing interface implication. PR #5640 proves its tariff only for square-zero updates although its lower bound applies to every endpoint; this package settles the square-zero dependence of the lower bound. It is a written mathematical side result, not a Lean formalization or a selected-caller binding.", + "bottleneck_link": "Side result: it prices reader recoding with borrowed dirty coordinates when the update is not square-zero. It changes no complete signed bill, kappa or selected frontier.", + "budget_minutes": 60, + "stop_rule": "Ship the lower-bound theorem and the exact census once every enumerated minimum matches; leave the general attaining construction as an open question.", + "outcome": "partial", + "evidence": "README.md proof; verify.py exhaustive BFS minima and witness replays on F2 (n,q)=(2,1),(2,2),(3,1), F3 (2,1), F5 (2,1); opt-in extended_census.py on F2 (3,2), local only.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Is max(2 ceil(r/q)+2, 6) attainable for every non-square-zero endpoint over every field?", + "why_it_matters": "It would complete the exact borrowed-space tariff for general endpoints in this alphabet.", + "first_step": "Construct a six-shear GSGSGS word for arbitrary T in SL(n,K) with q >= n, then splice with the grouped PR #5640 word for larger r.", + "blocked_by": "The PR #5640 condition L_i V_j = 0 fails for non-square-zero factors; no replacement invariant is known." + }, + { + "question": "Is every T in SL(n,K) reachable for every field and every q >= 1?", + "why_it_matters": "det T = 1 is necessary; reachability decides where the tariff is finite.", + "first_step": "Prove that the alphabet generates the block-unipotent subgroup and contains diag(SL(n,K), I_q).", + "blocked_by": "Only the six enumerated domains are checked here." + }, + { + "question": "Does the clean-borrowed count 2 ceil(r/q)+1 have the same square-zero gap?", + "why_it_matters": "Clean scratch is a separate alphabet use in PR #5640.", + "first_step": "Redo the two-gather state calculation with z0 = 0 and without the transpose argument.", + "blocked_by": "The transpose-reversal argument does not apply to clean coordinates." + } + ] +} diff --git a/research/borrowed-shear-general-endpoint/VERIFY.json b/research/borrowed-shear-general-endpoint/VERIFY.json new file mode 100644 index 0000000000..a28c29d83b --- /dev/null +++ b/research/borrowed-shear-general-endpoint/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Exact BFS shear minima on five prime-field domains against the general-endpoint tariff, literal witness replays, gather/scatter counts and two rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Same exact checks under optimized Python; all checks are explicit." + } + ] +} diff --git a/research/borrowed-shear-general-endpoint/extended_census.py b/research/borrowed-shear-general-endpoint/extended_census.py new file mode 100644 index 0000000000..459d46f99e --- /dev/null +++ b/research/borrowed-shear-general-endpoint/extended_census.py @@ -0,0 +1,72 @@ +#!/usr/bin/env python3 +"""Opt-in NumPy census over F2 (default n=3, q=2): exact minima for every diag(T, I_q). + +Not registered in VERIFY.json; run with an interpreter that has NumPy. +""" +import itertools, sys +import numpy as np +from collections import Counter +n, q = map(int, sys.argv[1:3]) if len(sys.argv) > 2 else (3, 2); m = n + q; M = (1 << m) - 1 +def pack(cols): return sum(c << (i*m) for i, c in enumerate(cols)) +I = pack([1 << i for i in range(m)]) +gens = [] # (kind, matrix) kind 'G': for x-col j list of z-cols a ; 'S': for z-col a list of x-cols i +for vals in itertools.product((0,1), repeat=q*n): + if not any(vals): continue + gens.append(('G', [[a for a in range(q) if vals[a*n+j]] for j in range(n)])) + gens.append(('S', [[i for i in range(n) if vals[a*n+i]] for a in range(q)])) +dist = np.full(1 << (m*m), 255, dtype=np.uint8); dist[I] = 0 +front = np.array([I], dtype=np.uint64); d = 0 +while front.size: + d += 1 + cols = [(front >> np.uint64(c*m)) & np.uint64(M) for c in range(m)] + new = [] + for kind, spec in gens: + nc = list(cols) + if kind == 'G': + for j in range(n): + for a in spec[j]: nc[j] = nc[j] ^ cols[n+a] + else: + for a in range(q): + for i in spec[a]: nc[n+a] = nc[n+a] ^ cols[i] + v = nc[0].copy() + for c in range(1, m): v |= nc[c] << np.uint64(c*m) + new.append(v) + cand = np.unique(np.concatenate(new)) + cand = cand[dist[cand] == 255] + dist[cand] = d; front = cand +def rank2(rows): + rows = list(rows); r = 0 + for bit in range(n): + piv = next((i for i in range(r, len(rows)) if rows[i] >> bit & 1), None) + if piv is None: continue + rows[r], rows[piv] = rows[piv], rows[r] + for i in range(len(rows)): + if i != r and rows[i] >> bit & 1: rows[i] ^= rows[r] + r += 1 + return r +def matmul(A, B): # row bitmask matrices n x n: row i bit j + return [ (lambda ri: __import__('functools').reduce(lambda acc, k: acc ^ (B[k] if ri >> k & 1 else 0), range(n), 0))(A[i]) for i in range(n)] +stats = Counter() +for Tbits in range(1 << (n*n)): + Trows = [(Tbits >> (i*n)) & ((1 << n) - 1) for i in range(n)] + # column j of full matrix: bits i of rows + cols = [sum(((Trows[i] >> j) & 1) << i for i in range(n)) for j in range(n)] + [1 << (n+a) for a in range(q)] + dd = int(dist[pack(cols)]) + if dd == 255: continue + N = [Trows[i] ^ (1 << i) for i in range(n)] + r = rank2(N); P = N; nil = None + for e in range(1, n+2): + if not any(P): nil = e; break + P = matmul(P, N) + N2 = matmul(N, N) + stats[(r, rank2(N2), nil, dd)] += 1 +bad = 0 +for (r, r2, nil, dd), cnt in sorted(stats.items(), key=lambda kv: (kv[0][0], kv[0][1], kv[0][2] or 99, kv[0][3])): + base = 2 * (-(-r // q)) + 2 if r else 0 + want = base if r2 == 0 else max(base, 6) + bad += cnt * (dd != want) + print("r=%d rank((T-I)^2)=%d nilpotency_index=%s minimum=%d tariff=%d : %d" % (r, r2, nil, dd, want, cnt)) +print("group_order", int((dist != 255).sum()), "endpoints", sum(stats.values()), "mismatches", bad) +if bad: + raise SystemExit("FAIL: tariff mismatch") +print("PASS_EXTENDED_CENSUS") diff --git a/research/borrowed-shear-general-endpoint/verify.py b/research/borrowed-shear-general-endpoint/verify.py new file mode 100644 index 0000000000..fd12e995a6 --- /dev/null +++ b/research/borrowed-shear-general-endpoint/verify.py @@ -0,0 +1,227 @@ +#!/usr/bin/env python3 +"""Exact borrowed-space shear minima for general endpoints diag(T, I_q). + +Alphabet (PR #5640): gathers G(A): z <- z + A x and scatters S(B): x <- x + B z, +with x in K^n (data) and z in K^q (arbitrary dirty borrowed coordinates). +A word implements diag(T, I_q) when it maps (x0, z0) to (T x0, z0) for all inputs. + +For each small domain this script runs a breadth-first search over the whole +group generated by the alphabet, so each recorded distance is the exact minimum +number of shears. It then checks every reachable endpoint against + + tariff(T) = 2 ceil(r/q) + 2 if (T - I)^2 = 0, + tariff(T) = max(2 ceil(r/q) + 2, 6) otherwise, r = rank(T - I) > 0, + +replays one shortest witness word per endpoint on the full (n+q)-square matrix, +and runs rejecting controls. +""" +import hashlib +import itertools +import json +import pathlib +import sys + +# (p, n, q): every domain is enumerated completely. +DOMAINS = ((2, 2, 1), (2, 2, 2), (2, 3, 1), (3, 2, 1), (5, 2, 1)) +MAX_GROUP = 400_000 + + +def check(condition, message): + """Explicit check that stays active under python -O.""" + if not condition: + raise SystemExit("FAIL: " + message) + + +def generators(p, n, q): + """Each generator is (kind, target_column, ((source_column, coeff), ...)) lists. + + Right multiplication by G(A) adds sum_a A[a][j] * column(n+a) to column j; + right multiplication by S(B) adds sum_i B[i][a] * column(i) to column n+a. + """ + gens = [] + for vals in itertools.product(range(p), repeat=q * n): + if not any(vals): + continue + gather = tuple((j, tuple((n + a, vals[a * n + j]) for a in range(q) if vals[a * n + j])) + for j in range(n)) + scatter = tuple((n + a, tuple((i, vals[a * n + i]) for i in range(n) if vals[a * n + i])) + for a in range(q)) + gens.append(("G", vals, gather)) + gens.append(("S", vals, scatter)) + return gens + + +def apply_gen(p, m, X, gen): + """Return X * g for a row-major flat matrix X (tuple of length m*m).""" + cols = [X[c::m] for c in range(m)] + new = list(cols) + for target, sources in gen[2]: + if not sources: + continue + col = list(cols[target]) + for src, coeff in sources: + col = [(a + coeff * b) % p for a, b in zip(col, cols[src])] + new[target] = col + return tuple(new[c][r] for r in range(m) for c in range(m)) + + +def gen_matrix(p, n, q, gen): + """Literal (n+q)-square matrix of a generator, built from its definition.""" + m = n + q + M = [[int(i == j) for j in range(m)] for i in range(m)] + kind, vals = gen[0], gen[1] + for a in range(q): + for b in range(n): + if kind == "G": + M[n + a][b] = vals[a * n + b] # z_a += A[a][b] x_b + else: + M[b][n + a] = vals[a * n + b] # x_b += B[b][a] z_a + return M + + +def matmul(p, X, Y): + return [[sum(X[i][k] * Y[k][j] for k in range(len(Y))) % p for j in range(len(Y[0]))] + for i in range(len(X))] + + +def rank(p, M): + rows = [list(r) for r in M] + r = 0 + for c in range(len(rows[0]) if rows else 0): + piv = next((i for i in range(r, len(rows)) if rows[i][c] % p), None) + if piv is None: + continue + rows[r], rows[piv] = rows[piv], rows[r] + inv = pow(rows[r][c], p - 2, p) + rows[r] = [v * inv % p for v in rows[r]] + for i in range(len(rows)): + if i != r and rows[i][c] % p: + f = rows[i][c] + rows[i] = [(a - f * b) % p for a, b in zip(rows[i], rows[r])] + r += 1 + return r + + +def bfs(p, n, q): + m = n + q + gens = generators(p, n, q) + ident = tuple(int(i == j) for i in range(m) for j in range(m)) + parent = {ident: None} + dist = {ident: 0} + frontier = [ident] + while frontier: + nxt = [] + for X in frontier: + for gi, g in enumerate(gens): + Y = apply_gen(p, m, X, g) + if Y not in dist: + dist[Y] = dist[X] + 1 + parent[Y] = (X, gi) + nxt.append(Y) + check(len(dist) <= MAX_GROUP, "group exceeds bounded size") + frontier = nxt + return gens, dist, parent + + +def word_to(parent, X): + word = [] + while parent[X] is not None: + X, gi = parent[X] + word.append(gi) + return word[::-1] + + +def tariff(r, q, square_zero): + base = 2 * (-(-r // q)) + 2 + return base if square_zero else max(base, 6) + + +def census(p, n, q): + m = n + q + gens, dist, parent = bfs(p, n, q) + rows = {} + old_formula_misses = 0 + for X, d in dist.items(): + full = [list(X[i * m:(i + 1) * m]) for i in range(m)] + if any(full[n + a][j] != int(n + a == j) for a in range(q) for j in range(m)): + continue + if any(full[i][n + a] for i in range(n) for a in range(q)): + continue + T = [row[:n] for row in full[:n]] + N = [[(T[i][j] - int(i == j)) % p for j in range(n)] for i in range(n)] + r = rank(p, N) + if r == 0: + check(d == 0, "identity must cost zero") + continue + sq0 = not any(v for row in matmul(p, N, N) for v in row) + want = tariff(r, q, sq0) + check(d == want, f"F{p} n={n} q={q}: T={T} minimum {d} != tariff {want}") + if d != 2 * (-(-r // q)) + 2: + old_formula_misses += 1 + # Replay one shortest witness on the literal full matrix. + word = word_to(parent, X) + check(len(word) == d, "witness length differs from distance") + prod = [[int(i == j) for j in range(m)] for i in range(m)] + for gi in word: + prod = matmul(p, prod, gen_matrix(p, n, q, gens[gi])) + check(prod == full, "witness word does not replay to diag(T, I)") + kinds = [gens[gi][0] for gi in word] + check(all(a != b for a, b in zip(kinds, kinds[1:])), "shortest word must alternate") + if not sq0: + check(kinds.count("G") >= 3 and kinds.count("S") >= 3, + "non-square-zero witness with at most two gathers or scatters") + key = f"r={r},square_zero={sq0},min={d}" + rows[key] = rows.get(key, 0) + 1 + return {"p": p, "n": n, "q": q, "group_order": len(dist), + "endpoint_classes": dict(sorted(rows.items())), + "endpoints_checked": sum(rows.values()) + 1, + "pr5640_formula_underestimates": old_formula_misses} + + +def controls(): + """Rejecting controls: a wrong tariff and a corrupted witness must fail.""" + out = {} + # Control 1: the square-zero-only tariff 2ceil(r/q)+2 is refuted on F2, n=q=2. + res = census(2, 2, 2) + check(res["pr5640_formula_underestimates"] == 2, "expected two non-square-zero misses") + out["square_zero_formula_refuted_on_F2_n2_q2"] = res["pr5640_formula_underestimates"] + # Control 2: a single corrupted coefficient in a witness changes the endpoint. + p, n, q = 3, 2, 1 + gens, dist, parent = bfs(p, n, q) + m = n + q + target = next(X for X, d in dist.items() if d == 6 + and all(X[(n + a) * m + j] == int(n + a == j) for a in range(q) for j in range(m)) + and all(X[i * m + n + a] == 0 for i in range(n) for a in range(q))) + word = word_to(parent, target) + bad = list(word) + g0 = gens[bad[0]] + alt = next(i for i, g in enumerate(gens) if g[0] == g0[0] and g[1] != g0[1]) + bad[0] = alt + prod = [[int(i == j) for j in range(m)] for i in range(m)] + for gi in bad: + prod = matmul(p, prod, gen_matrix(p, n, q, gens[gi])) + full = [list(target[i * m:(i + 1) * m]) for i in range(m)] + check(prod != full, "corrupted witness unexpectedly replays") + out["corrupted_witness_rejected"] = True + return out + + +def main(): + results = [census(*dom) for dom in DOMAINS] + totals = {"non_square_zero_endpoints": 0, "square_zero_endpoints": 0} + for res in results: + for key, count in res["endpoint_classes"].items(): + totals["square_zero_endpoints" if "square_zero=True" in key + else "non_square_zero_endpoints"] += count + payload = {"domains": results, "totals": totals, "controls": controls()} + here = pathlib.Path(__file__).resolve().parent + digest = hashlib.sha256() + for name in sorted(f.name for f in here.iterdir() if f.is_file()): + digest.update(name.encode() + b"\0" + (here / name).read_bytes()) + payload["package_sha256"] = digest.hexdigest() + print(json.dumps(payload, indent=1, sort_keys=True)) + print("PASS_BORROWED_SHEAR_GENERAL_ENDPOINT") + + +if __name__ == "__main__": + sys.exit(main())