Prove exact square-zero tensor determinant images (no κ)

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.

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.

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"
+    }
+  ]
+}