diff --git a/research/etale-tensor-determinant-image/README.md b/research/etale-tensor-determinant-image/README.md new file mode 100644 index 0000000000..0f07df6ce2 --- /dev/null +++ b/research/etale-tensor-determinant-image/README.md @@ -0,0 +1,256 @@ +# Exact determinant images of finite etale multiplication tensors + +This contribution is produced by Nick Petalas. Apache-2.0. +Independent human and formal proof-kernel review are unclaimed. + +## Result and scope + +Let K=F_q, let A be a nonzero finite etale K-algebra, and write + +\[ + A\cong\prod_{i=1}^r F_{q^{d_i}},\qquad n=\sum_i d_i. +\] + +Let t be its multiplication tensor in A* tensor A* tensor A, with the +ordinary covariant action of three general linear groups. The same statement +holds for every tensor in this GL orbit, with three independently chosen +factor bases. Let Delta(t) be the ordered determinant image of its stabilizer. + +**Theorem.** Define e=2 if q is odd and either some d_i is even or some odd +degree occurs at least twice. Define e=1 otherwise. Then + +\[ + \boxed{\Delta(t)=\{(u,v,w)\in(K^\times)^3:(uvw)^e=1\}.} +\] + +For e=1 the image has (q-1)^2 elements. For e=2 it has 2(q-1)^2 elements. +Moreover, for fixed q, a deterministic algorithm extracts e and the three +bounded monomial equations of atlas A030 from t in polynomially many field +operations, under the promise that t is in such an orbit. It does not need a +supplied multiplication basis, an invertible slice, a list of field factors, +or enumeration of the tensor stabilizer. It recovers the degrees from the +left nucleus by linear algebra and Frobenius-fixed spectral projectors. + +This is a **scoped mathematical proof**, with bounded exact computational +corroboration. It solves the promised finite etale multiplication class of +David Ganz's explicitly unproved atlas A030 in [PR #2849](https://github.com/CrocSwap/integer-mult-bounds/pull/2849). +It does not solve A030 for arbitrary tensors, recognize the promise, supply a +physical program, change the selected frontier, or prove a multiplication +bound. Global literature priority is unclaimed. The verifier's finite cases +are evidence for the implementation and the sign boundary, not a substitute +for the all-dimension proof below. + +The main first fixture is A=F3 cubed. Swapping two one-dimensional factors +has determinant -1, so the image is all eight determinant triples. For +A=F3 times F27, the degrees 1 and 3 are odd and distinct, so the image has +only four triples, those with product 1. Repeated odd factors matter even +when Frobenius has positive determinant on each individual factor. + +## Proof + +### 1. Normalize every autotopism + +Use the bilinear convention + +\[ + F(x)G(y)=H(xy),\qquad F,G,H\in\operatorname{GL}_K(A). +\] + +Set a=F(1), b=G(1). Substituting y=1 and x=1 gives +H(x)=F(x)b=aG(x). Thus multiplication by both a and b is invertible. +In a finite product of fields this says a,b are units. Put +sigma(x)=(ab)^(-1)H(x). Then + +\[ + F=L_a\sigma,\quad G=L_b\sigma,\quad H=L_{ab}\sigma. +\] + +Substitution in the autotopism identity gives +sigma(x)sigma(y)=sigma(xy), and sigma(1)=1. Invertibility makes sigma a +K-algebra automorphism. Conversely every pair of units and every such +sigma gives an autotopism by the displayed formula. This is the concrete +commutative specialization of the isotopy normalization in atlas A019; +its classical isotopy content is not claimed as new. + +For the ordinary covariant tensor action the corresponding stabilizer +triple is (F^(-T),G^(-T),H). Indeed the transformed bilinear map is +H times mu(F^(-1)x,G^(-1)y), which equals mu(x,y). Therefore, writing +N(a)=det L_a and delta=det sigma, the determinant triple is + +\[ + (N(a)^{-1}\delta^{-1},\ N(b)^{-1}\delta^{-1},\ N(a)N(b)\delta). +\] + +Its product is delta^(-1). This inverse-input convention is necessary; +the three determinants of a bilinear autotopism are not the three +covariant tensor determinants. + +### 2. Determine the automorphism signs and attain every allowed triple + +A K-algebra automorphism permutes the primitive field idempotents, preserves +their degrees, and on each field is a power of Frobenius after a field +identification. Conversely all such choices are automorphisms. + +On F_(q^d), the normal basis theorem makes Frobenius a d-cycle on a K-basis. +Its determinant is (-1)^(d-1). A transposition of two degree-d factors has +determinant (-1)^d: choose matching bases and exchange the d basis pairs. +These operations generate the automorphism group. Consequently every +algebra automorphism has determinant in {1,-1}. In odd characteristic a +negative determinant occurs precisely if a degree is even, or an odd +degree is repeated. If all degrees are distinct and odd, no factor can +be permuted and every Frobenius power has determinant 1. In characteristic +two all these signs equal 1. + +The norm N:A^times -> K^times is onto. For a field factor it is +z -> z^((q^d-1)/(q-1)), onto the order-(q-1) subgroup of its cyclic unit +group; take 1 in the other factors. This is a classical finite-field norm +fact. Fix an automorphism of determinant delta. The two independently +surjective norms in the formula of section 1 realize every nonzero triple +whose product is delta^(-1). Thus the complete image is precisely the +inverse automorphism-sign image in the product coordinate. Signs are their +own inverses, proving the formula and its cardinalities. + +For normal bases and the elementary finite-field facts, see J. S. Milne, +[Fields and Galois Theory](https://www.jmilne.org/math/Books/FT0.pdf), +sections on finite fields and the normal basis theorem. These are cited +classical premises; the contribution is the exact determinant-image +criterion and its extraction at this tensor interface. + +### 3. Recover the algebra without finding an invertible slice + +Given t as a bilinear map nu:U times V -> W, solve the linear equations + +\[ + \mathcal N_L(\nu)=\{(X,Y)\in\operatorname{End}(U)\oplus + \operatorname{End}(W):\nu(Xu,v)=Y\nu(u,v)\ \forall u,v\}. +\] + +There are 2n^2 unknowns and n^3 scalar equations. For canonical +multiplication, substituting v=1 gives X=Y, and then u=1 gives +X(v)=X(1)v. Hence this nucleus consists exactly of (L_a,L_a), a in A. +If nu(u,v)=R mu(P^(-1)u,Q^(-1)v), its nucleus is + +\[ + \{(P L_aP^{-1},\ R L_aR^{-1}):a\in A\}. +\] + +This follows by substitution in the defining equations in both directions. +Projection to Y is faithful. The projected matrix algebra B is therefore +isomorphic to A and is the regular representation on W up to conjugacy. +It can be computed by Gaussian elimination, without knowing P,Q,R or A. + +Compute the K-linear map Phi:B -> B, z -> z^q. It is linear because B is +commutative of characteristic p and scalar coefficients satisfy c^q=c. +Its fixed algebra C is isomorphic to K^r: each finite-field factor has +exactly K as its Frobenius fixed field. Compute a basis c_1,...,c_r of C. + +Starting with the idempotent 1, refine each current nonzero idempotent h, +for every basis vector c_j and every lambda in K, by the nonzero matrices + +\[ + h\bigl(1-(c_j-\lambda 1)^{q-1}\bigr). +\] + +In C=K^r, this is the coordinatewise indicator of the coordinates where +c_j=lambda, restricted to h. Each round is an orthogonal idempotent +partition. The final partition consists of all primitive idempotents: +if two coordinates agreed on every basis vector, they would agree on +all of K^r, contradicting the coordinate indicator vectors. The rank of +each resulting matrix on W is its field degree d_i, since B acts in the +regular representation. This proves that the degree multiset is recovered +intrinsically from t. + +The linear systems and matrix products have polynomial size. There are +at most n basis vectors, at most n current pieces, and q scalars per +refinement. Exponentiation takes O(log q) matrix products. For fixed q, +these operations and the rank computations are polynomial in n. No loop +ranges over q^n algebra elements or over automorphisms. Return the exponent +row (e,e,e), reduced modulo q-1, and two zero rows. These are three bounded +monomial equations in atlas A029/A030's convention. If q=2 the modulus is +one and all rows are zero. If q=3 and e=2 the returned first row is also +zero, correctly giving the full determinant group. + +## Exact finite evidence and reproduction + +From the repository root, use CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/etale-tensor-determinant-image/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/etale-tensor-determinant-image/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/etale-tensor-determinant-image +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/etale-tensor-determinant-image --check-source-history +``` + +For another machine replace the absolute interpreter prefix by its CPython +3.12 executable. The expected verifier status is +`PASS_ETALE_TENSOR_DETERMINANT_IMAGE`. Each run prints a generated JSON +receipt with its interpreter version, exact finite results and SHA-256 +hashes of the five package files. No receipt is handwritten and no output +is written into the checkout. + +The verifier constructs twelve literal product-algebra tables over F2, +F3 and F5, through dimension six. It recovers degrees both in the original +charts and after three independent factor changes, and explicitly realizes +every predicted determinant triple using literal unit and automorphism +matrices. The cubic and quadratic fixture polynomials are checked to have +no base-field root, which proves their irreducibility in these degrees. +For dimensions at most two, and dimension three over F2, it independently +loops over every invertible input-map pair, derives the only possible +output map from the unit, and tests every basis product. These are actual +complete stabilizer censuses on their named finite domains. No predecessor +program or census is replayed. + +Controls distinguish a missing repeated-odd-factor sign, a missing +even-degree Frobenius sign, a spurious sign for distinct odd factors, +a repeated cubic factor, a singular matrix, a matrix outside the computed algebra, a zero tensor +with the wrong nucleus dimension and the inverse-input determinant +convention. Checks remain active under optimized Python. + +## Provenance and limitations + +The exact base is ff3cc58e370d0f678e529246f8c73e8094e18fcf. `SOURCES.json` +pins the atlas statements and credit as provenance, along with the task +catalogue and selected record. They are not executable inputs. The current +selected conditional kappa remains 0.00302015. + +Credit David Ganz's atlas PR #2849 for A030's explicit extraction question, +A019's normalization and A029's bounded character-table framework. The +atlas retains the tensor and stabilizer lineage, including the classical +Chen, Grochow, Qiao, Tang and Zhang tensor-action context. Finite-field +cyclicity, norms, normal bases, primitive idempotents and Gaussian +elimination retain their classical credit. The all-tensor proposal and +other contributors' results are cited premises or context, not audit +deliverables. This package claims no global first discovery. + +The algorithm is a promise algorithm, not a recognition algorithm. The +proof covers every finite base field; the executable fixtures use only +prime fields 2, 3 and 5. No proof assistant, arbitrary-tensor solver, +physical supplier, full selected replay, recursive compiler, precision, +hosting or complete multiplication theorem was run or established. + +The verifier has no recursion or external process. All loops have finite +bounds from twelve fixed fixtures, p<=5, n<=6, at most 20,000 candidate +matrices and at most 250,000 input-map pairs per census. All functions +are kept within roughly one page. Its checks use explicit exceptions, +so optimization cannot erase the contracts. For Power of Ten rule 3, +Python's managed integers, tuples and elimination rows allocate during +execution. The bounded fixture domain and bounded collections compensate +for that runtime requirement; the script releases its memory on exit. +Moving to a general input CLI would require a separate input and memory +budget. Warning-strict normal/optimized replay is the available diagnostic +check; no separate static analyzer is required by this package. + +## Open next questions + +- Can this extraction extend to multiplication in finite local commutative + algebras with nilpotents? The unit norms and automorphism determinants + may have additional power restrictions. Start with K[z]/(z^m), deriving + the exact determinant characters before combining factors. The etale + Frobenius-fixed splitting proof does not apply to that class. +- Can an arbitrary tensor be recognized as isotopic to finite etale + multiplication in deterministic polynomial time at fixed q, with a + transporter witness? Start from the computed left nucleus and test its + regular action and compatibility with the second input. The present + theorem assumes that promise and does not supply recognition. + +Structured versions of these questions are in `TASK.json`. diff --git a/research/etale-tensor-determinant-image/SOURCES.json b/research/etale-tensor-determinant-image/SOURCES.json new file mode 100644 index 0000000000..7ad46b5298 --- /dev/null +++ b/research/etale-tensor-determinant-image/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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" + } + ] +} diff --git a/research/etale-tensor-determinant-image/TASK.json b/research/etale-tensor-determinant-image/TASK.json new file mode 100644 index 0000000000..31b604a3a8 --- /dev/null +++ b/research/etale-tensor-determinant-image/TASK.json @@ -0,0 +1,101 @@ +{ + "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 fixed-field polynomial extraction for tensors isotopic to finite etale algebra multiplication.", + "scope_change_reason": "The card suggests formalizing or auditing a selected caller. This contribution instead proves the explicitly open A030 promised tensor-class interface in David Ganz PR2849, without auditing a predecessor or claiming formalization.", + "bottleneck_link": "Algebraic side result for the tensor/stabilizer interface. It removes automorphism enumeration for this promised class; it is not a physical supplier or a change to the selected recursive bill.", + "budget_minutes": 60, + "stop_rule": "Stop after the first exact original determinant-image formula and a verified extraction procedure; leave recognition and nilpotents as open questions.", + "outcome": "completed", + "evidence": "README.md proves the all-finite-field theorem. verify.py supplies twelve exact fixtures, intrinsic recovery before and after independent charts, exhaustive small stabilizer domains, and controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can determinant-image extraction extend to multiplication in finite local commutative algebras with nilpotents?", + "why_it_matters": "This would enlarge the promised tensor class beyond finite etale algebras.", + "first_step": "Derive the exact unit and automorphism determinant characters of K[z]/(z^m).", + "blocked_by": "The Frobenius-fixed primitive-idempotent argument does not handle the nilpotent directions." + }, + { + "question": "Can the finite etale multiplication orbit promise be recognized with a transporter in deterministic polynomial time for fixed q?", + "why_it_matters": "Recognition would turn the promise algorithm into a wider tensor interface.", + "first_step": "Test the computed left nucleus for regular action and compatibility with the second input.", + "blocked_by": "This package assumes orbit membership and supplies no recognition or transporter construction." + } + ] +} diff --git a/research/etale-tensor-determinant-image/VERIFY.json b/research/etale-tensor-determinant-image/VERIFY.json new file mode 100644 index 0000000000..7fc786e930 --- /dev/null +++ b/research/etale-tensor-determinant-image/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Twelve finite etale algebra fixtures; chart-invariant nucleus/Frobenius extraction; explicit determinant-image attainment; seven exhaustive stabilizer domains; rejecting controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same exact finite domains with Python optimization, preserving explicit runtime checks." + } + ] +} diff --git a/research/etale-tensor-determinant-image/verify.py b/research/etale-tensor-determinant-image/verify.py new file mode 100644 index 0000000000..9cff778e7e --- /dev/null +++ b/research/etale-tensor-determinant-image/verify.py @@ -0,0 +1,377 @@ +"""Exact finite controls for the finite-etale determinant-image theorem. + +No dependencies, predecessor-code imports, network access, or file writes. +The all-dimension claim is the written proof, not this bounded enumeration. +""" + +import hashlib +import itertools +import json +from pathlib import Path +import sys + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def identity(n): + return tuple(tuple(int(i == j) for j in range(n)) for i in range(n)) + + +def add(a, b, p, scale=1): + return tuple(tuple((x + scale * y) % p for x, y in zip(ar, br)) + for ar, br in zip(a, b)) + + +def multiply(a, b, p): + n = len(a) + return tuple(tuple(sum(a[i][k] * b[k][j] for k in range(n)) % p + for j in range(n)) for i in range(n)) + + +def power(a, exponent, p): + result = identity(len(a)) + for bit in range(exponent.bit_length()): + if (exponent >> bit) & 1: + result = multiply(result, a, p) + a = multiply(a, a, p) + return result + + +def rref(rows, p): + rows = [list(row) for row in rows] + pivots = [] + height, width = len(rows), len(rows[0]) + for column in range(width): + candidates = [i for i in range(len(pivots), height) if rows[i][column]] + if not candidates: + continue + pivot = len(pivots) + other = candidates[0] + rows[pivot], rows[other] = rows[other], rows[pivot] + inv = pow(rows[pivot][column], -1, p) + rows[pivot] = [(x * inv) % p for x in rows[pivot]] + for i in range(height): + if i != pivot and rows[i][column]: + factor = rows[i][column] + rows[i] = [(x - factor * y) % p + for x, y in zip(rows[i], rows[pivot])] + pivots.append(column) + if len(pivots) == height: + break + return rows, pivots + + +def nullspace(rows, p): + reduced, pivots = rref(rows, p) + width = len(rows[0]) + basis = [] + for column in range(width): + if column in pivots: + continue + vector = [0] * width + vector[column] = 1 + for i, pivot in enumerate(pivots): + vector[pivot] = -reduced[i][column] % p + basis.append(tuple(vector)) + return basis + + +def determinant(a, p): + rows = [list(row) for row in a] + value, n = 1, len(a) + for column in range(n): + candidates = [i for i in range(column, n) if rows[i][column]] + if not candidates: + return 0 + other = candidates[0] + if other != column: + rows[column], rows[other] = rows[other], rows[column] + value = -value + pivot = rows[column][column] + value = value * pivot % p + for i in range(column + 1, n): + factor = rows[i][column] * pow(pivot, -1, p) % p + rows[i] = [(x - factor * y) % p + for x, y in zip(rows[i], rows[column])] + return value % p + + +def linear_combination(matrices, coefficients, p): + result = tuple(tuple(0 for _ in matrices[0]) for _ in matrices[0]) + for matrix, coefficient in zip(matrices, coefficients): + result = add(result, matrix, p, coefficient) + return result + + +def coordinates(matrices, target, p): + n, count = len(target), len(matrices) + rows = [[matrix[i][j] for matrix in matrices] + [target[i][j]] + for i in range(n) for j in range(n)] + reduced, pivots = rref(rows, p) + require(pivots == list(range(count)), "matrix outside the algebra") + return tuple(reduced[i][-1] for i in range(count)) + + +def bilinear(table, x, y, p): + n = len(table) + return tuple(sum(x[i] * y[j] * table[i][j][k] + for i in range(n) for j in range(n)) % p + for k in range(n)) + + +def apply(a, x, p): + return tuple(sum(v * w for v, w in zip(row, x)) % p for row in a) + + +def columns(a): + return tuple(zip(*a)) + + +def algebra_table(p, polynomials): + degrees = [len(f) - 1 for f in polynomials] + n, table, offset = sum(degrees), [], 0 + blocks = [] + for f, degree in zip(polynomials, degrees): + blocks.append((offset, degree, f)) + offset += degree + for i in range(n): + row = [] + for j in range(n): + vector = [0] * n + for start, degree, f in blocks: + if start <= i < start + degree and start <= j < start + degree: + monomial = [0] * (2 * degree - 1) + monomial[i + j - 2 * start] = 1 + for k in range(2 * degree - 2, degree - 1, -1): + coefficient = monomial[k] + for t in range(degree): + monomial[k - degree + t] -= coefficient * f[t] + vector[start:start + degree] = [x % p for x in monomial[:degree]] + row.append(tuple(vector)) + table.append(tuple(row)) + return tuple(table) + + +def change_bases(table, p): + n = len(table) + left, right = [list(r) for r in identity(n)], [list(r) for r in identity(n)] + if n > 1: + left[0][1], right[1][0] = 1, 1 + output = tuple(tuple((p - 1) * int(j == (i + 1) % n) % p + for j in range(n)) for i in range(n)) + lc, rc = columns(left), columns(right) + require(all(determinant(a, p) for a in (left, right, output)), "singular chart") + return tuple(tuple(apply(output, bilinear(table, x, y, p), p) + for y in rc) for x in lc) + + +def left_nucleus(table, p): + n, rows = len(table), [] + for i, j, k in itertools.product(range(n), repeat=3): + row = [0] * (2 * n * n) + for ell in range(n): + row[ell * n + i] += table[ell][j][k] + row[n * n + k * n + ell] -= table[i][j][ell] + rows.append([x % p for x in row]) + solutions = nullspace(rows, p) + matrices = [tuple(tuple(v[n * n + i * n + j] for j in range(n)) + for i in range(n)) for v in solutions] + require(len(matrices) == n, "wrong promised nucleus dimension") + require(len(rref([sum(m, ()) for m in matrices], p)[1]) == n, + "output projection is not faithful") + for a, b in itertools.product(matrices, repeat=2): + require(multiply(a, b, p) == multiply(b, a, p), "noncommutative nucleus") + return matrices + + +def extract_degrees(table, p): + algebra, n = left_nucleus(table, p), len(table) + frobenius_columns = [coordinates(algebra, power(a, p, p), p) for a in algebra] + frobenius = tuple(zip(*frobenius_columns)) + fixed_coefficients = nullspace(add(frobenius, identity(n), p, -1), p) + fixed = [linear_combination(algebra, v, p) for v in fixed_coefficients] + pieces = [identity(n)] + for c in fixed: + refined = [] + for e in pieces: + for scalar in range(p): + projector = add(identity(n), power(add(c, identity(n), p, -scalar), + p - 1, p), p, -1) + piece = multiply(e, projector, p) + if any(sum(piece, ())): + require(multiply(piece, piece, p) == piece, "not an idempotent") + refined.append(piece) + pieces = refined + require(len(pieces) <= n, "too many spectral pieces") + require(len(pieces) == len(fixed), "fixed algebra was not fully split") + require(linear_combination(pieces, [1] * len(pieces), p) == identity(n), + "incomplete idempotent partition") + degrees = sorted(len(rref(e, p)[1]) for e in pieces) + require(sum(degrees) == n, "wrong total degree") + return degrees + + +def predicted_image(p, degrees): + negative = p != 2 and (any(d % 2 == 0 for d in degrees) + or len(set(degrees)) != len(degrees)) + signs = {1, p - 1} if negative else {1} + return {(a, b, c) for a, b, c in itertools.product(range(1, p), repeat=3) + if a * b * c % p in signs} + + +def is_autotopism(table, f, g, h, p): + basis, n = columns(identity(len(table))), len(table) + return all(bilinear(table, apply(f, basis[i], p), apply(g, basis[j], p), p) + == apply(h, table[i][j], p) + for i in range(n) for j in range(n)) + + +def all_invertible(n, p): + require(n <= 3 and p ** (n * n) <= 20000, "matrix census exceeds bound") + result = [] + for entries in itertools.product(range(p), repeat=n * n): + matrix = tuple(tuple(entries[i * n + j] for j in range(n)) for i in range(n)) + if determinant(matrix, p): + result.append(matrix) + return result + + +def direct_autotopisms(table, p, unit): + n, image, count = len(table), set(), 0 + matrices = all_invertible(n, p) + require(len(matrices) ** 2 <= 250000, "autotopism census exceeds bound") + for f, g in itertools.product(matrices, repeat=2): + b = apply(g, unit, p) + h = tuple(zip(*(bilinear(table, apply(f, x, p), b, p) + for x in columns(identity(n))))) + if determinant(h, p) and is_autotopism(table, f, g, h, p): + count += 1 + image.add((pow(determinant(f, p), -1, p), + pow(determinant(g, p), -1, p), determinant(h, p))) + return image, count, len(matrices) ** 2 + + +def explicit_witnesses(table, p, polynomials): + n, norm_representatives = len(table), {} + for vector in itertools.product(range(p), repeat=n): + matrix = tuple(zip(*(bilinear(table, vector, x, p) + for x in columns(identity(n))))) + norm = determinant(matrix, p) + if norm and norm not in norm_representatives: + norm_representatives[norm] = matrix + require(set(norm_representatives) == set(range(1, p)), "norm is not onto") + automorphisms, start = [identity(n)], 0 + blocks = [] + for polynomial in polynomials: + degree = len(polynomial) - 1 + blocks.append((start, degree, polynomial)) + matrix = [list(row) for row in identity(n)] + for j in range(start, start + degree): + vector = tuple(int(i == j) for i in range(n)) + value = vector + for _ in range(p - 1): + value = bilinear(table, value, vector, p) + for i in range(n): + matrix[i][j] = value[i] + automorphisms.append(tuple(tuple(row) for row in matrix)) + start += degree + for (a, d, fa), (b, e, fb) in itertools.combinations(blocks, 2): + if d == e: + require(fa == fb, "fixture needs an explicit factor isomorphism") + permutation = list(range(n)) + permutation[a:a + d], permutation[b:b + d] = range(b, b + d), range(a, a + d) + automorphisms.append(tuple(tuple(int(i == permutation[j]) for j in range(n)) + for i in range(n))) + image = set() + for sigma in automorphisms: + require(is_autotopism(table, sigma, sigma, sigma, p), "bad automorphism") + for ma, mb in itertools.product(norm_representatives.values(), repeat=2): + f, g = multiply(ma, sigma, p), multiply(mb, sigma, p) + h = multiply(multiply(ma, mb, p), sigma, p) + require(is_autotopism(table, f, g, h, p), "bad unit witness") + image.add((pow(determinant(f, p), -1, p), + pow(determinant(g, p), -1, p), determinant(h, p))) + return image + + +def check_controls(): + require((1, 1, 2) in predicted_image(3, [1, 1, 1]), "missed odd factor swap") + require((1, 1, 2) in predicted_image(3, [2]), "missed even-degree Frobenius") + require((1, 1, 2) not in predicted_image(3, [1, 3]), "spurious negative sign") + require((1, 1, 2) in predicted_image(3, [3, 3]), "missed repeated odd degree") + bad = [list(row) for row in identity(2)] + bad[0][0] = 0 + require(determinant(bad, 3) == 0, "singular matrix control failed") + try: + coordinates([identity(2)], ((1, 1), (0, 1)), 3) + except ValueError: + pass + else: + raise ValueError("outside-algebra control accepted") + zero_table = tuple(tuple((0, 0) for _ in range(2)) for _ in range(2)) + try: + left_nucleus(zero_table, 3) + except ValueError: + pass + else: + raise ValueError("wrong-nucleus-dimension control accepted") + scalar_table = algebra_table(5, ((0, 1),)) + require(is_autotopism(scalar_table, ((2,),), ((1,),), ((2,),), 5), + "scalar autotopism control failed") + scalar_image = predicted_image(5, [1]) + require((3, 1, 2) in scalar_image and (2, 1, 2) not in scalar_image, + "inverse-input determinant convention lost") + + +def main(): + # Constant-first monic irreducibles; degrees two and three have no base-field root. + linear, f2quad, f2cube = (0, 1), (1, 1, 1), (1, 1, 0, 1) + f3quad, f3cube, f5quad = (1, 0, 1), (1, 2, 0, 1), (2, 0, 1) + fixtures = [(3, (linear,) * 3), (3, (f3cube,)), + (3, (linear, f3quad)), (3, (linear, f3cube)), + (3, (f3cube, f3cube)), (2, (linear,) * 3), + (2, (f2cube,)), (2, (f2quad,)), + (3, (linear, linear)), (3, (f3quad,)), + (5, (linear, linear)), (5, (f5quad,))] + results, censuses = [], [] + for p, polynomials in fixtures: + require(p in (2, 3, 5) and sum(len(f) - 1 for f in polynomials) <= 6, + "fixture outside finite bounds") + for f in polynomials: + if len(f) > 2: + require(all(sum(c * x ** i for i, c in enumerate(f)) % p + for x in range(p)), "fixture polynomial has a root") + table = algebra_table(p, polynomials) + degrees = sorted(len(f) - 1 for f in polynomials) + require(extract_degrees(table, p) == degrees, "wrong intrinsic factor degrees") + require(extract_degrees(change_bases(table, p), p) == degrees, + "factor degrees depend on tensor charts") + image = predicted_image(p, degrees) + require(explicit_witnesses(table, p, polynomials) == image, "image not attained") + results.append({"p": p, "degrees": degrees, "image_size": len(image)}) + if len(table) <= 2 or (p == 2 and len(table) == 3): + unit, offset = [0] * len(table), 0 + for polynomial in polynomials: + unit[offset] = 1 + offset += len(polynomial) - 1 + actual, count, pairs = direct_autotopisms(table, p, tuple(unit)) + require(actual == image, "direct stabilizer image disagrees") + censuses.append({"p": p, "degrees": degrees, "autotopisms": count, + "candidate_input_pairs": pairs}) + check_controls() + package = Path(__file__).resolve().parent + hashes = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py")} + print(json.dumps({"status": "PASS_ETALE_TENSOR_DETERMINANT_IMAGE", + "python": sys.version.split()[0], "fixtures": results, + "direct_censuses": censuses, "control_groups": 8, + "candidate_input_pairs": sum(c["candidate_input_pairs"] for c in censuses), + "accepted_autotopisms": sum(c["autotopisms"] for c in censuses), + "source_sha256": hashes}, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()