diff --git a/research/pencil-determinant-image/README.md b/research/pencil-determinant-image/README.md new file mode 100644 index 0000000000..20f8262d37 --- /dev/null +++ b/research/pencil-determinant-image/README.md @@ -0,0 +1,221 @@ +# Exact determinant images for invertible-slice matrix pencils + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Claim type: scoped written proof with exact finite corroboration.** +For every fixed finite field, the stabilizer determinant image of a square +matrix-pencil tensor with an invertible slice has an explicit formula and a +deterministic polynomial-time extraction algorithm. This settles that subclass +of David Ganz's [atlas A030](../pure-math-atlas-400/volumes/01-algebra.md#a030), +from [PR #2849](https://github.com/CrocSwap/integer-mult-bounds/pull/2849). +The general arbitrary-tensor proposal remains open. No new kappa, physical +supplier, selected-frontier change or complete multiplication theorem is claimed. +Global literature priority is unclaimed. + +The new step is the complete determinant-coset assembly over the slice actions, +including the similarity witness's determinant. Frobenius canonical forms, +centralizer structure and the atlas's character compression are predecessors. +The centralizer identity below is classical; it is not claimed as a new theorem +or offered as an audit of its authors. + +## Convention and theorem + +Let K=F_q, n>=1 and M in Mat_n(K). The tensor has ordered matrix slices (I,M), +with action + +```text +(P,Q,R): (I,M) -> (P(aI+bM)Q^T, P(cI+dM)Q^T), +R = [[a,b],[c,d]] in GL_2(K), P,Q in GL_n(K). +``` + +Write Delta_M for the image of its stabilizer under +`(P,Q,R) -> (det P, det Q, det R)`. +For each monic irreducible f, write the K[t]-module associated to M as + +```text +V_f = direct sum over e>=1 of (K[t]/f^e)^(m_f,e). +g = gcd(q-1, every e for which some m_f,e > 0). +H = {x^g : x in K*}. +``` + +For each R in GL_2(K), put B_R=aI+bM. Retain R precisely when B_R is invertible +and `N_R=(cI+dM) B_R^-1` is similar to M. Choose any P_R such that +`P_R N_R P_R^-1=M`, and set z_R=det P_R and b_R=det B_R. Then + +```text +Delta_M = union over retained R of + {(z_R h, (b_R z_R h)^-1, det R) : h in H}. (1) +``` + +Every triple on the right occurs, and no others occur. The answer is independent +of the choices of P_R. Scalar M and linearly dependent slices are included. +If an invertible slice exists but is not first, a search of the q+1 slice +directions finds one and a GL_2 action puts it first. For slices (A0,A1) with +A0 invertible, use M=A0^-1 A1. Normalization +is a GL tensor action. Conjugation of the stabilizer preserves each determinant, +so (1) gives the same determinant image in the original coordinates. + +## Proof + +The first stabilizer equation forces B_R invertible and +`Q^T=B_R^-1 P^-1`. Substitution into the second gives +`P N_R P^-1=M`. Conversely those two conditions and that definition of Q satisfy +both original equations. Thus retained R are exactly the feasible slice actions. +All admissible P for one retained R are `C P_R`, where C is an invertible +centralizer of M. Their determinants are exactly `z_R det(C)`. Taking the +determinant of the forced Q gives the second entry of (1). + +It remains to identify `det(C_GL_n(K)(M))` as H. Here are the module details, +including nonsplit primary factors. Distinct f-primary summands have no +intertwiners, by Bezout's identity, so their determinants multiply independently. +Fix f of degree d, put E=K[t]/f, and filter V_f by powers of f. Each quotient +`f^(k-1)V_f/f^k V_f` is an E-vector space with one group of m_f,e coordinates +for each e>=k. An intertwiner from a length-s summand to a length-e summand +has image divisible by `f^max(e-s,0)`. Consequently its induced matrix on +that quotient is triangular when the summands are ordered by length. Its +exact-length-e diagonal matrix U_f,e over E is the same on every layer k<=e. +Invertibility forces every U_f,e invertible. Multiplicativity of determinant +along this invariant filtration therefore gives + +```text +det_K C = product over f,e of Norm_(E/K)(det_E U_f,e)^e. (2) +``` + +For the reverse inclusion, choose one copy of K[t]/f^e and multiply it by any +unit lifting u in E*. This commutes with M, fixes the other copies, and has +K-determinant `Norm_(E/K)(u)^e`. The norm on finite fields is surjective: on +cyclic E* it is the power `(q^d-1)/(q-1)`, with image of order q-1. Hence the +centralizer determinant image contains every e-th power in K*. Equation (2) +gives the reverse containment in the subgroup generated by those powers. +Cyclicity of K* identifies that subgroup with H. This proves (1) and its +attainment statement. A different P_R differs by a centralizer element, so +it changes z_R only by an element of H. + +The Jordan/Weyr version of (2) is classical. See Josep Ferrer, David Mingueza +and M. Eulalia Montoro, *Determinant of any matrix that belongs to Z(J)*, +[EACA 2014, Theorem 4.3, printed pages 111-114](https://www.maia.ub.edu/~sombra/publications/EACA2014/2014_EACA_Conference_Proceedings.pdf#page=113). +The filtration above explains the finite-field norm needed here. + +## Deterministic extraction for each fixed q + +1. Compute a Frobenius form of M with its transformation matrix. This is a + deterministic polynomial-time subroutine over arbitrary fields, due to + [Arne Storjohann, FOCS 2001](https://doi.org/10.1109/SFCS.2001.959911). + The [Pernet-Storjohann primary paper, introduction](https://cs.uwaterloo.ca/~astorjoh/cpoly.pdf) + also records the deterministic result; its separate randomized large-field + algorithm is not the premise used here. +2. Squarefree-decompose each invariant-factor polynomial h of M and take the + gcd of q-1 and every multiplicity that occurs. This computes g without + irreducible factorization. Indeed those multiplicities are exactly the + elementary-divisor exponents appearing in h. Derivatives and polynomial + gcds separate unequal multiplicities. When a residual derivative vanishes, + take its characteristic-p-th root and multiply subsequent multiplicities + by p. Finite fields are perfect. Each such root lowers the positive degree, + so this procedure uses polynomially many field operations for fixed q. +3. Enumerate GL_2(K), at most q^4 matrices. Form B_R and N_R. Compare Frobenius + forms, and obtain P_R from their transformation matrices when they agree. + For `S_M^-1 M S_M = S_N^-1 N_R S_N`, take `P_R=S_M S_N^-1`. +4. Evaluate (1). At most `|GL_2(K)| |H|` triples are inserted. For fixed q + this is constant output size, independent of n. The algorithm enumerates + neither GL_n(K) nor the centralizer's units nor the tensor stabilizer. +5. If A030's equation-table output is wanted, enumerate the at most `(q-1)^3` + monomial characters and retain those equal to one on every output triple. + Their common kernel is Delta_M, by finite abelian duality. The annihilator + is generated by at most three characters, as in atlas A026/A029, so choose + a generating triple by a constant-size search and pad with zero rows. + +These steps prove deterministic polynomial time in n for each fixed q. They +make no uniform polynomial-in-log(q) claim. The general-size Frobenius and +squarefree-decomposition implementations are not supplied or benchmarked here; +they are established subroutines in this written reduction. The executable +below is an independent finite corroborator, not that polynomial-time program. + +## First discriminator and bounded evidence + +For `M=[[0,1],[0,0]]` over F3, g=2 and H={1}. The retained R have c=0 and +nonzero a,d. One may take `P_R=diag(a/d,1)`, giving z_R=a/d and b_R=a^2. +Equation (1) yields exactly + +```text +Delta_M = {(1,1,1), (2,2,2)}. +``` + +Replacing H by all of F3* or omitting z_R gives a different answer. Both are +explicit rejection controls in the verifier. + +The verifier uses no predecessor executable or external package. It enumerates +every P,Q,R literally on every 2-by-2 matrix M over F2 and F3, and compares +that determinant image with a separately implemented version of (1). + +- F2: 16 slices, 3,456 literal triples tested, 96 stabilizers. +- F3: 81 slices, 8,957,952 literal triples tested, 6,912 stabilizers. The image + sizes are 2 on 24 slices, 4 on 3 slices, and 8 on 54 slices. +- Eleven independent centralizer fixtures include repeated unequal block + lengths, coprime block-length gcd, scalar matrices, and nonsplit irreducible + degree-two blocks with exponents one and two. Their centralizer vector spaces + are enumerated exactly; the largest has 19,683 elements. + +These are finite corroboration of the written proof, not an exhaustive check +of all fields or dimensions. The centralizer checks support this new formula; +re-checking a predecessor result is not the deliverable. + +## Reproduce + +From the repository root, using CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/pencil-determinant-image/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/pencil-determinant-image/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/pencil-determinant-image +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/pencil-determinant-image --check-source-history +``` + +Any CPython 3.12 interpreter path may replace the absolute path. The direct +marker is `PASS_PENCIL_DETERMINANT_IMAGE fields=2,3 tensor_slices=97 controls=2`. +A generated JSON receipt binds the five package files and exact enumerated +results. The program writes no files, uses explicit checks that survive `-O`, +and needs no Git for direct replay. Each registered command has a 120-second +limit; local replay is below five seconds on the recorded environment. + +## Scope, engineering and credit + +The result requires a square pencil and an invertible slice over K. It does +not cover singular Kronecker blocks or regular pencils without a K-rational +invertible slice. The general arbitrary-tensor extraction proposal, transporter +height bounds and GL-to-SL compilation remain separate questions. There is no +physical access, dirty-state, routing, precision, recursive-invoice or supplier +admission result. Independent human and formal proof-kernel review are unclaimed. +No Lean build, selected cold replay or complete multiplication theorem was run. + +This package changes the formal-interface-lemma card to a mathematical tensor +side question explicitly left open in the atlas. It does not formalize a Lean +statement or resolve a selected-supplier hypothesis. Exact historical card and +source pins are in SOURCES.json; they are provenance, not live replay inputs. + +Engineering uses a fixed finite domain, pure arithmetic functions and explicit +invariant failures. Each loop has a finite bound from those fixtures; centralizer +enumeration enforces a 25,000-element cap before allocating combinations. No +function exceeds 60 lines. Python's managed allocation is a Power-of-Ten rule-3 +deviation: matrix tables have at most 81 entries per axis, module dimension is +at most five, and at most 19,683 centralizer candidates are generated one at a +time. Static inspection and both registered replays check these bounds. A future +CLI accepting general inputs must introduce explicit input/resource bounds before +reusing this finite verifier. No compiler diagnostics exist for this Python file; +warning-strict normal and optimized execution are the applicable checks. + +David Ganz retains credit for atlas A030, the determinant-image formulation, +A026/A029 and the atlas's cited tensor/stabilizer lineage. Arne Storjohann and +the cited canonical-form authors retain their algorithm credit. Ferrer, Mingueza +and Montoro retain the classical centralizer determinant credit. Only the +restricted extraction reduction and exact image assembly are claimed here. + +## Open next questions + +- Extend the determinant-image assembly to regular square pencils having no + invertible K-rational slice. The binary homogeneous elementary divisors offer + a first step; the missing issue is a coordinate-independent replacement for + B_R inverse. This would remove the rational-slice restriction. +- Handle singular Kronecker blocks and rectangular pencils. Begin with the + determinant characters of one left/right minimal-index block and its + multiplicity space. Couplings between block types and slice transformations + remain the obstruction to extending this proof. diff --git a/research/pencil-determinant-image/SOURCES.json b/research/pencil-determinant-image/SOURCES.json new file mode 100644 index 0000000000..e7ed40d041 --- /dev/null +++ b/research/pencil-determinant-image/SOURCES.json @@ -0,0 +1,44 @@ +{ + "schema_version": 1, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "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/pure-math-atlas-400/volumes/01-algebra.md", + "usage": "provenance", + "git_blob": "c3f1e94af804e35da07c3c8f61557e4b4d480c3d", + "sha256": "43aeda6c0de1cc8e64f0207fc98f2436f0e883d4d0f7183719d3e8c6e5bebfbf" + }, + { + "path": "research/pure-math-atlas-400/ATTRIBUTION.md", + "usage": "provenance", + "git_blob": "3e11aa228de6d6c7bf42b3cdc6344ed36986af33", + "sha256": "d53e93d56ae9ad488a95e71e190600b0547eed1b11e81f2bb401ff6d079a1830" + } + ], + "literature": [ + { + "authors": "Arne Storjohann", + "title": "Deterministic computation of the Frobenius form", + "url": "https://doi.org/10.1109/SFCS.2001.959911", + "usage": "Classical deterministic polynomial-time form and transformation subroutine." + }, + { + "authors": "Josep Ferrer, David Mingueza, M. Eulalia Montoro", + "title": "Determinant of any matrix that belongs to Z(J)", + "url": "https://www.maia.ub.edu/~sombra/publications/EACA2014/2014_EACA_Conference_Proceedings.pdf#page=113", + "usage": "Classical Jordan/Weyr centralizer determinant formula, Theorem 4.3." + } + ] +} diff --git a/research/pencil-determinant-image/TASK.json b/research/pencil-determinant-image/TASK.json new file mode 100644 index 0000000000..bf9df03c19 --- /dev/null +++ b/research/pencil-determinant-image/TASK.json @@ -0,0 +1,106 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "ff3cc58e370d0f678e529246f8c73e8094e18fcf", + "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 stabilizer determinant image and deterministic fixed-field extraction for square matrix pencils with an invertible slice.", + "scope_change_reason": "Take David Ganz atlas A030 invertible-slice subclass as an original mathematical side result; no Lean formalization or predecessor audit.", + "bottleneck_link": "Scoped tensor-automorphism side result; no selected supplier obligation or new kappa is claimed.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified exact image formula and independently checkable proof, or at a precise failed implication.", + "outcome": "completed", + "evidence": "README.md proof and standalone verify.py literal tensor census and source-bound generated receipt.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Extend to regular pencils without an invertible K-rational slice.", + "why_it_matters": "Removes the invertible-slice restriction on the extraction theorem.", + "first_step": "Use binary homogeneous elementary divisors to replace the B_R inverse normalization.", + "blocked_by": "No coordinate-independent determinant-coset assembly is proved here." + }, + { + "question": "Extend to singular Kronecker blocks and rectangular pencils.", + "why_it_matters": "Would cover the remaining matrix-pencil tensor classes.", + "first_step": "Compute determinant characters of a single minimal-index block and its multiplicity space.", + "blocked_by": "Interactions between block types and slice transformations." + } + ], + "environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit", + "dependencies": "CPython standard library only" + } +} diff --git a/research/pencil-determinant-image/VERIFY.json b/research/pencil-determinant-image/VERIFY.json new file mode 100644 index 0000000000..a61fe339c6 --- /dev/null +++ b/research/pencil-determinant-image/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": 120, + "checks": "Exact literal action on 97 binary/ternary matrix slices; eleven centralizer fixtures; two rejecting controls; generated file-hash receipt." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same exact finite checks with optimization enabled; no assert-dependent verification." + } + ] +} diff --git a/research/pencil-determinant-image/verify.py b/research/pencil-determinant-image/verify.py new file mode 100644 index 0000000000..cf180d14f8 --- /dev/null +++ b/research/pencil-determinant-image/verify.py @@ -0,0 +1,244 @@ +#!/usr/bin/env python3 +"""Exact bounded corroboration of the pencil determinant-image theorem.""" +from hashlib import sha256 +from itertools import product +import json +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def identity(n): + return tuple(int(i == j) for i in range(n) for j in range(n)) + + +def multiply(a, b, n, p): + return tuple(sum(a[i*n+k] * b[k*n+j] for k in range(n)) % p + for i in range(n) for j in range(n)) + + +def determinant(a, n, p): + rows = [list(a[i*n:(i+1)*n]) for i in range(n)] + answer = 1 + for col in range(n): + pivot = next((i for i in range(col, n) if rows[i][col]), None) + if pivot is None: + return 0 + if pivot != col: + rows[col], rows[pivot] = rows[pivot], rows[col] + answer = -answer + value = rows[col][col] + answer = answer * value % p + for row in range(col+1, n): + factor = rows[row][col] * pow(value, -1, p) % p + for j in range(col+1, n): + rows[row][j] = (rows[row][j] - factor*rows[col][j]) % p + return answer % p + + +def nullspace(rows, width, p): + rows = [list(row) for row in rows] + pivots = [] + for col in range(width): + pivot = next((i for i in range(len(pivots), len(rows)) + if rows[i][col]), None) + if pivot is None: + continue + at = len(pivots) + rows[at], rows[pivot] = rows[pivot], rows[at] + scale = pow(rows[at][col], -1, p) + rows[at] = [x*scale % p for x in rows[at]] + for i in range(len(rows)): + if i != at: + factor = rows[i][col] + rows[i] = [(x-factor*y) % p + for x, y in zip(rows[i], rows[at])] + pivots.append(col) + basis = [] + for free in (i for i in range(width) if i not in pivots): + vector = [0]*width + vector[free] = 1 + for i, col in enumerate(pivots): + vector[col] = -rows[i][free] % p + basis.append(tuple(vector)) + return basis + + +def centralizer_image(matrix, n, p): + units = [tuple(int(k == i) for k in range(n*n)) for i in range(n*n)] + differences = [] + for unit in units: + left = multiply(matrix, unit, n, p) + right = multiply(unit, matrix, n, p) + differences.append(tuple((x-y) % p for x, y in zip(left, right))) + equations = list(zip(*differences)) + basis = nullspace(equations, n*n, p) + require(p**len(basis) <= 25000, 'centralizer enumeration exceeds bound') + image = set() + for coefficients in product(range(p), repeat=len(basis)): + c = tuple(sum(a*v[j] for a, v in zip(coefficients, basis)) % p + for j in range(n*n)) + require(multiply(matrix, c, n, p) == multiply(c, matrix, n, p), + 'nullspace did not centralize') + value = determinant(c, n, p) + if value: + image.add(value) + return image, p**len(basis) + + +def block_diagonal(blocks): + n = sum(size for size, _ in blocks) + answer = [0]*(n*n) + offset = 0 + for size, block in blocks: + for i in range(size): + for j in range(size): + answer[(offset+i)*n+offset+j] = block[i*size+j] + offset += size + return tuple(answer) + + +def companion(coefficients, p): + n = len(coefficients)-1 + require(coefficients[-1] == 1, 'companion polynomial must be monic') + out = [0]*(n*n) + for i in range(1, n): + out[i*n+i-1] = 1 + for i in range(n): + out[i*n+n-1] = -coefficients[i] % p + return tuple(out) + + +def centralizer_fixtures(): + cases = [] + for p in (3, 5): + j2 = companion((0, 0, 1), p) + j3 = companion((0, 0, 0, 1), p) + cases.extend([(p, 2, j2, 2, 'J2'), + (p, 2, identity(2), 1, 'scalar2'), + (p, 3, j3, 3, 'J3')]) + j2 = companion((0, 0, 1), 3) + j3 = companion((0, 0, 0, 1), 3) + cases.extend([ + (3, 3, block_diagonal([(2, j2), (1, (0,))]), 1, 'J2+J1'), + (3, 4, block_diagonal([(2, j2), (2, j2)]), 2, 'J2+J2'), + (3, 5, block_diagonal([(3, j3), (2, j2)]), 1, 'J3+J2'), + (3, 2, companion((1, 0, 1), 3), 1, 'irreducible-degree2'), + (3, 4, companion((1, 0, 2, 0, 1), 3), 2, 'irreducible-square')]) + results = [] + for p, n, matrix, exponent, name in cases: + actual, count = centralizer_image(matrix, n, p) + expected = {pow(x, exponent, p) for x in range(1, p)} + require(actual == expected, f'centralizer determinant formula: {name}') + results.append([p, name, n, count, sorted(actual)]) + return results + + +def matrix_tables(p): + matrices = list(product(range(p), repeat=4)) + index = {a: i for i, a in enumerate(matrices)} + table = [[index[multiply(a, b, 2, p)] for b in matrices] for a in matrices] + determinants = [determinant(a, 2, p) for a in matrices] + group = [i for i, d in enumerate(determinants) if d] + transposes = [index[(a[0], a[2], a[1], a[3])] for a in matrices] + one = index[identity(2)] + inverses = {a: next(b for b in group if table[a][b] == one) for a in group} + return matrices, index, table, determinants, group, transposes, one, inverses + + +def signature(a, p): + scalar = a[0] if a[1] == a[2] == 0 and a[0] == a[3] else None + return (a[0]+a[3]) % p, determinant(a, 2, p), scalar + + +def predicted_image(m, data, p, enlarge=False, omit_coset=False): + matrices, index, table, dets, group, _, one, inverses = data + matrix = matrices[m] + trace, det, scalar = signature(matrix, p) + exponent = 2 if scalar is None and (trace*trace-4*det) % p == 0 else 1 + hset = {pow(x, 1 if enlarge else exponent, p) for x in range(1, p)} + image = set() + for r in group: + a, b, c, d = matrices[r] + b0 = index[tuple((a*x+b*y) % p for x, y in zip(matrices[one], matrix))] + if not dets[b0]: + continue + b1 = index[tuple((c*x+d*y) % p for x, y in zip(matrices[one], matrix))] + transformed = table[b1][inverses[b0]] + if signature(matrices[transformed], p) != signature(matrix, p): + continue + choices = [u for u in group if table[u][transformed] == table[m][u]] + require(bool(choices), 'similarity signature failed to produce intertwiner') + z = 1 if omit_coset else dets[choices[0]] + for h in hset: + first = z*h % p + second = pow(dets[b0]*first % p, -1, p) + image.add((first, second, dets[r])) + return image + + +def literal_image(m, data, p): + matrices, index, table, dets, group, transposes, one, _ = data + image = set() + stabilizers = 0 + for r in group: + a, b, c, d = matrices[r] + b0 = index[tuple((a*x+b*y) % p for x, y in zip(matrices[one], matrices[m]))] + b1 = index[tuple((c*x+d*y) % p for x, y in zip(matrices[one], matrices[m]))] + for left in group: + first, second = table[left][b0], table[left][b1] + for right in group: + qt = transposes[right] + if table[first][qt] == one and table[second][qt] == m: + image.add((dets[left], dets[right], dets[r])) + stabilizers += 1 + return image, stabilizers + + +def tensor_census(p): + data = matrix_tables(p) + matrices, index, _, _, group, _, _, _ = data + histogram = {} + stabilizer_total = 0 + exact_images = {} + for m in range(len(matrices)): + literal, count = literal_image(m, data, p) + predicted = predicted_image(m, data, p) + require(literal == predicted, f'literal tensor image mismatch: {p}, {m}') + require(bool(literal), 'identity determinant triple disappeared') + histogram[str(len(literal))] = histogram.get(str(len(literal)), 0)+1 + stabilizer_total += count + exact_images[m] = sorted(literal) + j = index[(0, 1, 0, 0)] + if p == 3: + actual = set(exact_images[j]) + require(actual == {(1, 1, 1), (2, 2, 2)}, 'first Jordan fixture') + require(predicted_image(j, data, p, enlarge=True) != actual, + 'enlarged centralizer control did not reject') + require(predicted_image(j, data, p, omit_coset=True) != actual, + 'omitted similarity determinant control did not reject') + encoded = json.dumps(exact_images, sort_keys=True, separators=(',', ':')).encode() + return {'field': p, 'matrices': len(matrices), 'group_size': len(group), + 'literal_triples': len(matrices)*len(group)**3, + 'stabilizers': stabilizer_total, 'image_size_histogram': histogram, + 'images_sha256': sha256(encoded).hexdigest()} + + +def main(): + results = {'centralizers': centralizer_fixtures(), + 'tensors': [tensor_census(p) for p in (2, 3)], + 'controls': ['enlarged-centralizer', 'omitted-similarity-coset']} + root = Path(__file__).resolve().parent + files = ('README.md', 'TASK.json', 'SOURCES.json', 'VERIFY.json', 'verify.py') + receipt = {'schema_version': 1, 'results': results, + 'source_sha256': {name: sha256((root/name).read_bytes()).hexdigest() + for name in files}} + print('PASS_PENCIL_DETERMINANT_IMAGE fields=2,3 tensor_slices=97 controls=2') + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == '__main__': + main()