From 143491876f44d2bbf83bf52ae6c9fe5e9496a03c Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 3 Nov 2026 18:26:15 +0000 Subject: [PATCH] feat(research): derive non-Frobenius tensor characters --- .../PROOF.md | 171 ++++++++ .../README.md | 147 +++++++ .../SOURCES.json | 48 +++ .../TASK.json | 70 ++++ .../VERIFY.json | 34 ++ .../verify.py | 389 ++++++++++++++++++ 6 files changed, 859 insertions(+) create mode 100644 research/nonfrobenius-rectangular-characters/PROOF.md create mode 100644 research/nonfrobenius-rectangular-characters/README.md create mode 100644 research/nonfrobenius-rectangular-characters/SOURCES.json create mode 100644 research/nonfrobenius-rectangular-characters/TASK.json create mode 100644 research/nonfrobenius-rectangular-characters/VERIFY.json create mode 100644 research/nonfrobenius-rectangular-characters/verify.py diff --git a/research/nonfrobenius-rectangular-characters/PROOF.md b/research/nonfrobenius-rectangular-characters/PROOF.md new file mode 100644 index 0000000000..ce417eaea4 --- /dev/null +++ b/research/nonfrobenius-rectangular-characters/PROOF.md @@ -0,0 +1,171 @@ +# Non-Frobenius rectangular multiplication characters + +This contribution was produced by Nick Petalas. Apache-2.0. + +The claim is a scoped written proof. Finite execution corroborates it. +Independent human and formal proof-kernel review are unclaimed. + +## Statement + +Let K = F_q have characteristic p, let d >= 2, and let n >= 2 be an integer +which is not a power of p. Set + +```text +A = K[x_1,...,x_d]/(x_1^n,...,x_d^n), +N = n^d, +E = n^(d-1) n(n-1)/2, +S = n^(d-2) n(n-1)/2, +m = q-1. +``` + +For an integer r >= 0, write H_r = {a^r : a in K*}. Define + +```text +D = H_E <(-1)^S>, +g = gcd(m,N), +h = gcd(m,E,m/2) if q is odd and S is odd, +h = gcd(m,E) otherwise. +``` + +Then D is the subgroup of K* of index h. Every K-algebra automorphism of A +has a monomial tangent matrix on the radical modulo its square. Its full +linear determinant image is exactly D. + +Let mu in A* tensor A* tensor A be multiplication. Use the ordered ordinary +covariant action of GL(A*) times GL(A*) times GL(A), without permutations or +field automorphisms of the tensor factors. The exact stabilizer determinant +image is + +```text +Delta(mu) = {(u,v,w) in (K*)^3 : vw in H_N, uw in H_N, uvw in D}. +``` + +Equivalently it is defined by the three equations + +```text +(vw)^(m/g) = 1, +(uw)^(m/g) = 1, +(uvw)^(m/h) = 1. +``` + +Its size is m^3/(g^2 h). The GL orbit of mu contains exactly g^2 h orbits +under the product of the three special linear groups. This statement is +invariant under independent changes of basis in the three tensor factors. +It supplies character equations under an orbit promise, not recognition of +that promise, a multiplication chart or a transporter. + +## 1. The tangent obstruction + +The unique maximal ideal J consists of elements of zero constant term and +is nilpotent. Every automorphism preserves J and induces an invertible map +on J/J^2. Let the linear term of the image of x_i be +ell_i = sum_j a_ij x_j. The degree-n part of the relation sigma(x_i)^n = 0 +requires ell_i^n = 0 in A, since all nonlinear terms contribute only degrees +greater than n. The defining ideal is homogeneous. + +Write n = p^a b with p not dividing b. The assumption on n means b > 1. +Put k = p^a, so 0 < k < n. In characteristic p, + +```text +(1+t)^n = (1+t^(p^a))^b, +binom(n,k) = b mod p != 0. +``` + +If a row of the tangent matrix has two nonzero entries a_ij and a_il, +the coefficient of x_j^k x_l^(n-k) in ell_i^n is +binom(n,k) a_ij^k a_il^(n-k), which is nonzero. This monomial survives in A +because both exponents are less than n. No other variable can contribute +to this particular monomial. Thus each tangent row has at most one nonzero +entry. Invertibility makes the tangent matrix monomial: exactly one nonzero +entry in each row and column. + +Conversely every invertible diagonal scaling and every permutation of the +variables preserves the relations and defines an automorphism. This proves +the exact set of possible tangent maps. The power-of-p hypothesis matters: +when n is a power of p, x_1 -> x_1+x_2 is also allowed. + +## 2. The determinant of every nonlinear lift + +The finite filtration A, J, J^2, ... is invariant under every automorphism. +In a basis ordered by total degree its matrix is block triangular. Its +diagonal blocks are the maps on the associated graded algebra. That graded +algebra is canonically the same graded quotient A. The graded map is induced +by the tangent substitution, since higher terms vanish in each degree +quotient. Therefore every automorphism has the same determinant as its +monomial tangent substitution. This covers all nonlinear lifts without +classifying or counting them. + +Scale one variable by a. Among the n^d basis monomials, each exponent +0,...,n-1 of that variable occurs n^(d-1) times. The determinant is a^E. +Independent scalings thus have image H_E. + +Swap two variables. For each of the n^(d-2) choices of the remaining +exponents, exactly binom(n,2) pairs of distinct monomials are exchanged. +The determinant of this basis permutation is (-1)^S. Every variable +permutation is a product of these swaps. Consequently all automorphism +determinants lie in D, and the literal scaling and swap automorphisms attain +every element of D. In the cyclic group K*, adding -1 to H_E adds the +exponent m/2 when that sign is nontrivial. This proves the formula for h. + +## 3. Unit determinants and covariant stabilizers + +For a in A, multiplication L_a is triangular in increasing degree with +constant diagonal a_0. It is invertible exactly when a_0 != 0, and +det L_a = a_0^N. Hence unit multiplication has exact determinant image H_N, +already attained by constant units. + +For completeness, the classical normalization of a unital commutative +algebra autotopism is included. Suppose invertible K-linear F,G,H satisfy + +```text +F(x) G(y) = H(xy) for every x,y in A. +``` + +Set a = F(1), b = G(1). Substituting 1 gives H = L_b F = L_a G, so both +L_a and L_b are invertible. Thus a and b are units. The map +sigma = L_(ab)^(-1) H fixes 1, is invertible, and preserves multiplication +by substitution in the displayed identity. Hence + +```text +F = L_a sigma, G = L_b sigma, H = L_(ab) sigma. +``` + +Conversely these maps form an autotopism for any units a,b and automorphism +sigma. No decomposition or tensor recognition algorithm is being assumed. + +The corresponding covariant tensor stabilizer is (F^(-T),G^(-T),H). +Writing x = det L_a, y = det L_b, z = det sigma gives + +```text +(u,v,w) = ((xz)^(-1), (yz)^(-1), xyz), +x,y in H_N, z in D. +``` + +This parametrization is injective, with inverse +x = vw, y = uw, z = (uvw)^(-1). It proves necessity and sufficiency of the +three conditions, the equations and the image size. Constant units and the +scaling/swap automorphisms above give actual attaining maps. + +Finally the determinant map from the product GL group onto (K*)^3 is +surjective and has the product SL group as kernel. Its orbits within the +fixed GL orbit are therefore the cosets of Delta(mu), so there are g^2 h. +Conjugating the stabilizer by an independent basis change leaves each +determinant unchanged. This proves the last two assertions. + +## Scope and predecessors + +The nilpotent-algebra question is posed in Nick Petalas's PR5252. Ali +Romman's PR5316 covers one variable, and PR5459 covers characteristic-power +cutoffs. Armin Pourshafeie's PR5656 and PR5663 extend that latter family to +split and nonsplit products. Their results are credited comparisons, not +theorems reverified here. Recent PR6578 counts the automorphisms of the +Frobenius family; the present result supplies no such count and requires a +different truncation relation. The new step is the non-Frobenius tangent +restriction and its exact scaling/permutation determinant image. The +radical filtration, binomial identity, isotopy normalization and cyclic-group +arguments are classical; no global literature-priority claim is made. + +This does not classify unequal non-Frobenius cutoffs, recognize arbitrary +tensors, price coefficient preparation or provide a physical supplier. +Native, compiler, ownership, precision/tape and analytic obligations remain. +There is no new kappa or complete multiplication theorem. diff --git a/research/nonfrobenius-rectangular-characters/README.md b/research/nonfrobenius-rectangular-characters/README.md new file mode 100644 index 0000000000..526d6a9098 --- /dev/null +++ b/research/nonfrobenius-rectangular-characters/README.md @@ -0,0 +1,147 @@ +# Exact tensor characters beyond Frobenius truncations + +This contribution was produced by Nick Petalas. Apache-2.0. + +Scoped written proof with exact finite corroboration. For every finite field +K = F_q of characteristic p, d >= 2, and n >= 2 which is not a power of p, +we determine the exact ordered covariant stabilizer determinant image for +multiplication in + +```text +A = K[x_1,...,x_d]/(x_1^n,...,x_d^n). +``` + +The new step is the monomial tangent restriction. It settles a non-Frobenius +part of the nilpotent-algebra question in [PR5252](https://github.com/CrocSwap/integer-mult-bounds/pull/5252). +[PROOF.md](PROOF.md) gives the quantified argument. This is an algebraic side +result with no new kappa or selected-frontier change. + +## Result + +Write H_r = {a^r : a in K*}, and put + +```text +N = n^d, +E = n^(d-1) n(n-1)/2, +S = n^(d-2) n(n-1)/2, +D = H_E <(-1)^S>. +``` + +Every algebra automorphism has a monomial tangent matrix, and its determinant +is the determinant of that tangent substitution on all N monomials. Nonlinear +lifts add no determinant character. The exact automorphism determinant image +is D, attained by variable scalings and swaps. + +For the multiplication tensor in A* tensor A* tensor A, + +```text +Delta = {(u,v,w) : vw in H_N, uw in H_N, uvw in D}. +``` + +Let m = q-1, g = gcd(m,N), and h = gcd(m,E), adding m/2 to the latter gcd +when q and S are both odd. Three bounded equations define Delta: + +```text +(vw)^(m/g) = (uw)^(m/g) = (uvw)^(m/h) = 1. +``` + +The image has m^3/(g^2 h) elements. The GL orbit splits into exactly g^2 h +orbits under the product SL group. Independent changes of the three bases +preserve these equations. Extracting them uses q,n,d under an explicit orbit +promise; recognition and a transporter are not supplied. + +The swap sign is necessary. For K = F3 and n = d = 2, scalar variable changes +have determinant one, but swapping x and y has determinant minus one. The +full covariant image is exactly {(1,1,1),(2,2,2)}. Omitting the swap loses +one of its two elements. For K = F7, n = 2, d = 3, swaps instead have +determinant one, and the automorphism image is the three nonzero squares. + +## Evidence and reproduction + +The self-contained standard-library verifier constructs literal quotient +rings and substitution matrices. It executes no predecessor scientific code. +Its generated report binds all six package files by SHA256. + +- Fifteen contexts, including F4 and F8, supply 138 literal attaining + automorphisms. Every basis product is checked. +- Two complete generator-image domains visit 729 pairs over F3 at n = 2 + and 65,536 pairs over F2 at n = 3. They accept 72 and 2,048 automorphisms, + respectively. Every accepted nonlinear map has monomial tangent and the + same determinant as its linear substitution. These are complete domains + for those two small algebras, not a general automorphism-count formula. +- The above checks cover 232,714 basis products. Complete small unit domains + execute 310 multiplication matrices and recover their exact determinant + images. All 3,243 determinant triples across the fifteen contexts agree + with both subgroup membership and the three equations. +- A nonlinear autotopism transforms all 64 coefficients of one literal + multiplication tensor. Using raw input maps or omitting the input + transposes changes coefficients and rejects. Five invalid checker domains + reject, and four named semantic discriminators cover the characteristic + power boundary, swap sign and determinant image. + +From the repository root, with CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/nonfrobenius-rectangular-characters/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/nonfrobenius-rectangular-characters/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/nonfrobenius-rectangular-characters +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/nonfrobenius-rectangular-characters --check-source-history +``` + +Other machines may substitute their CPython 3.12 path. The direct marker is +`PASS_NONFROBENIUS_RECTANGULAR_CHARACTERS no_new_kappa`. Checks write no files +and remain active under optimization. Receipts are emitted to stdout. + +The executable is a bounded corroborator. Literal algebra dimension is at +most 36, fields have at most 13 elements, generator-pair enumeration is +capped at 65,536 and unit enumeration at 1,024 elements. All loops are finite +and no recursion or generated code is used. Python allocates managed objects; +these enforced domain bounds replace fixed-memory allocation. The sole small +callback dispatch is the five invalid-domain controls. Every function is +shorter than 60 lines. Warning-strict normal and optimized execution are the +available Python diagnostics; no external static analyzer is required. + +## Scope and credit + +The [advance CLAIM](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19380662) +records the changed scope of the bit-new-register-model card. The original +physical-mechanism acceptance gate is unclaimed. Base is canonical main +7c49fe32c55de02c2c873655c804b16e4c3fef0a, priority revision 8, selected PR6030. +The selected source-binding positive control passed. SOURCES.json pins the +question and comparison proofs as provenance, with no external runtime input. + +Credit Nick Petalas / PR5252 for the nilpotent-algebra question and covariant +normalization precedent; Ali Romman / PR5316 for one-variable truncations and +PR5459 for characteristic-power cutoffs; Armin Pourshafeie / PR5656 and PR5663 +for their split and nonsplit product extensions; David Ganz and the retained +tensor-atlas lineage. The present main step derives the different tangent +restriction directly. No predecessor construction, count or scientific replay +is validated here. Recent PR6578 counts Frobenius-family automorphisms; its +formula and family are not extended. Radical filtrations, the binomial +identity, unital isotopy and cyclic-group facts retain classical credit. +Global literature priority is unclaimed. + +Live open/account PRs, handoff claims, active Discussions, local reservations, +main README formula/object searches and merged/general-family searches were +checked. The cached broad search covered 626 open PRs, 6,745 Discussion records +and all 8,917 committed local notes at the pinned base. These are overlap +checks, not a novelty certificate; unpublished work and arbitrary historical +code/diffs remain outside them. + +Independent human and formal proof-kernel review are unclaimed. Unequal +cutoffs, arbitrary-tensor recognition, chart recovery, coefficient preparation, +native realization, movement, dirty restoration, precision/tape, a complete +paid supplier/caller invoice and the multiplication theorem remain outside +scope. No selected cold replay, Lean or Docker build is needed or run. + +## Open next questions + +- Determine the tangent restrictions and determinant image for unequal + non-Frobenius cutoffs. Start with K[x,y]/(x^2,y^3); a complete lift argument + for those changed relations is missing. +- Recognize this promised equal-cutoff orbit and recover a multiplication + chart. Start with a unital table and its radical generators; neither a + certified recognition procedure nor a physical coefficient bill is given. + +Structured relevance, first steps and blockers are in TASK.json. Stop here; +no further construction campaign is implied by this side result. diff --git a/research/nonfrobenius-rectangular-characters/SOURCES.json b/research/nonfrobenius-rectangular-characters/SOURCES.json new file mode 100644 index 0000000000..72b9b20c78 --- /dev/null +++ b/research/nonfrobenius-rectangular-characters/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/etale-tensor-determinant-image/README.md", + "usage": "provenance", + "git_blob": "0f07df6ce2a8c43ea1fcc5f0081ee3532da28208", + "sha256": "2ec18042a1a63d5fd5da246f4f6060c5fb66cff338f25a2a1b95e3ea8b4f0fba" + }, + { + "path": "research/truncated-tensor-characters/README.md", + "usage": "provenance", + "git_blob": "9dac5ac07eb867ff2ff44bd8f033d0ac1114fb82", + "sha256": "2ebd7660dc342ea7a20c3c67dd58530b8ebf3d224ca13c5f689956338d3a32d7" + }, + { + "path": "research/frobenius-tensor-characters/README.md", + "usage": "provenance", + "git_blob": "b62f9a906e6ed49605684cca52a221f064924461", + "sha256": "31573ba91ac69caff5b8e5a42ce7fd0d80a6d54673c08d7f225c9ee08e0e0893" + }, + { + "path": "research/frobenius-product-characters/PROOF.md", + "usage": "provenance", + "git_blob": "a9f931a378ebf7a67881d209f46c2f7fe47d1041", + "sha256": "0eb6c9f9eba70dc339e54b72a98b5b0fdcef706bcff5e02546ab2d0426a85ad9" + }, + { + "path": "research/nonsplit-frobenius-characters/PROOF.md", + "usage": "provenance", + "git_blob": "66178c0eb7a23b520a63f2cd7d636dd6b57bd749", + "sha256": "dd860085f8f5b6e5d48956fa520b593a7c06fb406e0225816baf5216e3110bcf" + } + ] +} diff --git a/research/nonfrobenius-rectangular-characters/TASK.json b/research/nonfrobenius-rectangular-characters/TASK.json new file mode 100644 index 0000000000..c5439694d9 --- /dev/null +++ b/research/nonfrobenius-rectangular-characters/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Scoped algebraic proof of the monomial tangent restriction and exact ordered covariant stabilizer determinant image for multiplication in F_q[x_1,...,x_d]/(x_i^n), d>=2, n not a power of the characteristic.", + "scope_change_reason": "The assigned bit-new-register-model card is changed to an algebraic side result on the nilpotent-algebra question of PR5252. It does not meet the card physical mechanism or paid-profile acceptance gate.", + "bottleneck_link": "Algebraic side result only. It gives complete symmetry character restrictions for a new multiplication-tensor class; no physical supplier, complete bill or kappa consequence is claimed.", + "budget_minutes": 60, + "stop_rule": "Stop at the first proved non-Frobenius character formula and its bounded exact corroboration. Unequal cutoffs and recognition remain open.", + "outcome": "completed", + "evidence": "Written all-finite-field proof; 138 attaining automorphisms in 15 contexts; 66,265 complete generator-image pairs with 2,120 accepted automorphisms; 310 unit maps; 232,714 basis-product checks; 3,243 determinant triples and 64 literal tensor coefficients; rejecting domain and convention controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact determinant image for unequal cutoffs which are not characteristic powers?", + "why_it_matters": "The tangent restriction can become triangular rather than monomial, so the equal-cutoff theorem does not settle the next local-algebra family.", + "first_step": "Analyze the allowed tangent entries for K[x,y]/(x^2,y^3), then compute the filtration determinant.", + "blocked_by": "A complete tangent-map and lift argument for the changed relations." + }, + { + "question": "Can one recognize this equal non-Frobenius tensor orbit and recover a multiplication chart?", + "why_it_matters": "The current equations assume the algebra-class promise.", + "first_step": "Recover a unital multiplication table from a supplied isotopy and identify its radical generators.", + "blocked_by": "A certified recognition and chart recovery procedure; no physical coefficient or caller tariff is supplied." + } + ] +} diff --git a/research/nonfrobenius-rectangular-characters/VERIFY.json b/research/nonfrobenius-rectangular-characters/VERIFY.json new file mode 100644 index 0000000000..cde0c3f6c4 --- /dev/null +++ b/research/nonfrobenius-rectangular-characters/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": "Complete small substitution and unit domains, literal determinant and product identities, exact character image and rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete check with Python assertions optimized away; all scientific checks use explicit exceptions." + } + ] +} diff --git a/research/nonfrobenius-rectangular-characters/verify.py b/research/nonfrobenius-rectangular-characters/verify.py new file mode 100644 index 0000000000..607718312c --- /dev/null +++ b/research/nonfrobenius-rectangular-characters/verify.py @@ -0,0 +1,389 @@ +"""Exact bounded corroboration; no predecessor executable or external input.""" + +from __future__ import annotations + +import hashlib +import itertools +import json +import math +from pathlib import Path + + +def require(condition: bool, message: str) -> None: + if not condition: + raise AssertionError(message) + + +class Field: + """Small prime fields, F4 = F2[t]/(t^2+t+1), F8 = F2[t]/(t^3+t+1).""" + + def __init__(self, q: int) -> None: + if type(q) is not int or q not in (2, 3, 4, 5, 7, 8, 11, 13): + raise ValueError("unsupported finite checker field") + self.q = q + self.p = 2 if q in (4, 8) else q + self.sums = tuple(tuple(self._sum(a, b) for b in range(q)) for a in range(q)) + self.products = tuple(tuple(self._product(a, b) for b in range(q)) for a in range(q)) + self.negatives = tuple(next(b for b in range(q) if self.sums[a][b] == 0) for a in range(q)) + self.inverses = (0,) + tuple( + next(b for b in range(1, q) if self.products[a][b] == 1) + for a in range(1, q) + ) + + def _sum(self, a: int, b: int) -> int: + return a ^ b if self.q in (4, 8) else (a + b) % self.q + + def _product(self, a: int, b: int) -> int: + if self.q not in (4, 8): + return a * b % self.q + degree, modulus = (2, 0b111) if self.q == 4 else (3, 0b1011) + result = 0 + for bit in range(degree): + if (b >> bit) & 1: + result ^= a << bit + for bit in range(2 * degree - 2, degree - 1, -1): + if (result >> bit) & 1: + result ^= modulus << (bit - degree) + return result + + def add(self, a: int, b: int) -> int: + return self.sums[a][b] + + def mul(self, a: int, b: int) -> int: + return self.products[a][b] + + def power(self, a: int, exponent: int) -> int: + if not 0 <= exponent <= 1_000_000: + raise ValueError("finite exponent bound") + result = 1 + for bit in range(exponent.bit_length()): + if (exponent >> bit) & 1: + result = self.mul(result, a) + a = self.mul(a, a) + return result + + +def determinant(columns: tuple[tuple[int, ...], ...], field: Field) -> int: + size = len(columns) + require(1 <= size <= 36 and all(len(c) == size for c in columns), "matrix shape") + rows = [[columns[j][i] for j in range(size)] for i in range(size)] + result = 1 + for col in range(size): + pivot = next((i for i in range(col, size) if rows[i][col]), None) + if pivot is None: + return 0 + if pivot != col: + rows[pivot], rows[col] = rows[col], rows[pivot] + result = field.negatives[result] + value = rows[col][col] + result = field.mul(result, value) + inverse = field.inverses[value] + for i in range(col + 1, size): + scale = field.mul(rows[i][col], inverse) + if scale: + for j in range(col, size): + term = field.mul(scale, rows[col][j]) + rows[i][j] = field.add(rows[i][j], field.negatives[term]) + return result + + +class Algebra: + """The literal quotient algebra, with a bounded monomial table.""" + + def __init__(self, field: Field, n: int, d: int) -> None: + if type(n) is not int or type(d) is not int or not 2 <= n <= 6 or not 2 <= d <= 4: + raise ValueError("finite algebra parameter bound") + if n**d > 36: + raise ValueError("finite algebra dimension bound") + self.field, self.n, self.d = field, n, d + self.exponents = tuple(itertools.product(range(n), repeat=d)) + self.size = len(self.exponents) + self.index = {e: i for i, e in enumerate(self.exponents)} + self.zero = (0,) * self.size + self.one = (1,) + (0,) * (self.size - 1) + self.variables = tuple( + self.index[tuple(int(i == j) for i in range(d))] for j in range(d) + ) + self.table = tuple(tuple(self._basis_product(a, b) for b in self.exponents) for a in self.exponents) + + def _basis_product(self, a: tuple[int, ...], b: tuple[int, ...]) -> int: + exponent = tuple(x + y for x, y in zip(a, b, strict=True)) + return self.index[exponent] if max(exponent) < self.n else -1 + + def basis(self, index: int) -> tuple[int, ...]: + require(0 <= index < self.size, "basis index") + return tuple(int(i == index) for i in range(self.size)) + + def mul(self, a: tuple[int, ...], b: tuple[int, ...]) -> tuple[int, ...]: + require(len(a) == len(b) == self.size, "algebra input shape") + result = [0] * self.size + left = tuple((i, x) for i, x in enumerate(a) if x) + right = tuple((j, y) for j, y in enumerate(b) if y) + for i, x in left: + for j, y in right: + destination = self.table[i][j] + if destination >= 0: + term = self.field.mul(x, y) + result[destination] = self.field.add(result[destination], term) + return tuple(result) + + def powers(self, value: tuple[int, ...]) -> tuple[tuple[int, ...], ...]: + result = [self.one] + for _ in range(self.n): + result.append(self.mul(result[-1], value)) + return tuple(result) + + def substitution(self, images: tuple[tuple[int, ...], ...]) -> tuple[tuple[int, ...], ...]: + require(len(images) == self.d and all(v[0] == 0 for v in images), "generator images") + powers = tuple(self.powers(v) for v in images) + require(all(p[-1] == self.zero for p in powers), "truncation relation") + columns = [] + for exponent in self.exponents: + value = self.one + for i, power in enumerate(exponent): + value = self.mul(value, powers[i][power]) + columns.append(value) + return tuple(columns) + + +def is_characteristic_power(n: int, p: int) -> bool: + remainder = n + for _ in range(n.bit_length()): + if remainder % p: + break + remainder //= p + return remainder == 1 + + +def character_data(field: Field, n: int, d: int) -> dict[str, int]: + if type(n) is not int or type(d) is not int or not 2 <= n <= 1000 or not 2 <= d <= 8: + raise ValueError("finite formula parameter bound") + if is_characteristic_power(n, field.p): + raise ValueError("the theorem excludes characteristic-power truncations") + size = n**d + exponent = size * (n - 1) // 2 + swap_exponent = n ** (d - 2) * n * (n - 1) // 2 + order = field.q - 1 + sign_generator = order // 2 if field.p != 2 and swap_exponent % 2 else 0 + g = math.gcd(order, size) + h = math.gcd(order, exponent, sign_generator) + return {"N": size, "E": exponent, "S": swap_exponent, "g": g, "h": h, "SL_orbits": g * g * h} + + +def power_subgroup(field: Field, exponent: int) -> set[int]: + return {field.power(a, exponent) for a in range(1, field.q)} + + +def predicted_automorphism_image(field: Field, data: dict[str, int]) -> set[int]: + return {a for a in range(1, field.q) if field.power(a, (field.q - 1) // data["h"]) == 1} + + +def tangent_is_monomial(algebra: Algebra, images: tuple[tuple[int, ...], ...]) -> bool: + rows = tuple(tuple(v[j] for j in algebra.variables) for v in images) + return all(sum(bool(x) for x in row) == 1 for row in rows) and all( + sum(bool(rows[i][j]) for i in range(algebra.d)) == 1 for j in range(algebra.d) + ) + + +def check_homomorphism(algebra: Algebra, columns: tuple[tuple[int, ...], ...]) -> int: + checked = 0 + for i in range(algebra.size): + for j in range(algebra.size): + destination = algebra.table[i][j] + expected = algebra.zero if destination < 0 else columns[destination] + require(algebra.mul(columns[i], columns[j]) == expected, "basis-product identity") + checked += 1 + return checked + + +def linear_witnesses(algebra: Algebra) -> dict[str, object]: + field = algebra.field + data = character_data(field, algebra.n, algebra.d) + observed: set[int] = set() + products_checked = maps = 0 + for swap in (False, True): + for scalar in range(1, field.q): + images = [algebra.basis(j) for j in algebra.variables] + images[0] = tuple(field.mul(scalar, a) for a in images[0]) + if swap: + images[0], images[1] = images[1], images[0] + columns = algebra.substitution(tuple(images)) + require(tangent_is_monomial(algebra, tuple(images)), "monomial attaining tangent") + value = determinant(columns, field) + expected = field.power(scalar, data["E"]) + if swap and data["S"] % 2: + expected = field.negatives[expected] + require(value == expected and value != 0, "literal monomial determinant") + observed.add(value) + products_checked += check_homomorphism(algebra, columns) + maps += 1 + require(observed == predicted_automorphism_image(field, data), "automorphism image attainment") + return {"q": field.q, "n": algebra.n, "d": algebra.d, **data, + "maps": maps, "basis_products": products_checked, "determinants": sorted(observed)} + + +def complete_substitution_domain(q: int, n: int) -> dict[str, object]: + algebra = Algebra(Field(q), n, 2) + field = algebra.field + require(q ** (2 * (algebra.size - 1)) <= 65536, "complete census capacity") + values = tuple((0,) + tail for tail in itertools.product(range(q), repeat=algebra.size - 1)) + admissible = {v for v in values if algebra.powers(v)[-1] == algebra.zero} + observed: set[int] = set() + pairs = accepted = products_checked = 0 + for left in values: + for right in values: + pairs += 1 + if left not in admissible or right not in admissible: + continue + images = (left, right) + tangent = tuple(tuple(v[j] for j in algebra.variables) for v in images) + if determinant(tangent, field) == 0: + continue + columns = algebra.substitution(images) + value = determinant(columns, field) + require(value != 0, "invertible tangent lifts to an automorphism") + require(tangent_is_monomial(algebra, images), "complete nonlinear tangent restriction") + linear = tuple(tuple(c if sum(e) == 1 else 0 for c, e in zip(v, algebra.exponents, strict=True)) + for v in images) + require(value == determinant(algebra.substitution(linear), field), "every nonlinear lift determinant") + products_checked += check_homomorphism(algebra, columns) + observed.add(value) + accepted += 1 + require(observed == predicted_automorphism_image(field, character_data(field, n, 2)), "complete automorphism image") + return {"q": q, "n": n, "d": 2, "pairs": pairs, "automorphisms": accepted, + "basis_products": products_checked, "determinants": sorted(observed)} + + +def complete_unit_domain(q: int, n: int) -> dict[str, object]: + algebra = Algebra(Field(q), n, 2) + field = algebra.field + require(q**algebra.size <= 1024, "unit census capacity") + observed: set[int] = set() + units = 0 + for value in itertools.product(range(q), repeat=algebra.size): + if value[0] == 0: + continue + columns = tuple(algebra.mul(value, algebra.basis(i)) for i in range(algebra.size)) + actual = determinant(columns, field) + require(actual == field.power(value[0], algebra.size), "literal unit norm") + observed.add(actual) + units += 1 + require(observed == power_subgroup(field, algebra.size), "complete unit character") + return {"q": q, "n": n, "units": units, "determinants": sorted(observed)} + + +def determinant_triples(field: Field, n: int, d: int) -> dict[str, int]: + data = character_data(field, n, d) + norms = power_subgroup(field, data["N"]) + automorphisms = predicted_automorphism_image(field, data) + attained = set() + for x, y, z in itertools.product(norms, norms, automorphisms): + attained.add((field.inverses[field.mul(x, z)], field.inverses[field.mul(y, z)], + field.mul(field.mul(x, y), z))) + tested = 0 + for u, v, w in itertools.product(range(1, field.q), repeat=3): + vw, uw = field.mul(v, w), field.mul(u, w) + uvw = field.mul(u, vw) + subgroup_test = vw in norms and uw in norms and uvw in automorphisms + equation_test = (field.power(vw, (field.q - 1) // data["g"]) == 1 + and field.power(uw, (field.q - 1) // data["g"]) == 1 + and field.power(uvw, (field.q - 1) // data["h"]) == 1) + require(((u, v, w) in attained) == subgroup_test == equation_test, "three character equations") + tested += 1 + require(len(attained) * data["SL_orbits"] == (field.q - 1) ** 3, "determinant index") + return {"q": field.q, "n": n, "d": d, "tested": tested, "image_size": len(attained), + "SL_orbits": data["SL_orbits"]} + + +def literal_covariant_control() -> dict[str, int]: + """Transform every coefficient of one multiplication tensor directly.""" + algebra = Algebra(Field(7), 2, 2) + field = algebra.field + x, y = (algebra.basis(j) for j in algebra.variables) + xy = algebra.mul(x, y) + forward = tuple(field.add(a, b) for a, b in zip(x, xy, strict=True)) + backward = tuple(field.add(a, field.negatives[b]) for a, b in zip(x, xy, strict=True)) + sigma = algebra.substitution((forward, y)) + inverse = algebra.substitution((backward, y)) + # F=2 sigma, G=2 sigma, H=4 sigma; sigma(x)=x+xy, sigma(y)=y. + f_inverse_transpose = tuple(tuple(field.mul(4, inverse[i][j]) for i in range(4)) for j in range(4)) + g_inverse_transpose = f_inverse_transpose + h = tuple(tuple(field.mul(4, x) for x in column) for column in sigma) + checked = 0 + wrong = missing_transpose = 0 + for i, j, k in itertools.product(range(4), repeat=3): + actual = mistaken = untransposed = 0 + for a, b in itertools.product(range(4), repeat=2): + c = algebra.table[a][b] + if c >= 0: + term = field.mul(f_inverse_transpose[a][i], g_inverse_transpose[b][j]) + actual = field.add(actual, field.mul(term, h[c][k])) + raw = field.mul(field.mul(2, sigma[a][i]), field.mul(2, sigma[b][j])) + mistaken = field.add(mistaken, field.mul(raw, h[c][k])) + raw_inverse = field.mul(field.mul(4, inverse[a][i]), field.mul(4, inverse[b][j])) + untransposed = field.add(untransposed, field.mul(raw_inverse, h[c][k])) + expected = int(algebra.table[i][j] == k) + require(actual == expected, "literal covariant tensor coefficient") + wrong += int(mistaken != expected) + missing_transpose += int(untransposed != expected) + checked += 1 + require(wrong > 0, "raw autotopism must not act covariantly without inverse transposes") + require(missing_transpose > 0, "inverse without transpose must reject") + triple = tuple(determinant(matrix, field) for matrix in (f_inverse_transpose, g_inverse_transpose, h)) + require(triple == (4, 4, 4), "literal covariant determinant triple") + return {"coefficients": checked, "wrong_convention_coefficients": wrong, + "missing_transpose_coefficients": missing_transpose} + + +def controls() -> dict[str, object]: + algebra = Algebra(Field(3), 2, 2) + x, y = (algebra.basis(j) for j in algebra.variables) + mixed = tuple(algebra.field.add(a, b) for a, b in zip(x, y, strict=True)) + require(algebra.powers(mixed)[-1] != algebra.zero, "non-Frobenius shear must fail") + binary = Algebra(Field(2), 2, 2) + bx, by = (binary.basis(j) for j in binary.variables) + bmixed = tuple(a ^ b for a, b in zip(bx, by, strict=True)) + require(binary.powers(bmixed)[-1] == binary.zero, "Frobenius shear discriminator") + rejected = 0 + for operation, args in ((Field, (True,)), (Field, (6,)), (Algebra, (Field(3), 6, 4)), + (character_data, (Field(3), 3, 2)), + (character_data, (Field(5), 2, 1))): + try: + operation(*args) + except ValueError: + rejected += 1 + else: + raise AssertionError("invalid checker domain accepted") + data = character_data(Field(3), 2, 2) + require(predicted_automorphism_image(Field(3), data) == {1, 2}, "swap sign is indispensable") + require(power_subgroup(Field(3), data["E"]) == {1}, "sign omission discriminator") + require(determinant_triples(Field(3), 2, 2)["image_size"] == 2, "two ternary determinant triples") + require(character_data(Field(7), 2, 3)["h"] == 2, "swap sign can disappear in higher dimension") + return {"invalid_domains_rejected": rejected, + "semantic_discriminators": ["Frobenius versus non-Frobenius shear", + "indispensable variable-swap sign", + "ternary covariant image size two", + "higher-dimensional swap sign disappearance"]} + + +def main() -> None: + contexts = ((3, 2, 2), (5, 2, 2), (7, 2, 2), (7, 2, 3), (3, 2, 4), + (5, 3, 2), (7, 3, 2), (2, 3, 2), (4, 3, 2), (8, 3, 2), + (3, 4, 2), (5, 4, 2), (5, 6, 2), (7, 6, 2), (13, 6, 2)) + witnesses = [linear_witnesses(Algebra(Field(q), n, d)) for q, n, d in contexts] + census = [complete_substitution_domain(3, 2), complete_substitution_domain(2, 3)] + units = [complete_unit_domain(3, 2), complete_unit_domain(2, 3)] + triples = [determinant_triples(Field(q), n, d) for q, n, d in contexts] + report = {"claim_type": "scoped proof with exact finite corroboration", "witnesses": witnesses, + "complete_substitutions": census, "complete_units": units, + "determinant_triples": triples, "literal_covariant": literal_covariant_control(), + "controls": controls()} + root = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", "verify.py") + report["source_sha256"] = {name: hashlib.sha256((root / name).read_bytes()).hexdigest() for name in names} + print(json.dumps(report, sort_keys=True, indent=2)) + print("PASS_NONFROBENIUS_RECTANGULAR_CHARACTERS no_new_kappa") + + +if __name__ == "__main__": + main()