From b80abf6285a93faee360a792942f06834f04c27a Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 11 Nov 2026 12:50:21 +0000 Subject: [PATCH] feat(research): classify square-zero tensor determinant images --- .../squarezero-tensor-characters/PROOF.md | 167 ++++++++++++++++ .../squarezero-tensor-characters/README.md | 140 ++++++++++++++ .../squarezero-tensor-characters/SOURCES.json | 24 +++ .../squarezero-tensor-characters/TASK.json | 102 ++++++++++ .../squarezero-tensor-characters/VERIFY.json | 32 ++++ .../squarezero-tensor-characters/algebra.py | 173 +++++++++++++++++ .../squarezero-tensor-characters/verify.py | 179 ++++++++++++++++++ 7 files changed, 817 insertions(+) create mode 100644 research/squarezero-tensor-characters/PROOF.md create mode 100644 research/squarezero-tensor-characters/README.md create mode 100644 research/squarezero-tensor-characters/SOURCES.json create mode 100644 research/squarezero-tensor-characters/TASK.json create mode 100644 research/squarezero-tensor-characters/VERIFY.json create mode 100644 research/squarezero-tensor-characters/algebra.py create mode 100644 research/squarezero-tensor-characters/verify.py diff --git a/research/squarezero-tensor-characters/PROOF.md b/research/squarezero-tensor-characters/PROOF.md new file mode 100644 index 0000000000..1113bd8960 --- /dev/null +++ b/research/squarezero-tensor-characters/PROOF.md @@ -0,0 +1,167 @@ +# Square-zero local multiplication tensors + +This contribution was produced by Nick Petalas. Apache-2.0. + +## Statement and conventions + +Let K=F_q, let V be a K-vector space of dimension d>=2, and set n=d+1. +Give A=K plus V the multiplication + +```text +(a,x)(b,y) = (ab, ay+bx). +``` + +Thus A is a commutative unital local algebra, its radical is J=V, and +J squared is zero. Conversely every commutative unital local K-algebra +with residue K and square-zero radical has this form: its given scalar +copy of K complements J, and all radical products vanish. Its socle is J, +of dimension d, so the d>=2 class is non-Gorenstein. + +Let t be the multiplication tensor in A* tensor A* tensor A. We use the +ordinary covariant action of GL(A*) times GL(A*) times GL(A). In chosen +dual/input and output bases these are three independent GL_n(K) factors. +Write Delta(t) for the ordered determinant image of its stabilizer, and +H_n={c^n:c in K*}. Then + +```text +Delta(t) = {(u,v,w) in (K*)^3 : uw in H_n and vw in H_n}. +``` + +If g=gcd(n,q-1), the same subgroup is defined by the two equations + +```text +(uw)^((q-1)/g) = (vw)^((q-1)/g) = 1. +``` + +It has (q-1)^3/g^2 elements. The GL_n(K)^3 orbit of t contains exactly +g^2 orbits under SL_n(K)^3. These statements hold after three independent +basis changes, because stabilizers conjugate factor by factor and +determinants are invariant under conjugation. + +This is a scoped algebraic proof. The finite verification below only +corroborates its constructions on explicitly bounded domains. + +## 1. Unit and automorphism determinants + +Use a basis (1,e_1,...,e_d) with e_i in J. Multiplication L_a by +a=(a_0,x) has matrix + +```text + [a_0 0 ] +L_a = [x a_0 I_d ]. +``` + +Therefore det(L_a)=a_0^n. The element a is a unit exactly when a_0 is +nonzero; its inverse is (a_0^-1,-a_0^-2 x). The unit determinant image is +precisely H_n. Nilpotent coordinates change no determinant. + +Every unital K-algebra automorphism fixes the scalar copy of K and +preserves the radical, since nilpotence and units are intrinsic. It is +therefore (a,x) -> (a,Px) for P in GL_d(K). Conversely every such P +preserves multiplication. Consequently Aut_K(A)=GL_d(K), with determinant +det(P) on the whole n-dimensional algebra. Its determinant map is onto +K*: the diagonal map with radical entries delta,1,...,1 attains delta. + +## 2. Normalize every autotopism + +Let F,G,H be invertible K-linear maps satisfying + +```text +F(x)G(y)=H(xy) for all x,y in A. +``` + +Put a=F(1), b=G(1). Setting one input to 1 gives H=L_b F=L_a G. +Thus L_a and L_b are invertible, and a,b are units. Define +sigma=L_(ab)^-1 H. The preceding identities give + +```text +F=L_a sigma, G=L_b sigma, H=L_(ab) sigma. +``` + +Substituting into the autotopism equation and cancelling the unit ab +shows sigma(x)sigma(y)=sigma(xy). Also sigma(1)=1, and sigma is invertible. +It is an algebra automorphism. Conversely every pair of units a,b and +every algebra automorphism sigma give an autotopism by these formulas. +This normalization is classical unital isotopy; it is included to fix the +action convention and does not rely on a predecessor's computation. + +## 3. Pass to the covariant tensor action and prove exactness + +The stabilizer triple associated to this autotopism is +(F^-T,G^-T,H). In fact its transformed bilinear map is + +```text +(x,y) -> H(F^-1(x) G^-1(y)) = xy. +``` + +Let alpha=a_0^n, beta=b_0^n, delta=det(sigma). Its ordered determinants are + +```text +u=alpha^-1 delta^-1, +v=beta^-1 delta^-1, +w=alpha beta delta. +``` + +In particular vw=alpha and uw=beta. Section 1 proves the necessity of +both nth-power restrictions. + +Conversely suppose (u,v,w) satisfies them. Choose a_0,b_0 in K* with +a_0^n=vw and b_0^n=uw. Take any radical coordinates for a,b, and choose +sigma with determinant delta=(uvw)^-1 using section 1. The displayed +formulas now give exactly u,v,w. Thus every allowed triple has an explicit +stabilizer, including nonzero radical coordinates in both unit factors. +This proves equality of the images, rather than just an upper bound. + +There is no additional restriction on uvw. For example, at q=5 and n=4, +the image is {(c,c,c^-1):c in F5*}. Its products c can be arbitrary. +Conversely a product-one triple can fail both nth-power restrictions: +(2,3,1) over F5 has product one but is excluded when n=4. + +## 4. Equations, size and special-linear orbit count + +The multiplicative group K* is cyclic of order m=q-1. Hence its nth-power +subgroup has size m/g and consists exactly of the roots of z^(m/g)=1, +where g=gcd(n,m). This proves the two equations in the statement. + +The map + +```text +(u,v,w) -> (uw,vw) +``` + +from (K*)^3 to (K*)^2 is onto and each fiber has m elements: choose w +freely and then u,v are forced. The preimage of H_n times H_n therefore +has m*(m/g)^2=m^3/g^2 elements. + +For completeness let G=GL_n(K)^3 and N=SL_n(K)^3. The componentwise +determinant map G -> (K*)^3 is surjective with kernel N, so N is normal. +The N-orbits on G/Stab(t) correspond to the cosets of +det(Stab(t)) in (K*)^3. Indeed two elements of G differ by a left element +of N and a right stabilizer precisely when their determinants differ by +an element of Delta(t). Their number is m^3/|Delta(t)|=g^2. + +This orbit count refers to ordinary linear tensor equivalence over K. +It asserts no semilinear count, physical implementation or computational +recognition algorithm for arbitrary tensors. + +## Interface, credit and scope + +Ali Romman's #5540 reconstructs commutative multiplication from arbitrary +square tensors over prime fields and leaves the recovered-algebra and +determinant-character interfaces open. It is a cited predecessor, not +replayed here. For its recovered square-zero local class, the above proof +gives the exact determinant subgroup. Given a multiplication chart, +membership of its determinant triple in Delta(t) decides whether a +general-linear equivalence can be adjusted to a special-linear one. +No extractor or transporter from an arbitrary uncharted tensor is supplied. + +Finite-field cyclicity, unital isotopy, radical invariance and the normal- +subgroup orbit argument are classical. The new contribution is their exact +assembly for this non-Gorenstein class, the two equations, attaining maps +and explicit replay. Related etale and rectangular truncated-polynomial +packages cover different algebras. Their verifiers, inventories and numerical +results are not used as steps of this proof. + +Independent human and formal proof-kernel review are unclaimed. This is no +new kappa, native caller, paid supplier, selected-frontier update or complete +multiplication theorem. diff --git a/research/squarezero-tensor-characters/README.md b/research/squarezero-tensor-characters/README.md new file mode 100644 index 0000000000..1add0991c2 --- /dev/null +++ b/research/squarezero-tensor-characters/README.md @@ -0,0 +1,140 @@ +# Exact determinant images for square-zero local tensors + +This contribution was produced by Nick Petalas. Apache-2.0. + +Scoped written algebraic proof with exact finite corroboration. Let K=F_q +and let A=K plus J be a commutative unital local K-algebra with residue K, +J squared zero, and d=dim_K J>=2. Put n=d+1 and g=gcd(n,q-1). For its +multiplication tensor in A* tensor A* tensor A, with the ordinary covariant +three-factor action, the exact stabilizer determinant image is + +```text +Delta = {(u,v,w) in (K*)^3 : uw and vw are nth powers in K*}. +``` + +Equivalently, `(uw)^((q-1)/g)=(vw)^((q-1)/g)=1`. Its order is +`(q-1)^3/g^2`, and its general-linear orbit splits into exactly `g^2` +special-linear orbits. Every allowed determinant triple has an explicit +attaining stabilizer, with arbitrary radical coordinates in its two units. + +At q=5 and n=4 the image is `{(c,c,c^-1):c in F5*}` and there are 16 +special-linear orbits. A product-one condition alone gives the wrong image. +[PROOF.md](PROOF.md) proves the statements over every finite field and all +d>=2, including characteristic two and extension fields. + +## What this adds + +Ali Romman's [PR #5540](https://github.com/CrocSwap/integer-mult-bounds/pull/5540) +reconstructs commutative multiplication from tensors over prime fields. It +leaves recovered-algebra comparison and determinant-character interfaces +open. This supplies the exact character subgroup for its non-Gorenstein +square-zero local class. The reconstruction theorem is cited, not audited. + +The etale, Frobenius-truncated and equal-cutoff rectangular determinant +packages concern different algebra classes. No scientific executable, +inventory, count or new theorem from those packages is a step of this proof. +Unital isotopy normalization, cyclicity of finite-field unit groups and the +normal-subgroup orbit argument are classical. The contribution is this exact +assembly, its two equations, constructive witnesses and bounded verifier. +Global literature priority is unclaimed. + +This changes the formal-interface-lemma card to an algebraic side result. +It does not meet that card's proof-assistant gate or discharge a selected +supplier assumption. The canonical base is +`e54523517d0f03e58352e647c403a5af3e525a57`, priority revision 8, selected +#7000 with conditional kappa .00363005817. The baseline binding check passed. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19541747) +and SOURCES.json record the source interface and provenance. + +## Exact finite evidence + +The new verifier uses only its own arithmetic and Python's standard library. +It writes no files and emits a generated JSON receipt with SHA256 hashes of +all seven package files. Checks remain active under optimized Python. + +- All 42 contexts with q in {2,3,4,5,7,8,11} and n=3,...,8. Every allowed + determinant triple has a literal full tensor-action witness: 5,448 total. + All 4,506 excluded triples reject. Independently enumerated cosets of the + attained subgroup give the claimed special-linear orbit count. +- Complete raw automorphism domains of 512, 65,536 and 19,683 matrices at + (q,n)=(2,3),(2,4),(3,3), accepting 6, 168 and 48 automorphisms. These tests + check invertibility, the unit and every basis product directly. +- A separate complete GL3(F2)^2 domain contains 28,224 input-map pairs. + The unit forces the only possible output map; exactly 96 pairs give + invertible autotopisms. Their full covariant tensor action also passes. +- All 833 elements of seven specified small algebras check the literal + multiplication determinant; 680 are units. Field checks cover 2,410 + triples. Fifteen controls reject changed tensor factors, the wrong input + action convention, omitted subgroup restrictions and invalid domains. + +The exhaustive claims apply only to these named finite domains. The +all-field and all-dimension conclusions rely on the written proof. + +## Reproduce + +From the repository root with CPython 3.12: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/squarezero-tensor-characters/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -O -B research/squarezero-tensor-characters/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/squarezero-tensor-characters +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/squarezero-tensor-characters --check-source-history --check-modes +``` + +Another machine may substitute its CPython 3.12 path. The direct marker is +`PASS_SQUAREZERO_TENSOR_CHARACTERS`; registered replay also returns +`PASS_REGISTERED_RESEARCH_PACKAGE`. The direct commands need no Git or +predecessor files. Provenance checks require the recorded repository history. + +## Limits and engineering + +There is no arbitrary-tensor recognizer, supplied-table radical extractor or +special-linear transporter implementation here. The witness builder accepts +canonical multiplication charts on the bounded field/dimension domain of +the verifier. The proof gives the image on the promised general-linear +orbit; the group-theoretic orbit count does not supply an algorithm to find +that chart. Nonsplit residue fields, higher radical products and semilinear +equivalence are outside the result. + +The code has no recursion or external processes. Matrix loops have dimension +at most eight, field loops have order at most eleven, exponentiation has at +most 64 steps, and raw matrix enumeration rejects domains larger than 70,000. +Each function is below 60 physical lines. Explicit ValueError checks cover +all mathematical verification conditions, including optimized execution. +Internal matrix helpers receive only constructed bounded fixtures. + +Power-of-Ten rule 3 has a bounded managed-runtime deviation: Python allocates +matrix rows, integers and sets during verification. The largest determinant +ambient group has 1,000 triples. Cosets partition that group; at most 1,000 +triples persist across the distinct stored cosets, with one further transient +coset of at most 1,000 entries. The full GL3(F2) list stores 168 matrices; +larger raw domains stream one matrix at a time. The lifetime ends at each +finite check. No external input can enlarge these fixtures. A future general +API must set its own resource contract. Rule 9's exception is the fixed list +of local rejection callbacks; none escapes its immediate check. Warning-strict +normal/optimized execution and AST compilation provide the available Python +diagnostics; no claim of exhaustive static analysis is made. + +There is no physical coefficient preparation, native program, dirty-state +restoration tariff, precision/tape implementation, complete paid supplier, +new kappa or selected-frontier change. No selected cold replay, Lean or Docker +run is needed for this isolated algebraic statement. Independent human and +formal proof-kernel review are unclaimed. + +## Open next questions + +1. Build a bounded supplied-table extractor for this exact class, then compose + it with #5540's recovered-table interface and an explicit special-linear + transporter. Begin with the radical and scalar-residue checks. No such + program is supplied here. +2. Determine the determinant image for square-zero local algebras with a + nonsplit residue field. Start with the determinant of the induced + semilinear radical map; the present scalar-residue calculation does not + justify dropping that contribution. +3. Find a named native producer/consumer that uses one of these equivalences, + then charge coefficient preparation, movement, precision and restoration. + An abstract special-linear orbit count supplies none of those costs. + +Credit Ali Romman for #5540 and its retained apoursh, Nick Petalas, David Ganz +and tensor/algebra reconstruction lineage. Classical algebra and finite-field +facts retain their usual credit. Predecessor source files are unchanged. diff --git a/research/squarezero-tensor-characters/SOURCES.json b/research/squarezero-tensor-characters/SOURCES.json new file mode 100644 index 0000000000..0a09b4dc6f --- /dev/null +++ b/research/squarezero-tensor-characters/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "75d77b328ea02ded535e7f23aee5b1e55d0bb1a8", + "sha256": "154c3d30455d778fd3343b6b4851f0fa4665f0f7625b0adb3675e2bafbbf6bf1" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/nonreduced-tensor-recognition/README.md", + "usage": "provenance", + "git_blob": "826c6b010725d98b6ca6599a748c4179264140e9", + "sha256": "2eaed94a9f12ad7b6bb7253b14bff95b86549b3e320f0e91fa4e35c0025536de" + } + ] +} diff --git a/research/squarezero-tensor-characters/TASK.json b/research/squarezero-tensor-characters/TASK.json new file mode 100644 index 0000000000..6a90805eb7 --- /dev/null +++ b/research/squarezero-tensor-characters/TASK.json @@ -0,0 +1,102 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "e54523517d0f03e58352e647c403a5af3e525a57", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact covariant stabilizer determinant image and special-linear orbit count for split local multiplication tensors with radical squared zero and radical dimension at least two, over every finite field.", + "scope_change_reason": "A written algebraic side result at the recovered-table interface of Ali Romman PR5540 replaces proof-assistant work. The non-Gorenstein square-zero class is outside the etale and rectangular truncated-polynomial character results; no selected-supplier assumption is discharged.", + "bottleneck_link": "Algebraic side result: character obstructions distinguish general-linear equivalence from special-linear implementability. No native caller or complete paid saving follows.", + "budget_minutes": 60, + "stop_rule": "Stop after the exact image, explicit attaining maps and bounded finite corroboration; do not expand to higher nilpotency or physical implementation.", + "outcome": "completed", + "evidence": "PROOF.md; verify.py generates hash-bound receipts. All 42 field/dimension images, 5448 attaining maps, 4506 exclusions, three raw automorphism domains and the complete 28224-pair binary stabilizer census pass.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Construct an exact supplied-table extractor and special-linear transporter for this class.", + "why_it_matters": "Makes the character theorem executable at the recovered-table interface.", + "first_step": "Recover the radical and scalar residue and bind one multiplication chart.", + "blocked_by": "No arbitrary-table extractor or transporter is included." + }, + { + "question": "Determine the image for nonsplit residue fields.", + "why_it_matters": "Separates the residue norm and semilinear radical determinants.", + "first_step": "Classify the determinant of the induced semilinear radical map.", + "blocked_by": "The scalar-residue proof does not cover that contribution." + } + ], + "claim_type": "scoped written algebraic proof with exact finite corroboration" +} diff --git a/research/squarezero-tensor-characters/VERIFY.json b/research/squarezero-tensor-characters/VERIFY.json new file mode 100644 index 0000000000..f38b82c8ad --- /dev/null +++ b/research/squarezero-tensor-characters/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": "All-field theorem finite fixtures, exact tensor action, full small raw censuses, cosets and rejecting controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Identical finite verification with optimization; explicit checks remain active." + } + ] +} diff --git a/research/squarezero-tensor-characters/algebra.py b/research/squarezero-tensor-characters/algebra.py new file mode 100644 index 0000000000..b3e6563756 --- /dev/null +++ b/research/squarezero-tensor-characters/algebra.py @@ -0,0 +1,173 @@ +"""Exact bounded arithmetic for the split radical-square-zero fixtures.""" + +from itertools import product + +FIELDS = (2, 3, 4, 5, 7, 8, 11) +MAX_DIMENSION = 8 +MAX_MATRIX_DOMAIN = 70_000 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +class Field: + """Prime fields and the fixed polynomial presentations F4 and F8.""" + + def __init__(self, order): + require(type(order) is int and order in FIELDS, "unsupported field") + self.q = order + self.modulus = {4: 0b111, 8: 0b1011}.get(order) + + def add(self, a, b): + return a ^ b if self.modulus else (a + b) % self.q + + def neg(self, a): + return a if self.modulus else -a % self.q + + def sub(self, a, b): + return self.add(a, self.neg(b)) + + def mul(self, a, b): + if not self.modulus: + return a * b % self.q + result = 0 + for _ in range(self.q.bit_length() - 1): + if b & 1: + result ^= a + b >>= 1 + a <<= 1 + if a & self.q: + a ^= self.modulus + return result + + def power(self, a, exponent): + require(0 <= exponent <= 64, "exponent exceeds fixture bound") + result = 1 + for _ in range(exponent): + result = self.mul(result, a) + return result + + def inverse(self, a): + require(a != 0, "zero has no inverse") + return self.power(a, self.q - 2) + + +def identity(n): + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def determinant(matrix, field): + rows = [row[:] for row in matrix] + n = len(rows) + value = 1 + for column in range(n): + pivot = next((j for j in range(column, n) if rows[j][column]), None) + if pivot is None: + return 0 + if pivot != column: + rows[column], rows[pivot] = rows[pivot], rows[column] + value = field.neg(value) + entry = rows[column][column] + value = field.mul(value, entry) + reciprocal = field.inverse(entry) + for j in range(column + 1, n): + scale = field.mul(rows[j][column], reciprocal) + for k in range(column + 1, n): + rows[j][k] = field.sub(rows[j][k], field.mul(scale, rows[column][k])) + return value + + +def inverse(matrix, field): + n = len(matrix) + rows = [matrix[i][:] + identity(n)[i] for i in range(n)] + for column in range(n): + pivot = next((j for j in range(column, n) if rows[j][column]), None) + require(pivot is not None, "singular matrix") + rows[column], rows[pivot] = rows[pivot], rows[column] + scale = field.inverse(rows[column][column]) + rows[column] = [field.mul(scale, x) for x in rows[column]] + for j in range(n): + if j != column: + scale = rows[j][column] + rows[j] = [field.sub(x, field.mul(scale, y)) + for x, y in zip(rows[j], rows[column])] + return [row[n:] for row in rows] + + +def transpose(matrix): + return [list(row) for row in zip(*matrix)] + + +def matvec(matrix, vector, field): + result = [] + for row in matrix: + value = 0 + for a, b in zip(row, vector): + value = field.add(value, field.mul(a, b)) + result.append(value) + return result + + +def matmul(left, right, field): + return transpose([matvec(left, column, field) for column in transpose(right)]) + + +def multiply(left, right, field): + """Multiplication in F plus J, with J squared zero and e0 the unit.""" + return [field.mul(left[0], right[0])] + [ + field.add(field.mul(left[0], right[j]), field.mul(right[0], left[j])) + for j in range(1, len(left))] + + +def unit_matrix(unit, field): + return transpose([multiply(unit, column, field) for column in identity(len(unit))]) + + +def preserves_product(first, second, output, field): + n = len(first) + columns_f, columns_g = transpose(first), transpose(second) + basis = identity(n) + for i, j in product(range(n), repeat=2): + left = multiply(columns_f[i], columns_g[j], field) + if left != matvec(output, multiply(basis[i], basis[j], field), field): + return False + return True + + +def fixes_tensor(first, second, output, field): + """Literal covariant action on every coefficient of the multiplication tensor.""" + n = len(first) + basis = identity(n) + for i, j in product(range(n), repeat=2): + # The first two tensor factors act on covectors, hence these rows. + transformed = matvec(output, multiply(first[i], second[j], field), field) + if transformed != multiply(basis[i], basis[j], field): + return False + return True + + +def witness(triple, n, field): + """Construct a stabilizer with the requested allowed determinant triple.""" + require(3 <= n <= MAX_DIMENSION, "radical dimension must be at least two") + require(len(triple) == 3 and all(type(x) is int and 0 < x < field.q + for x in triple), "invalid determinant triple") + u, v, w = triple + roots = {field.power(a, n): a for a in range(1, field.q)} + aw, bw = field.mul(v, w), field.mul(u, w) + require(aw in roots and bw in roots, "outside determinant image") + a = [roots[aw]] + [(i + u) % field.q for i in range(1, n)] + b = [roots[bw]] + [(i + v + 1) % field.q for i in range(1, n)] + sigma = identity(n) + sigma[1][1] = field.inverse(field.mul(field.mul(u, v), w)) + first = matmul(unit_matrix(a, field), sigma, field) + second = matmul(unit_matrix(b, field), sigma, field) + output = matmul(unit_matrix(multiply(a, b, field), field), sigma, field) + return transpose(inverse(first, field)), transpose(inverse(second, field)), output + + +def all_matrices(n, field): + require(field.q ** (n * n) <= MAX_MATRIX_DOMAIN, "matrix census exceeds cap") + for entries in product(range(field.q), repeat=n * n): + yield [list(entries[n * i:n * (i + 1)]) for i in range(n)] diff --git a/research/squarezero-tensor-characters/verify.py b/research/squarezero-tensor-characters/verify.py new file mode 100644 index 0000000000..ecc2ac91a0 --- /dev/null +++ b/research/squarezero-tensor-characters/verify.py @@ -0,0 +1,179 @@ +"""Finite corroboration of the new square-zero tensor determinant theorem.""" + +import hashlib +from itertools import product +import json +from math import gcd +from pathlib import Path +import platform + +from algebra import (FIELDS, Field, all_matrices, determinant, fixes_tensor, + identity, inverse, matmul, preserves_product, require, + transpose, unit_matrix, witness) + + +def field_checks(): + cases = 0 + for q in FIELDS: + f = Field(q) + for a, b, c in product(range(q), repeat=3): + require(f.mul(a, f.add(b, c)) == f.add(f.mul(a, b), f.mul(a, c)), + "distributivity") + require(f.mul(f.mul(a, b), c) == f.mul(a, f.mul(b, c)), "associativity") + cases += 1 + for a in range(1, q): + require(f.mul(a, f.inverse(a)) == 1, "inverse law") + return cases + + +def rejects(operation): + try: + operation() + except ValueError: + return 1 + raise ValueError("invalid operation was accepted") + + +def image_checks(): + reports = [] + for q, n in product(FIELDS, range(3, 9)): + f = Field(q) + powers = {f.power(a, n) for a in range(1, q)} + actual, equations = set(), set() + rejected = 0 + exponent = (q - 1) // gcd(n, q - 1) + for triple in product(range(1, q), repeat=3): + u, v, w = triple + allowed = f.mul(v, w) in powers and f.mul(u, w) in powers + if (f.power(f.mul(v, w), exponent) == 1 + and f.power(f.mul(u, w), exponent) == 1): + equations.add(triple) + if not allowed: + rejected += rejects(lambda: witness(triple, n, f)) + continue + matrices = witness(triple, n, f) + require(tuple(determinant(m, f) for m in matrices) == triple, + "wrong attaining determinant") + require(fixes_tensor(*matrices, f), "literal tensor action failed") + actual.add(triple) + require(actual == equations, "equations disagree with constructed image") + require(len(actual) * gcd(n, q - 1) ** 2 == (q - 1) ** 3, "image order") + ambient = set(product(range(1, q), repeat=3)) + orbits = set() + for c in ambient: + coset = frozenset(tuple(f.mul(a, b) for a, b in zip(c, d)) for d in actual) + orbits.add(coset) + require(len(orbits) == gcd(n, q - 1) ** 2, "SL orbit index") + reports.append(dict(q=q, dimension=n, attained=len(actual), rejected=rejected, + special_linear_orbits=len(orbits))) + return reports + + +def automorphism_census(q, n): + """All raw square matrices, tested by unit, inverse and basis products.""" + f = Field(q) + tested = invertible = accepted = 0 + determinants = set() + for matrix in all_matrices(n, f): + tested += 1 + det = determinant(matrix, f) + if not det: + continue + invertible += 1 + if transpose(matrix)[0] != identity(n)[0]: + continue + if preserves_product(matrix, matrix, matrix, f): + accepted += 1 + determinants.add(det) + expected = 1 + d = n - 1 + for i in range(d): + expected *= q ** d - q ** i + require(accepted == expected, "raw automorphism census order") + require(determinants == set(range(1, q)), "automorphism determinant image") + return dict(q=q, dimension=n, raw_matrices=tested, invertible=invertible, + automorphisms=accepted) + + +def stabilizer_census(): + """Full GL3(F2)^2 search; the output map is forced by the unit.""" + f, n = Field(2), 3 + invertibles = [m for m in all_matrices(n, f) if determinant(m, f)] + tested = accepted = 0 + determinants = set() + for first, second in product(invertibles, repeat=2): + tested += 1 + b = transpose(second)[0] + output = matmul(unit_matrix(b, f), first, f) + if not determinant(output, f) or not preserves_product(first, second, output, f): + continue + accepted += 1 + covariant = (transpose(inverse(first, f)), transpose(inverse(second, f)), output) + require(fixes_tensor(*covariant, f), "raw isotopy/covariant conversion") + determinants.add(tuple(determinant(m, f) for m in covariant)) + require(accepted == 96 and determinants == {(1, 1, 1)}, "full stabilizer census") + return dict(q=2, dimension=3, input_map_pairs=tested, stabilizers=accepted) + + +def norm_census(): + reports = [] + for q, n in ((2, 3), (2, 4), (3, 3), (3, 4), (4, 3), (5, 3), (8, 3)): + f = Field(q) + units = 0 + image = set() + for a in product(range(q), repeat=n): + det = determinant(unit_matrix(a, f), f) + require(det == f.power(a[0], n), "literal unit multiplication determinant") + if a[0]: + units += 1 + image.add(det) + require(image == {f.power(a, n) for a in range(1, q)}, "norm image") + reports.append(dict(q=q, dimension=n, elements=q ** n, units=units, + norm_image=sorted(image))) + return reports + + +def controls(): + f, n = Field(5), 4 + base = witness((2, 2, 3), n, f) + require(fixes_tensor(*base, f), "control fixture invalid") + detected = 0 + for factor in range(3): + changed = [[row[:] for row in matrix] for matrix in base] + changed[factor][0][0] = f.add(changed[factor][0][0], 1) + require(not fixes_tensor(*changed, f), "factor mutation was undetected") + detected += 1 + raw_inputs = (transpose(inverse(base[0], f)), transpose(inverse(base[1], f)), base[2]) + require(not fixes_tensor(*raw_inputs, f), "raw autotopism input convention accepted") + detected += 1 + for operation in (lambda: Field(6), lambda: Field(True), + lambda: witness((0, 1, 1), n, f), + lambda: witness((1, 1, 1), 2, f), + lambda: witness((1, 2, 1), n, f), + lambda: inverse([[1, 0], [0, 0]], f), + lambda: list(all_matrices(5, Field(2))), + lambda: f.power(1, 65)): + detected += rejects(operation) + # Both restrictions are needed; product-one alone is insufficient. + for triple in ((1, 2, 1), (2, 1, 1), (2, 3, 1)): + detected += rejects(lambda: witness(triple, n, f)) + return detected + + +def main(): + result = dict(status="PASS_SQUAREZERO_TENSOR_CHARACTERS", + python=platform.python_version(), field_triples=field_checks(), + images=image_checks(), norms=norm_census(), + automorphisms=[automorphism_census(q, n) + for q, n in ((2, 3), (2, 4), (3, 3))], + stabilizer=stabilizer_census(), controls=controls()) + root = Path(__file__).resolve().parent + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "algebra.py", "verify.py") + result["sha256"] = {name: hashlib.sha256((root / name).read_bytes()).hexdigest() + for name in names} + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()