From 0764ab259a8ce496a4c5d4debeed4c4e4d9f7ca4 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Thu, 22 Oct 2026 20:50:05 +0100 Subject: [PATCH] feat(research): classify split radical pencil reachability --- research/split-radical-pencil/README.md | 230 ++++++++++++++++ research/split-radical-pencil/SOURCES.json | 24 ++ research/split-radical-pencil/TASK.json | 104 ++++++++ research/split-radical-pencil/VERIFY.json | 32 +++ research/split-radical-pencil/verify.py | 293 +++++++++++++++++++++ 5 files changed, 683 insertions(+) create mode 100644 research/split-radical-pencil/README.md create mode 100644 research/split-radical-pencil/SOURCES.json create mode 100644 research/split-radical-pencil/TASK.json create mode 100644 research/split-radical-pencil/VERIFY.json create mode 100644 research/split-radical-pencil/verify.py diff --git a/research/split-radical-pencil/README.md b/research/split-radical-pencil/README.md new file mode 100644 index 0000000000..c75b9d4962 --- /dev/null +++ b/research/split-radical-pencil/README.md @@ -0,0 +1,230 @@ +# Exact reachability of square-zero radical pencils + +This package was produced by Nick Petalas. Apache-2.0. + +**Scoped algebraic proof, with finite corroboration.** For every field K, +every n >= 1 and A in M_n(K), put R = K[x,y]/(x,y)^2. Allow paid factors +I + u v^T with u in R^n and v in K^n, including singular factors, and free +GL_n(K) maps anywhere. Then + +```text +xI_n + yA is reachable + if and only if the characteristic polynomial of A splits over K. +When reachable, its exact paid cost is n. +``` + +A scalar eigenvalue alone is insufficient. For example, over F2, + +```text + [0 0 0] +A = [0 0 1] has characteristic polynomial t(t^2+t+1). + [0 1 1] +``` + +Its pencil is unreachable at every finite length, although A has eigenvalue +zero. This settles Open next question 1 of +[PR #4773](https://github.com/CrocSwap/integer-mult-bounds/pull/4773), whose +necessary condition only excludes matrices without a base-field eigenvalue. +The new proof uses determinants of polynomial lifts, followed by a sharp +column-replacement construction. It does not audit the predecessor theorem. +No new kappa, supplier admission or complete multiplication theorem is claimed. + +## Proof + +### Necessity by polynomial lifting + +Take any alleged finite word, including its free maps. Every paid left vector +has a unique expression a + xb + yc with a,b,c in K^n. Lift that factor to + +```text +F_hat = I + (a + Xb + Yc) v^T over K[X,Y], +``` + +and lift each free map to the same constant matrix. Let Q be the literal +polynomial product in the same order. Reduction modulo (X,Y)^2 is the alleged +endpoint, so every entry of Q has zero constant term and + +```text +Q = XI + YA + terms of total degree at least two. +``` + +The homogeneous degree-n part of det(Q) is therefore det(XI+YA). There are +no terms of degree below n, and the coefficient of X^n is one. In particular, +det(Q) is not the zero polynomial and has exact order n at the origin. + +The rank-one determinant identity over the commutative polynomial ring gives + +```text +det(F_hat) = 1 + v^T a + X v^T b + Y v^T c. +``` + +Determinant multiplicativity expresses det(Q) as a nonzero constant from +the free maps times a product of these affine linear polynomials. None can +be identically zero. Let s be the number whose constant term is zero. +The lowest homogeneous part of their product has degree s, because a product +of nonzero polynomials over a field is nonzero. Since det(Q) has order n, +s=n. Its homogeneous degree-n part is a nonzero scalar times the product +of those n homogeneous linear factors. Hence + +```text +det(XI+YA) = c product_(i=1)^n (alpha_i X + beta_i Y), c != 0. +``` + +The coefficient of X^n forces every alpha_i to be nonzero. Substituting +X=t,Y=-1 shows that det(tI-A) splits over K. This excludes every finite +word for a nonsplit A, even with arbitrary free maps and extra paid factors. +It also proves that any realizing word has at least n paid factors. + +Lifting is essential. The determinant of the endpoint in R itself is zero +when n>=2 and would give no such condition. No equality of higher-degree +matrix entries in K[X,Y] has been assumed. + +### Sufficiency and exact cost + +A matrix over K has split characteristic polynomial exactly when it is +triangularizable over K. For completeness, choose an eigenvector, pass to +the quotient by its invariant line, and repeat. The quotient characteristic +polynomial is the original one divided by that linear factor, so induction +constructs a full invariant flag. Conversely an upper triangular matrix has +split characteristic polynomial by its diagonal. + +Choose S in GL_n(K) with T=S^-1 A S upper triangular. Let M= xI+yT and +m_j its j-th column. Define the paid factors + +```text +C_j = I + (m_j-e_j)e_j^T, j=1,...,n. +``` + +They are legal because e_j is over K. In execution order C_1,...,C_n, the +first j-1 factors leave coordinate j unchanged: their modified columns have +support only in rows at most j-1. Consequently e_j^T C_(j-1)...C_1=e_j^T. +Multiplication by C_j replaces column j of the partial product with m_j +without changing its other columns. Induction gives + +```text +C_n ... C_1 = xI+yT, +S C_n ... C_1 S^-1 = xI+yA. +``` + +This word uses exactly n paid factors. The lower bound above proves its +optimality. It is a literal matrix identity on arbitrary dirty inputs; +there are no assumed zero registers or erased inputs. + +## Executed evidence + +The standalone verifier uses only the Python standard library and imports +no predecessor executable. It compares two different criteria on every A in +its declared finite domains: a permutation expansion and root division of +the characteristic polynomial, and a constructive invariant-flag search +that never reads that polynomial. Every successful flag yields an explicit +legal paid word, checked by direct square-zero matrix multiplication and +free conjugation. + +The domains are all matrices at (q,n)=(2,2),(2,3),(3,2),(3,3),(4,2),(5,2),(7,2). +F4 uses t^2+t+1. These domains contain 23,574 matrices in total. The binary +three-role classification is exactly + +```text +352 split, reachable at cost 3; +112 nonsplit with a scalar eigenvalue, unreachable; + 48 without a scalar eigenvalue, unreachable. +``` + +The 112 rootful exclusions are additional to the predecessor's eigenvalue +obstruction. The familiar 48 count agrees with #4773; the new result is the +classification, not an independent audit of that count. All 512 binary dirty +inputs pass one nontrivial three-role upper-triangular word. Nine evaluations +of an odd-field polynomial lift check its determinant against the product +of the individual affine determinants without truncating degree-two terms. + +The nine control cases are the rootful nonsplit witness, reversed word, +three separate dropped factors, an odd-characteristic determinant sign, +the F4 multiplication law, an irreducible polynomial and a singular A with +nonsplit characteristic polynomial. These exercise different hypotheses or +failure modes. Checks use explicit exceptions and remain active under -O. +Each run emits a generated receipt binding all five package files by SHA256; +no receipt is stored or hand-written. + +## Reproduction + +From the repository root, with CPython 3.12 and no third-party dependencies: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B -W error research/split-radical-pencil/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -O -B -W error research/split-radical-pencil/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/split-radical-pencil +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/split-radical-pencil --check-source-history +``` + +Any CPython 3.12 installation may replace the local interpreter path. Expected +marker: `PASS_SPLIT_RADICAL_PENCIL binary_three_role=352/512 rootful_excluded=112 no_new_kappa`. +Both registered commands have a 120-second timeout. The current selected +source-binding orientation also passed; it is metadata orientation only. + +## Scope and implementation limits + +This classifies the particular two-generator pencils with invertible first +coefficient normalized to I. It does not classify all radical matrices, +more radical generators, higher nilpotency, restored auxiliary roles or +ring-valued right vectors/free maps. The universal claim is the written +proof; the finite checks corroborate it and do not exhaust finite words. +Independent human and formal proof-kernel review are unclaimed. Native +coefficient preparation, physical routing, restoration, precision, stock and +complete supplier costs remain unknown. Lean, Docker and the selected operator +replay were outside scope and were not run. All registered checks ran locally. + +The verifier has no recursion or subprocesses and accepts no search-size +arguments. The largest matrix has nine entries and the largest streamed +census has 19,683 matrices. Flag vectors and spans have at most 49 elements; +loops are bounded by the fixed domain, n<=3 and q<=7. Functions stay below +60 physical lines. Package receipt reads have a 128 KiB limit per file. +Managed Python allocation is a bounded deviation from fixed steady-state +allocation, including tuples and generator temporaries during arithmetic. +There is no persistent service or resource. Warning-strict normal and +optimized execution provide the available diagnostics. No repository-wide +static-analysis configuration was changed. + +## Open next questions + +1. Which pencils xB+yC with singular B are reachable? Start with a fixed + Kronecker singular block and compare its minimal indices with column + replacement words. The invertible-coefficient determinant argument no + longer gives a nonzero degree-n determinant. +2. With three or more independent square-zero generators, when is splitting + of the homogeneous determinant sufficient? Start with an invertible first + coefficient and two other coefficient matrices. Simultaneous invariant + flags can fail even if a determinant factors; an attaining word or a new + obstruction is needed. + +Structured first steps, relevance and blockers are in [TASK.json](TASK.json). +These follow-ups are not investigated here. + +## Credit, provenance and coordination + +Produced by Nick Petalas. Nick Petalas's #4773 supplies the open question, +the earlier arbitrary-role eigenvalue obstruction and its explicit first +working example. #4745 supplies the two-role square-zero classification; +#4243 supplies the common free-map convention. Wentao Li's #4099 following +#2513 supplies the right-vector alphabet, and ToikY's #4334 supplies the +shared-chart algebra context. Determinant multiplicativity, the rank-one +determinant identity and triangularization are classical. The new contribution +is their polynomial-lift application giving the exact all-role pencil +classification and exact cost. No predecessor credit line is changed. + +The formal-interface-lemma card is changed to a formal-alphabet algebraic +side result. The selected source-bound baseline replaces the card's historical +baseline as directed by current priorities. Initial baseline attempts exposed +omitted sparse files; all selected source directories were materialized before +the successful run. No scientific replay was inferred from that control. +SOURCES.json pins the original card, selected record and conceptual predecessor +README as provenance at canonical main 624de9dc66858af0945e5f8a0942488d62280d43, +priority revision 7. There are no live predecessor executable dependencies. + +Before claiming, open PRs, this account's recent PRs and claims, active +Discussions, the local reservation directory, merged PR terms and main README +terms were checked. The overlap helper reported complete remote pagination +at 19:44 UTC and incomplete sparse local-note coverage. This is search +coverage, not proof of novelty. The relevant merged package is #4773; +no currently open PR in the inspected list studies this pencil classification. + +[Advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131512). diff --git a/research/split-radical-pencil/SOURCES.json b/research/split-radical-pencil/SOURCES.json new file mode 100644 index 0000000000..1733ad619a --- /dev/null +++ b/research/split-radical-pencil/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/multirole-radical-pencil/README.md", + "usage": "provenance", + "git_blob": "3e2e9b9ae2c8211b072f0078e0a762de87f465d3", + "sha256": "4f775b02c4f10c4b5394b8520e3837738fb695d255cba56b7639bd02bd1984a1" + } + ] +} diff --git a/research/split-radical-pencil/TASK.json b/research/split-radical-pencil/TASK.json new file mode 100644 index 0000000000..9f534e37bc --- /dev/null +++ b/research/split-radical-pencil/TASK.json @@ -0,0 +1,104 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "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 reachability and paid cost of xI+yA over K[x,y]/(x,y)^2 for every field and role count.", + "scope_change_reason": "Take the explicit converse question in PR4773 instead of formalizing the historical card interface; classify this formal-alphabet family by polynomial determinant lifting.", + "bottleneck_link": "Side result: identifies a sharp obstruction and optimal words in the restricted right-vector alphabet; physical supplier costs remain unpriced.", + "budget_minutes": 60, + "stop_rule": "Stop after the first proved pencil classification and literal finite corroboration.", + "outcome": "completed", + "evidence": "Written determinant-lift necessity and triangular-word sufficiency; exhaustive finite matrix domains, literal words and nine controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which pencils xB+yC with singular B are reachable?", + "why_it_matters": "The current classification requires an invertible first coefficient.", + "first_step": "Test a fixed Kronecker singular block and its minimal indices against literal column-replacement words.", + "blocked_by": "The homogeneous determinant can vanish identically, so the present necessity test gives no complete criterion." + }, + { + "question": "With at least three independent square-zero generators, is splitting of the homogeneous determinant sufficient?", + "why_it_matters": "This tests whether determinant data classify a larger family or miss noncommuting coefficient information.", + "first_step": "Use an invertible first coefficient and two other coefficient matrices; test simultaneous flags and explicit words.", + "blocked_by": "No general attaining-word criterion is supplied here." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19131512", + "overlap_checked_utc": "2026-10-22T19:44:54Z", + "claim_type": "scoped-proof" +} diff --git a/research/split-radical-pencil/VERIFY.json b/research/split-radical-pencil/VERIFY.json new file mode 100644 index 0000000000..12d79c86ac --- /dev/null +++ b/research/split-radical-pencil/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Complete finite split/flag censuses, legal attaining words, dirty inputs and nine failure/hypothesis controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "-W", + "error", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Identical checks and file-bound receipt with assertions disabled." + } + ] +} diff --git a/research/split-radical-pencil/verify.py b/research/split-radical-pencil/verify.py new file mode 100644 index 0000000000..a90a5ffb87 --- /dev/null +++ b/research/split-radical-pencil/verify.py @@ -0,0 +1,293 @@ +#!/usr/bin/env python3 +"""Finite corroboration of the split-pencil theorem. Apache-2.0. + +Produced by Nick Petalas. This verifier imports no predecessor code. +""" + +from collections import Counter +from hashlib import sha256 +from itertools import permutations, product +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def field(q): + require(q in (2, 3, 4, 5, 7), "unsupported field") + add = tuple(tuple(a ^ b if q == 4 else (a + b) % q + for b in range(q)) for a in range(q)) + mul = [] + for a in range(q): + row = [] + for b in range(q): + c = (a * b) % q + if q == 4: + c = ((a & 1) * (b & 1)) ^ (((a & 1) * (b >> 1)) << 1) + c ^= (((a >> 1) * (b & 1)) << 1) ^ ((a >> 1) * (b >> 1) * 3) + row.append(c) + mul.append(tuple(row)) + neg = tuple(next(b for b in range(q) if add[a][b] == 0) for a in range(q)) + return add, tuple(mul), neg + + +def total(values, f): + result = 0 + for value in values: + result = f[0][result][value] + return result + + +def eye(n): + return tuple(int(i == j) for i in range(n) for j in range(n)) + + +def mm(a, b, n, f): + return tuple(total((f[1][a[i*n+k]][b[k*n+j]] for k in range(n)), f) + for i in range(n) for j in range(n)) + + +def mv(a, v, n, f): + return tuple(total((f[1][a[i*n+j]][v[j]] for j in range(n)), f) + for i in range(n)) + + +def inverse(a, n, q, f): + rows = [list(a[i*n:(i+1)*n]) + list(eye(n)[i*n:(i+1)*n]) for i in range(n)] + for col in range(n): + pivot = next((r for r in range(col, n) if rows[r][col]), None) + if pivot is None: + return None + rows[col], rows[pivot] = rows[pivot], rows[col] + inv = next(x for x in range(1, q) if f[1][rows[col][col]][x] == 1) + rows[col] = [f[1][inv][x] for x in rows[col]] + for r in range(n): + if r != col: + scale = f[2][rows[r][col]] + rows[r] = [f[0][x][f[1][scale][y]] + for x, y in zip(rows[r], rows[col], strict=True)] + return tuple(x for row in rows for x in row[n:]) + + +def poly_mul(a, b, f): + result = [0] * (len(a) + len(b) - 1) + for i, x in enumerate(a): + for j, y in enumerate(b): + result[i+j] = f[0][result[i+j]][f[1][x][y]] + return tuple(result) + + +def characteristic(a, n, f): + result = [0] * (n + 1) + for perm in permutations(range(n)): + sign = sum(perm[i] > perm[j] for i in range(n) for j in range(i+1, n)) % 2 + term = (f[2][1] if sign else 1,) + for i, j in enumerate(perm): + term = poly_mul(term, (f[2][a[i*n+j]], int(i == j)), f) + for i, value in enumerate(term): + result[i] = f[0][result[i]][value] + require(result[-1] == 1, "characteristic polynomial is not monic") + return tuple(result) + + +def evaluate(poly, value, f): + result = 0 + for coefficient in reversed(poly): + result = f[0][f[1][result][value]][coefficient] + return result + + +def splits(poly, q, f): + for root in range(q): + for _ in range(len(poly) - 1): + if len(poly) == 1 or evaluate(poly, root, f): + break + quotient = [0] * (len(poly) - 1) + quotient[-1] = poly[-1] + for i in range(len(quotient)-2, -1, -1): + quotient[i] = f[0][poly[i+1]][f[1][root][quotient[i+1]]] + require(f[0][poly[0]][f[1][root][quotient[0]]] == 0, "bad division") + poly = tuple(quotient) + return len(poly) == 1 + + +def triangular_basis(a, n, q, f): + """Build a full invariant flag, independently of characteristic().""" + vectors = tuple(product(range(q), repeat=n)) + span = {tuple(0 for _ in range(n))} + columns = [] + for _ in range(n): + chosen = None + for v in vectors: + if v in span: + continue + av = mv(a, v, n, f) + if any(tuple(f[0][av[i]][f[2][f[1][lam][v[i]]]] for i in range(n)) + in span for lam in range(q)): + chosen = v + break + if chosen is None: + return None + columns.append(chosen) + span = {tuple(f[0][w[i]][f[1][c][chosen[i]]] for i in range(n)) + for w in span for c in range(q)} + require(len(span) == q ** len(columns), "dependent flag column") + return tuple(columns[j][i] for i in range(n) for j in range(n)) + + +def ring_mm(a, b, n, f): + scalar = mm(a[0], b[0], n, f) + coefficients = [] + for k in (1, 2): + left, right = mm(a[0], b[k], n, f), mm(a[k], b[0], n, f) + coefficients.append(tuple(f[0][x][y] for x, y in zip(left, right, strict=True))) + return (scalar, *coefficients) + + +def pencil(a, n): + return (tuple(0 for _ in a), eye(n), a) + + +def attaining_word(a, basis, n, q, f): + inv = inverse(basis, n, q, f) + require(inv is not None, "singular flag basis") + t = mm(mm(inv, a, n, f), basis, n, f) + require(all(t[i*n+j] == 0 for i in range(n) for j in range(i)), "not triangular") + zero = tuple(0 for _ in a) + word = [] + for j in range(n): + scalar, xpart, ypart = list(eye(n)), list(zero), list(zero) + scalar[j*n+j] = 0 + xpart[j*n+j] = 1 + for i in range(n): + ypart[i*n+j] = t[i*n+j] + word.append((tuple(scalar), tuple(xpart), tuple(ypart))) + result = (eye(n), zero, zero) + for factor in word: + result = ring_mm(factor, result, n, f) + require(result == pencil(t, n), "column replacement word failed") + result = ring_mm((basis, zero, zero), result, n, f) + result = ring_mm(result, (inv, zero, zero), n, f) + require(result == pencil(a, n), "free conjugation failed") + return word, t + + +def census(q, n): + f = field(q) + counts = Counter() + for a in product(range(q), repeat=n*n): + poly = characteristic(a, n, f) + split = splits(poly, q, f) + basis = triangular_basis(a, n, q, f) + require(split == (basis is not None), "polynomial and flag criteria disagree") + if split: + attaining_word(a, basis, n, q, f) + counts["split"] += 1 + elif any(evaluate(poly, root, f) == 0 for root in range(q)): + counts["rootful_nonsplit"] += 1 + else: + counts["rootless"] += 1 + require(sum(counts.values()) == q ** (n*n), "incomplete census") + return dict(counts) + + +def ring_action(a, v, n, f): + return (mv(a[0], v[0], n, f), + tuple(f[0][x][y] for x, y in zip(mv(a[0], v[1], n, f), + mv(a[1], v[0], n, f), strict=True)), + tuple(f[0][x][y] for x, y in zip(mv(a[0], v[2], n, f), + mv(a[2], v[0], n, f), strict=True))) + + +def dirty_checks(): + f, n = field(2), 3 + a = (0, 1, 1, 0, 1, 1, 0, 0, 0) + word, t = attaining_word(a, eye(n), n, 2, f) + count = 0 + for entries in product(range(2), repeat=3*n): + v = tuple(tuple(entries[k*n:(k+1)*n]) for k in range(3)) + result = v + for factor in word: + result = ring_action(factor, result, n, f) + require(result == ring_action(pencil(t, n), v, n, f), "dirty action mismatch") + count += 1 + return count + + +def controls(): + f = field(2) + # Scalar block plus irreducible quadratic: a root is insufficient. + a = (0, 0, 0, 0, 0, 1, 0, 1, 1) + poly = characteristic(a, 3, f) + require(evaluate(poly, 0, f) == 0 and not splits(poly, 2, f), "rootful control") + require(triangular_basis(a, 3, 2, f) is None, "partial flag accepted") + require(poly[0] == 0 and poly == (0, 1, 1, 1), "singular A control") + # The attaining word has an essential chronological direction. + upper = (0, 1, 1, 0, 1, 1, 0, 0, 0) + word, t = attaining_word(upper, eye(3), 3, 2, f) + zero = tuple(0 for _ in upper) + reverse = (eye(3), zero, zero) + for factor in reversed(word): + reverse = ring_mm(factor, reverse, 3, f) + require(reverse != pencil(t, 3), "reversed word escaped control") + for omit in range(3): + result = (eye(3), zero, zero) + for j, factor in enumerate(word): + if j != omit: + result = ring_mm(factor, result, 3, f) + require(result != pencil(t, 3), "dropped factor escaped control") + odd = field(3) + require(characteristic((0, 1, 2, 0), 2, odd) == (1, 0, 1), "odd sign control") + extension = field(4) + require(extension[1][2][2] == 3 and extension[1][2][3] == 1, "F4 field control") + require(not splits((1, 1, 1), 2, f), "irreducible polynomial accepted") + return 9 + + +def determinant_lift_checks(): + """Evaluate full polynomial lifts, without truncating degree-two terms.""" + f, n = field(3), 3 + t = (1, 2, 1, 0, 2, 2, 0, 0, 0) + word, _ = attaining_word(t, eye(n), n, 3, f) + comparisons = 0 + for x, y in product(range(3), repeat=2): + result = eye(n) + for factor in word: + evaluated = tuple(total((factor[0][i], f[1][x][factor[1][i]], + f[1][y][factor[2][i]]), f) for i in range(n*n)) + result = mm(evaluated, result, n, f) + expected = 1 + for j in range(n): + expected = f[1][expected][f[0][x][f[1][y][t[j*n+j]]]] + actual = characteristic(result, n, f)[0] + require(f[2][actual] == expected, "lifted determinant product mismatch") + comparisons += 1 + return comparisons + + +def main(): + domains = ((2, 2), (2, 3), (3, 2), (3, 3), (4, 2), (5, 2), (7, 2)) + results = {f"q{q}_n{n}": census(q, n) for q, n in domains} + require(results["q2_n3"] == {"split": 352, "rootful_nonsplit": 112, + "rootless": 48}, "binary census changed") + dirty, control_count, lifts = dirty_checks(), controls(), determinant_lift_checks() + package = Path(__file__).resolve().parent + files = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + hashes = {} + for name in files: + with (package / name).open("rb") as stream: + raw = stream.read(128 * 1024 + 1) + require(len(raw) <= 128 * 1024, "package file too large") + hashes[name] = sha256(raw).hexdigest() + print(json.dumps({"censuses": results, "dirty_inputs": dirty, + "controls": control_count, "determinant_lifts": lifts, + "sha256": hashes}, sort_keys=True)) + print("PASS_SPLIT_RADICAL_PENCIL binary_three_role=352/512 " + "rootful_excluded=112 no_new_kappa") + + +if __name__ == "__main__": + main()