From 571194d4ce2a1ae5473a0fe9ff6d71384d877bcd Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 27 Oct 2026 10:12:45 +0000 Subject: [PATCH] feat(research): derive matrix tensor determinant characters --- .../matrix-tensor-determinant-image/PROOF.md | 193 +++++++++++ .../matrix-tensor-determinant-image/README.md | 123 +++++++ .../SOURCES.json | 36 ++ .../matrix-tensor-determinant-image/TASK.json | 118 +++++++ .../VERIFY.json | 34 ++ .../matrix-tensor-determinant-image/verify.py | 324 ++++++++++++++++++ 6 files changed, 828 insertions(+) create mode 100644 research/matrix-tensor-determinant-image/PROOF.md create mode 100644 research/matrix-tensor-determinant-image/README.md create mode 100644 research/matrix-tensor-determinant-image/SOURCES.json create mode 100644 research/matrix-tensor-determinant-image/TASK.json create mode 100644 research/matrix-tensor-determinant-image/VERIFY.json create mode 100644 research/matrix-tensor-determinant-image/verify.py diff --git a/research/matrix-tensor-determinant-image/PROOF.md b/research/matrix-tensor-determinant-image/PROOF.md new file mode 100644 index 0000000000..907199c873 --- /dev/null +++ b/research/matrix-tensor-determinant-image/PROOF.md @@ -0,0 +1,193 @@ +# Determinant characters of a full matrix multiplication tensor + +This scoped proof was produced by Nick Petalas. Apache-2.0. + +## Statement and action convention + +Let K=F_q, n>=1, A=M_n(K), d=n^2, and let +mu in A* tensor A* tensor A be the tensor of matrix multiplication. +All three tensor factors have independent general-linear actions, with +no permutations of the factors and no semilinear field automorphisms. +Let Delta(mu) be the ordered determinant image of its stabilizer. +Write m=q-1, g=gcd(n,m), h=m/g, and H_n={a^n:a in K*}. + +Then + +```text +Delta(mu) = {(u,v,(uv)^-1): u,v in H_n} + = {(u,v,w) in (K*)^3: u^h=v^h=1, uvw=1}. (1) +``` + +Consequently the GL_d(K)^3 orbit of mu contains exactly + +```text +(q-1) gcd(n,q-1)^2 (2) +``` + +orbits under SL_d(K)^3. A promised tensor in the GL orbit of mu has the +same determinant image, even when the three multiplication bases are not +given. Its dimensions and q give the three character equations in (1). +This is an extraction algorithm under an orbit promise, not recognition. + +For a literal multiplication tensor, or one with a supplied multiplication +chart, an existing GL transporter with determinant triple (d1,d2,d3) +can be corrected to an SL transporter exactly when + +```text +d1,d2 in H_n and d1 d2 d3=1. (3) +``` + +The proof below gives an attaining correction whenever (3) holds. + +## Normalize every stabilizer + +In chosen dual bases, a covariant triple (S,T,R) stabilizes mu exactly +when (F,G,H)=(S^-T,T^-T,R) satisfies + +```text +F(x)G(y)=H(xy) for every x,y in A. (4) +``` + +Indeed covariant action gives R mu(S^T x,T^T y)=mu(x,y); +substitute x=F(a), y=G(b). This fixes the inverse-input convention. + +Put a=F(1), b=G(1). Setting one input in (4) to 1 gives +H(x)=F(x)b=aG(x). Hence right multiplication by b and left +multiplication by a are bijective: for example R_b=H F^-1. +Surjectivity of R_b gives cb=1. Injectivity applied to +(bc-1)b=0 gives bc=1. Thus b is a unit, and the same argument +on the other side makes a a unit. + +Define sigma(x)=a^-1 F(x)=a^-1 H(x)b^-1=G(x)b^-1. +It is an invertible K-linear unital map. Equation (4) gives + +```text +sigma(x)sigma(y) + = a^-1 F(x)G(y)b^-1 + = a^-1 H(xy)b^-1 + = sigma(xy). +``` + +Therefore sigma is an algebra automorphism, and every autotopism has +the form + +```text +F=L_a sigma, G=R_b sigma, H=L_a R_b sigma, a,b in GL_n(K). (5) +``` + +Conversely (5) satisfies (4) for every such a,b and every algebra +automorphism sigma. This is the unital associative normalization of +David Ganz's atlas A019, written here in a two-sided form to preserve +the multiplication order. No commutativity is assumed. + +## The automorphism contributes determinant one + +Here is the classical matrix-unit proof, included to make the +noncommutative step self-contained. Put f_ij=sigma(E_ij). +These are matrix units, with f_ij f_kl=delta_jk f_il and sum f_ii=I. +The nonzero idempotent f_11 has a nonzero vector v in its image. +For 1<=i<=n put v_i=f_i1 v. Then f_1j v_i=delta_ji v. +Thus sum c_i v_i=0 implies every c_j=0. There are n independent +vectors v_i in K^n, so they form a basis. If P has these columns, +then f_ij v_k=delta_jk v_i proves f_ij=P E_ij P^-1. +By linearity sigma(x)=P x P^-1 for every x. + +Left multiplication L_P acts independently on n columns, so its +determinant as a d-dimensional linear map is det(P)^n. +Right multiplication R_Q acts independently on n rows and has +determinant det(Q)^n. These statements are basis-independent. +Consequently + +```text +det(sigma)=det(L_P)det(R_(P^-1))=1. (6) +``` + +For n=1 the same argument says sigma is the identity. For n>1, +transposition reverses the product and cannot replace sigma in (5) +with the two inputs in their fixed order. Factor permutations are +outside the action being considered. + +## Image equality and the equation table + +Let alpha=det(a), beta=det(b). Equations (5) and (6) give + +```text +(det F,det G,det H)=(alpha^n,beta^n,(alpha beta)^n). +``` + +The covariant triple has determinants + +```text +(alpha^-n,beta^-n,(alpha beta)^n). (7) +``` + +Every covariant stabilizer therefore lies in the right side of (1). +Conversely, for u,v in H_n choose alpha,beta with alpha^-n=u, +beta^-n=v. Take a=diag(alpha,1,...,1), b=diag(beta,1,...,1), and +sigma=identity in (5). This realizes (u,v,(uv)^-1), so no other +restriction is present. + +The cyclic group K* of order m has nth-power subgroup of order h, +which is precisely the set of roots of X^h=1. This proves (1). +To put its three equations into atlas A029's bounded table, use rows + +```text +(h mod m,0,0), (0,h mod m,0), (1 mod m,1 mod m,1 mod m). +``` + +For q=2 all entries are zero and the target determinant group is +trivial. For n=1 equation (1) gives the full product-one subgroup, +and (2) gives q-1, as it should for a nonzero scalar tensor. + +If mu'=k mu for a triple of independent base changes, its stabilizer +is k Stab(mu) k^-1. Determinants are unchanged by conjugation in +each factor, so the same image holds in unknown independent bases. +Under that promise, finding n from the common dimension d=n^2, +computing gcd(n,q-1), and reducing three exponent rows extracts the +table without enumerating any automorphism group. These integer +operations take polynomial bit time in the dimensions and log q; +evaluating the resulting equations uses ordinary field powers. + +## Special-linear orbits and a correction witness + +Let G=GL_d(K)^3, N=SL_d(K)^3, and D=(K*)^3. The determinant +map G to D is surjective with kernel N. Since N is normal, +N-orbits in G/Stab(mu) are the cosets D/Delta(mu): two elements +of G give the same N-orbit exactly when their determinant triples +differ by an element of Delta(mu). Formula (1) gives +|Delta(mu)|=h^2. Hence their number is m^3/h^2=m g^2, proving (2). + +Given g0 with g0 mu=t and determinant triple (d1,d2,d3), every +other transporter mu to t is g0 s with s in Stab(mu). Its factors +all have determinant one exactly when det(s)=(d1^-1,d2^-1,d3^-1). +Equation (1) makes this equivalent to (3). + +For attainment choose alpha^n=d1 and beta^n=d2 and the diagonal +a,b above. The stabilizer + +```text +s=(L_a^-T,R_b^-T,L_a R_b) +``` + +has determinant triple (d1^-1,d2^-1,d1 d2)=(d1^-1,d2^-1,d3^-1). +Thus g0 s is an SL transporter. If a source multiplication chart +k is supplied instead, use k s k^-1 in the source basis. Existence +of a GL transporter and any needed multiplication chart are explicit +inputs to this construction, not outputs of the extraction algorithm. + +## What is new here and what remains open + +This package adds the exact noncommutative full-matrix-algebra image, +its orbit count and constructive determinant correction to the +repository's promised-class extraction results. David Ganz's atlas +#2849 supplies A019's normalization and A029/A030's question and +framework. Nick Petalas's #5252 handles finite etale algebras; it +is a precedent, not a result reverified here. Innerness for full +matrix algebras and finite cyclic-group arithmetic are classical. +Global literature priority is unclaimed. + +The all-field theorem is this written argument. Finite executable +checks corroborate it and do not constitute a proof-kernel derivation. +No raw-tensor recognition algorithm, general semisimple classification, +native program, supplier admission or integer multiplication saving +is established. diff --git a/research/matrix-tensor-determinant-image/README.md b/research/matrix-tensor-determinant-image/README.md new file mode 100644 index 0000000000..2555bb7859 --- /dev/null +++ b/research/matrix-tensor-determinant-image/README.md @@ -0,0 +1,123 @@ +# Exact determinant image of a full matrix multiplication tensor + +This contribution was produced by Nick Petalas. Apache-2.0. + +**Claim type: scoped algebraic proof with exact finite corroboration.** +Let mu be multiplication in M_n(F_q), viewed as an ordinary tensor in +A* tensor A* tensor A. Put H_n={(a^n):a in F_q*}. Its ordered covariant +stabilizer determinant image is exactly + +```text +Delta(mu) = {(u,v,(uv)^-1): u,v in H_n}. +``` + +Its GL_(n^2)(F_q)^3 orbit contains exactly +`(q-1) gcd(n,q-1)^2` orbits under SL_(n^2)(F_q)^3. +Both statements hold for every finite field and every n>=1, including +characteristic dividing n. Independent input/output basis changes do not +change the image. + +[PROOF.md](PROOF.md) derives the character table, proves that every +allowed determinant triple is attained, and gives an explicit stabilizer +that corrects a supplied GL transporter to an SL transporter whenever +possible. Under an explicit promise of membership in this multiplication +orbit, the dimensions and q suffice to extract the three character +equations without enumerating a stabilizer. This adds a noncommutative +case to David Ganz's atlas A030 question in +[#2849](https://github.com/CrocSwap/integer-mult-bounds/pull/2849). +It does not recognize arbitrary tensors or recover unknown multiplication +bases. A constructive transporter correction requires the literal source +tensor or a supplied multiplication chart. + +## Reproduction + +From the repository root, with CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/matrix-tensor-determinant-image/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/matrix-tensor-determinant-image/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/matrix-tensor-determinant-image +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/matrix-tensor-determinant-image --check-source-history +``` + +Another CPython 3.12 installation can replace the absolute interpreter +path. The direct verifier prints `PASS_MATRIX_TENSOR_DETERMINANT_IMAGE +no_new_kappa` and a generated JSON receipt binding all six package files +by SHA256. It writes no files and needs no Git checkout. The publication +preflight requires a committed package and its pinned source history. + +## Evidence and implementation limits + +The written proof supplies the universal claim. The independent finite +corroboration uses q=2,3,4,5,7,8,9 and n=1,2,3. The extension fields +are literal polynomial quotients, and every nonzero element has an +enumerated multiplicative inverse. + +- In 21 field/size contexts, 537 constructed stabilizers satisfy every + basis-product identity and all 142,126 coefficients of the transformed + covariant multiplication tensors. Their determinant triples attain + every predicted image and agree with the three-equation description. +- A separate complete enumeration visits all 65,536 binary 4-by-4 + linear maps, finds 20,160 invertible maps, and tests which preserve + the unit and all matrix-basis products. Its six automorphisms equal + the six inner maps of M_2(F_2). +- At n=2, all 1,171 determinant triples over those seven fields are + considered. Explicit stabilizers correct all 89 admissible triples + to determinant one in each factor; the other 1,082 fail the criterion. + This is a determinant-domain census, not an enumeration of whole + transporter sets or whole tensor orbits. +- Twelve semantic and boundary controls distinguish raw input-map + determinants from covariant determinants, both character constraints, + even n, an extension field, n=1, q=2, an altered tensor factor and + unsupported checker domains. Explicit exceptions preserve all checks + under optimized Python. + +The verifier has no recursion, subprocess, dynamic code loading or +external dependency. Its fixed domains bound every loop: fields have at +most nine elements, matrices have dimension at most nine, the exhaustive +map domain has 65,536 elements, and explicit powers stop at 128. Every +function stays below 60 physical lines. CPython's managed allocation is +a deviation from fixed steady-state allocation; fixed fixture domains +bound the live matrices and sets. Table-driven arithmetic and ordinary +iterator dispatch are bounded managed-runtime indirections. Warning-strict +normal and optimized runs provide diagnostics; no separate static +analyzer or proof kernel is claimed. + +## Scope and credit + +The tensor factors remain ordered and the action is K-linear. Semilinear +actions and factor permutations are outside scope. The promised orbit +class, literal-source/chart requirement for correction, and existing GL +transporter are explicit hypotheses. There is no physical supplier, +native operator, uniform compiler, precision/stock bill, new kappa or +complete multiplication theorem. Independent human and formal proof-kernel +review are unclaimed. Lean, Docker and selected scientific replay are unrun. + +Credit David Ganz's [atlas #2849](https://github.com/CrocSwap/integer-mult-bounds/pull/2849) +for A019's associative isotopy normalization, A029's bounded character +framework and A030's extraction question. Nick Petalas's merged +[#5252](https://github.com/CrocSwap/integer-mult-bounds/pull/5252) provides +the finite-etale extraction precedent. The atlas retains the Chen, +Grochow, Qiao, Tang and Zhang tensor-action context. Innerness of full +matrix-algebra automorphisms, matrix-unit arguments and cyclic-group +arithmetic are classical. The new contribution is the exact matrix-algebra +character extraction and correction package in this repository. Global +literature priority is unclaimed. No predecessor executable is imported +or replayed, and no predecessor credit is changed. + +[SOURCES.json](SOURCES.json) binds the atlas, etale predecessor, original +task catalogue and selected record as historical provenance. They are +not live executable inputs. [TASK.json](TASK.json) explicitly changes +the formal-interface card to this algebraic side question. + +## Open next questions + +1. What is the exact image for products of full matrix algebras over + finite extensions? Derive one extension-field block character, then + account for determinants of permutations of identical blocks. Those + extension and permutation characters remain unproved here. +2. Can a raw tensor in this class be recognized with a multiplication + chart and transporter? Start with its three nuclei and simple-module + actions. A complete recognition and chart-recovery proof is missing. + +The structured first steps and blockers are in [TASK.json](TASK.json). diff --git a/research/matrix-tensor-determinant-image/SOURCES.json b/research/matrix-tensor-determinant-image/SOURCES.json new file mode 100644 index 0000000000..ae5af67b9f --- /dev/null +++ b/research/matrix-tensor-determinant-image/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "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" + }, + { + "path": "research/etale-tensor-determinant-image/README.md", + "usage": "provenance", + "git_blob": "0f07df6ce2a8c43ea1fcc5f0081ee3532da28208", + "sha256": "2ec18042a1a63d5fd5da246f4f6060c5fb66cff338f25a2a1b95e3ea8b4f0fba" + } + ] +} diff --git a/research/matrix-tensor-determinant-image/TASK.json b/research/matrix-tensor-determinant-image/TASK.json new file mode 100644 index 0000000000..bee3bd06a6 --- /dev/null +++ b/research/matrix-tensor-determinant-image/TASK.json @@ -0,0 +1,118 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 8, + "base_commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "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 ordered covariant stabilizer determinant image, SL orbit count and determinant-correction witness for multiplication in M_n(F_q), all n>=1 and every finite field, under an explicit orbit promise.", + "scope_change_reason": "The user requests original mathematical work rather than a predecessor audit. This changes the formal-interface card to atlas A030's noncommutative full-matrix-algebra extraction case; it is a scoped algebraic side result, not a selected-caller formalization.", + "bottleneck_link": "Side result for exact tensor equivalence and character extraction. It supplies no physical supplier or new kappa.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified matrix-algebra image theorem; do not extend to semisimple products or recognition.", + "outcome": "completed", + "evidence": "PROOF.md proves the all-field theorem. verify.py checks literal covariant tensor coefficients, attaining maps, an exhaustive binary automorphism domain, determinant corrections and semantic controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "What is the exact image for products of full matrix algebras over finite extensions?", + "why_it_matters": "It would extend the promise class to noncommutative semisimple algebras.", + "first_step": "Derive one extension-field block character, then account for determinants of permutations of identical blocks.", + "blocked_by": "Extension-field Frobenius and block-permutation characters have not been derived here." + }, + { + "question": "Can a raw tensor in this class be recognized with a multiplication chart and transporter?", + "why_it_matters": "The present extraction assumes class membership; constructive transport correction needs a chart.", + "first_step": "Compute the three nuclei and test whether their simple module actions recover the matrix-algebra factors.", + "blocked_by": "A complete recognition and chart-recovery proof is missing." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19214431", + "upstream_refresh": { + "commit": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "priority_revision": 8, + "utc": "2026-10-27T10:12:38.993668+00:00" + }, + "preserved_checkout": { + "branch": null, + "head": "de5ec2e7a6074068452f45b1a191b5c72832df4a", + "state": "clean detached HEAD" + }, + "overlap_coverage": { + "open_prs": 418, + "discussion_records": 5316, + "local_note_coverage": "incomplete sparse checkout; distinctive origin/main README searches also run", + "live_at": "2026-10-27T10:11:19.871427+00:00" + } +} diff --git a/research/matrix-tensor-determinant-image/VERIFY.json b/research/matrix-tensor-determinant-image/VERIFY.json new file mode 100644 index 0000000000..4a1a6c89bb --- /dev/null +++ b/research/matrix-tensor-determinant-image/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "All-field theorem finite corroboration: literal covariant tensor action, image attainment, complete binary automorphism census, SL corrections and semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same explicit contracts and semantic controls with assertions disabled." + } + ] +} diff --git a/research/matrix-tensor-determinant-image/verify.py b/research/matrix-tensor-determinant-image/verify.py new file mode 100644 index 0000000000..532fa1b951 --- /dev/null +++ b/research/matrix-tensor-determinant-image/verify.py @@ -0,0 +1,324 @@ +#!/usr/bin/env python3 +"""Exact finite corroboration of the matrix-algebra determinant theorem.""" + +import hashlib +import itertools +import json +import math +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +class Field: + """The seven fixed small fields used by this verifier.""" + + def __init__(self, q): + configs = {2: (2, (0, 1)), 3: (3, (0, 1)), + 4: (2, (1, 1, 1)), 5: (5, (0, 1)), + 7: (7, (0, 1)), 8: (2, (1, 1, 0, 1)), + 9: (3, (1, 0, 1))} + require(q in configs, "unsupported field") + self.q = q + self.p, self.modulus = configs[q] + self.e = len(self.modulus) - 1 + self.add = tuple(tuple(self.add_raw(a, b) for b in range(q)) + for a in range(q)) + self.mul = tuple(tuple(self.mul_raw(a, b) for b in range(q)) + for a in range(q)) + self.neg = tuple(next(b for b in range(q) if self.add[a][b] == 0) + for a in range(q)) + self.inv = (0,) + tuple(next(b for b in range(1, q) + if self.mul[a][b] == 1) + for a in range(1, q)) + + def digits(self, a): + return [(a // self.p**i) % self.p for i in range(self.e)] + + def add_raw(self, a, b): + x, y = self.digits(a), self.digits(b) + return sum(((x[i] + y[i]) % self.p) * self.p**i + for i in range(self.e)) + + def mul_raw(self, a, b): + x, y = self.digits(a), self.digits(b) + c = [0] * (2 * self.e - 1) + for i, j in itertools.product(range(self.e), repeat=2): + c[i + j] = (c[i + j] + x[i] * y[j]) % self.p + for k in range(2 * self.e - 2, self.e - 1, -1): + for j in range(self.e): + c[k - self.e + j] = (c[k - self.e + j] + - c[k] * self.modulus[j]) % self.p + return sum(c[i] * self.p**i for i in range(self.e)) + + def power(self, a, exponent): + require(0 <= exponent <= 128, "unsupported exponent") + value = 1 + for _ in range(exponent): + value = self.mul[value][a] + return value + + +def identity(n): + require(1 <= n <= 9, "unsupported matrix size") + return tuple(int(i == j) for i in range(n) for j in range(n)) + + +def product(a, b, n, f): + out = [0] * (n * n) + for i, j, k in itertools.product(range(n), repeat=3): + out[i * n + j] = f.add[out[i * n + j]][ + f.mul[a[i * n + k]][b[k * n + j]]] + return tuple(out) + + +def inverse_det(a, n, f): + require(len(a) == n * n and 1 <= n <= 9, "invalid square matrix") + rows = [list(a[i * n:(i + 1) * n]) + list(identity(n)[i * n:(i + 1) * n]) + for i in range(n)] + determinant = 1 + for col in range(n): + pivot = next((r for r in range(col, n) if rows[r][col]), None) + if pivot is None: + return None, 0 + if pivot != col: + rows[col], rows[pivot] = rows[pivot], rows[col] + determinant = f.neg[determinant] + scale = rows[col][col] + determinant = f.mul[determinant][scale] + rows[col] = [f.mul[x][f.inv[scale]] for x in rows[col]] + for r in range(n): + if r != col: + coefficient = rows[r][col] + rows[r] = [f.add[x][f.neg[f.mul[coefficient][y]]] + for x, y in zip(rows[r], rows[col])] + return tuple(x for row in rows for x in row[n:]), determinant + + +def matrix_basis(n): + return tuple(tuple(int(j == i) for j in range(n * n)) + for i in range(n * n)) + + +def linear_map(columns): + d = len(columns) + return tuple(columns[j][i] for i in range(d) for j in range(d)) + + +def apply_map(a, x, f): + d = len(x) + out = [0] * d + for i, j in itertools.product(range(d), repeat=2): + out[i] = f.add[out[i]][f.mul[a[i * d + j]][x[j]]] + return tuple(out) + + +def transpose(a, d): + return tuple(a[j * d + i] for i in range(d) for j in range(d)) + + +def autotopy(a, b, p, n, f): + pinv, dp = inverse_det(p, n, f) + require(dp != 0, "singular conjugator") + sigma = tuple(product(product(p, x, n, f), pinv, n, f) + for x in matrix_basis(n)) + fm = linear_map(tuple(product(a, x, n, f) for x in sigma)) + gm = linear_map(tuple(product(x, b, n, f) for x in sigma)) + hm = linear_map(tuple(product(product(a, x, n, f), b, n, f) + for x in sigma)) + return fm, gm, hm + + +def check_autotopy(maps, n, f): + fm, gm, hm = maps + d = n * n + determinants = tuple(inverse_det(a, d, f)[1] for a in maps) + require(all(determinants), "singular autotopy") + for x, y in itertools.product(matrix_basis(n), repeat=2): + lhs = product(apply_map(fm, x, f), apply_map(gm, y, f), n, f) + rhs = apply_map(hm, product(x, y, n, f), f) + require(lhs == rhs, "basis-product failure") + return tuple(f.inv[determinants[i]] if i < 2 else determinants[i] + for i in range(3)) + + +def covariant_maps(maps, n, f): + d = n * n + return (transpose(inverse_det(maps[0], d, f)[0], d), + transpose(inverse_det(maps[1], d, f)[0], d), maps[2]) + + +def literal_tensor_check(maps, n, f): + """Transform all coefficients of mu in A* tensor A* tensor A.""" + s, t, h = maps + d = n * n + for i, j, k in itertools.product(range(d), repeat=3): + value = 0 + for a, b, c in itertools.product(range(n), repeat=3): + term = f.mul[f.mul[s[i * d + a * n + b]][ + t[j * d + b * n + c]]][h[k * d + a * n + c]] + value = f.add[value][term] + expected = int(i % n == j // n and k == (i // n) * n + j % n) + require(value == expected, "literal covariant tensor failure") + return d**3 + + +def predicted_image(n, f): + powers = {f.power(a, n) for a in range(1, f.q)} + return {(u, v, f.inv[f.mul[u][v]]) for u in powers for v in powers} + + +def equation_image(n, f): + exponent = (f.q - 1) // math.gcd(n, f.q - 1) + return {(u, v, w) for u, v, w in itertools.product(range(1, f.q), repeat=3) + if f.power(u, exponent) == f.power(v, exponent) == 1 + and f.mul[f.mul[u][v]][w] == 1} + + +def diagonal(value, n): + a = list(identity(n)) + a[0] = value + return tuple(a) + + +def attaining_fixtures(f): + report = [] + for n in range(1, 4): + images = set() + coefficients = 0 + for alpha, beta in itertools.product(range(1, f.q), repeat=2): + p = list(identity(n)) + if n > 1: + p[0], p[-1] = alpha, beta + p[1] = f.add[alpha][beta] + maps = autotopy(diagonal(alpha, n), diagonal(beta, n), tuple(p), n, f) + triple = check_autotopy(maps, n, f) + coefficients += literal_tensor_check(covariant_maps(maps, n, f), n, f) + images.add(triple) + require(triple == (f.inv[f.power(alpha, n)], + f.inv[f.power(beta, n)], + f.power(f.mul[alpha][beta], n)), "character") + expected = predicted_image(n, f) + require(images == expected == equation_image(n, f), "image mismatch") + g = math.gcd(n, f.q - 1) + orbit_count = (f.q - 1)**3 // len(images) + require(orbit_count == (f.q - 1) * g * g, "SL orbit count") + report.append({"q": f.q, "n": n, "stabilizers": (f.q - 1)**2, + "literal_tensor_coefficients": coefficients, + "image": sorted(images), "sl_orbits": orbit_count}) + return report + + +def is_automorphism(a, n, f): + if apply_map(a, identity(n), f) != identity(n): + return False + for x, y in itertools.product(matrix_basis(n), repeat=2): + if apply_map(a, product(x, y, n, f), f) != product( + apply_map(a, x, f), apply_map(a, y, f), n, f): + return False + return True + + +def binary_automorphism_census(): + f = Field(2) + automorphisms = set() + invertible = 0 + for entries in itertools.product(range(2), repeat=16): + _, determinant = inverse_det(entries, 4, f) + if determinant: + invertible += 1 + if is_automorphism(entries, 2, f): + automorphisms.add(entries) + inner = set() + for p in itertools.product(range(2), repeat=4): + pinv, determinant = inverse_det(p, 2, f) + if determinant: + inner.add(linear_map(tuple(product(product(p, x, 2, f), pinv, 2, f) + for x in matrix_basis(2)))) + require(automorphisms == inner and len(inner) == 6, "complete automorphism census") + require(invertible == 20160, "complete GL4 census") + return {"candidate_maps": 65536, "invertible_maps": invertible, + "automorphisms": len(automorphisms)} + + +def correction_fixtures(f): + counts = {"determinant_triples": 0, "correctable": 0, "rejected": 0} + n = 2 + image = predicted_image(n, f) + for d1, d2, d3 in itertools.product(range(1, f.q), repeat=3): + counts["determinant_triples"] += 1 + roots1 = [x for x in range(1, f.q) if f.power(x, n) == d1] + roots2 = [x for x in range(1, f.q) if f.power(x, n) == d2] + condition = bool(roots1 and roots2 and f.mul[f.mul[d1][d2]][d3] == 1) + require(condition == ((f.inv[d1], f.inv[d2], f.inv[d3]) in image), + "correction criterion") + if not condition: + counts["rejected"] += 1 + continue + counts["correctable"] += 1 + maps = autotopy(diagonal(roots1[0], n), diagonal(roots2[0], n), + identity(n), n, f) + s = covariant_maps(maps, n, f) + for factor, target in zip(s, (d1, d2, d3)): + g = diagonal(target, n * n) + require(inverse_det(product(g, factor, n * n, f), n * n, f)[1] == 1, + "SL correction witness") + return {"q": f.q, **counts} + + +def controls(): + f = Field(7) + maps = autotopy(diagonal(2, 2), identity(2), identity(2), 2, f) + raw = tuple(inverse_det(a, 4, f)[1] for a in maps) + correct = check_autotopy(maps, 2, f) + require(raw == (4, 1, 4) and correct == (2, 1, 4), "inverse convention control") + require(raw not in predicted_image(2, f), "raw determinants falsely admitted") + require((3, 1, 5) not in predicted_image(2, f), "nth-power restriction omitted") + require((2, 1, 2) not in predicted_image(2, f), "product restriction omitted") + require(len(predicted_image(2, Field(3))) == 1, "even-n restriction") + require(len(predicted_image(3, Field(4))) == 1, "extension-field restriction") + require(predicted_image(1, Field(4)) == equation_image(1, Field(4)), "n=1") + require(predicted_image(3, Field(2)) == {(1, 1, 1)}, "q=2") + bad = list(covariant_maps(maps, 2, f)) + bad[2] = identity(4) + rejected = False + try: + literal_tensor_check(tuple(bad), 2, f) + except ValueError: + rejected = True + require(rejected, "altered output tensor survived") + for q, n in ((6, 1), (2, 0), (2, 10)): + rejected = False + try: + identity(n) if q == 2 else Field(q) + except ValueError: + rejected = True + require(rejected, "unsupported domain survived") + return 12 + + +def main(): + fields = tuple(Field(q) for q in (2, 3, 4, 5, 7, 8, 9)) + for f in fields: + for a, b, c in itertools.product(range(f.q), repeat=3): + require(f.mul[a][f.add[b][c]] == f.add[f.mul[a][b]][f.mul[a][c]], + "field distributivity") + report = {"claim_type": "scoped proof with finite corroboration", + "attainment": [r for f in fields for r in attaining_fixtures(f)], + "binary_census": binary_automorphism_census(), + "corrections": [correction_fixtures(f) for f in fields], + "controls": controls()} + root = Path(__file__).resolve().parent + report["package_sha256"] = { + name: hashlib.sha256((root / name).read_bytes()).hexdigest() + for name in ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "verify.py")} + print(json.dumps(report, sort_keys=True)) + print("PASS_MATRIX_TENSOR_DETERMINANT_IMAGE no_new_kappa") + + +if __name__ == "__main__": + main()