Compute tensor determinant characters for unequal Frobenius cutoffs

research/frobenius-tensor-characters/README.md

@@ -0,0 +1,160 @@
+# Determinant characters for Frobenius-truncated local algebras
+
+This package extends the promised tensor class in PR5316 to multivariable local
+algebras with unequal characteristic-power cutoffs. It derives the full
+stabilizer determinant image and the resulting special-linear orbit count.
+It is an algebraic interface result. The complete kappa calculation is unchanged.
+
+## The algebra and character formula
+
+Let K=F_q have characteristic p. Choose r>=1 integers e_i>=1, set n_i=p^e_i,
+and let
+
+```
+A = K[x_1,...,x_r] / (x_i^n_i for every i),
+N = product_i n_i,
+E_i = N (n_i-1) / 2,
+h = gcd(q-1,E_1,...,E_r).
+```
+
+Each E_i is an integer. Let mu in A* tensor A* tensor A be multiplication,
+with the ordinary covariant action on its three tensor factors. Then
+
+```
+Delta(mu) = {(u,v,w) in (K*)^3 : (u v w)^((q-1)/h) = 1}.
+```
+
+The image has (q-1)^3/h elements. The one GL orbit splits into exactly h
+orbits under the product of the three special linear groups. These statements
+hold after independent changes of basis in all three tensor factors.
+They assume the tensor belongs to this algebra's GL orbit. They do not
+recognize that orbit or produce a transporter.
+
+For equal e_i=1 and odd p, h=(p-1)/2, independent of r and the extension degree
+of K. For p=2 and e_i=1, h=1. Unequal or higher cutoffs can change the image:
+over F4, the univariate cutoff four has h=3, whereas two cutoff-two variables
+have h=1. Both algebras have dimension four, but their determinant images differ.
+
+## Automorphisms must preserve the height flag
+
+Write J for the radical. Every automorphism induces an invertible map L on J/J
+squared. If the image of x_i has a nonzero linear x_j term, then e_j<=e_i.
+Indeed the p^e_i power of that linear term gives a nonzero x_j^(p^e_i) term
+when e_j>e_i. Frobenius removes mixed terms. Terms of degree at least two have
+power degree at least 2p^e_i and cannot cancel that term. Thus L preserves the
+flag given by the spans of variables of height at most e.
+
+Conversely, every invertible flag-preserving linear substitution respects all
+relations: each allowed x_j has n_j dividing n_i. Its inverse preserves the same
+flag and relations, so it is an algebra automorphism. More generally, a valid
+substitution with invertible tangent map is an automorphism by the finite
+radical filtration. Validity of the relations remains a separate condition;
+an invertible tangent matrix alone does not authorize forbidden height mixing.
+
+An automorphism and its linear substitution induce the same map on the
+associated graded algebra. Ordering monomials by total degree therefore shows
+that they have equal determinants. Higher terms do not change the determinant.
+
+## Compute the automorphism and unit characters
+
+A diagonal change x_i -> c x_i has determinant c^E_i. The sum of the x_i
+exponents over all N monomials is N(n_i-1)/2. An allowed elementary change
+x_i -> x_i+c x_j has determinant one: order monomials by the x_i exponent;
+every new term has a smaller exponent, and the diagonal stays one. The
+flag-preserving linear group is generated by these elementary changes and
+diagonal changes. Within an equal-height block, they generate its full GL group.
+If L_e is the tangent block for height e, this proves
+
+```
+det(sigma) = product_e det(L_e)^(N(p^e-1)/2).
+```
+
+Independent diagonal scalings attain all products of these power subgroups.
+Since K* is cyclic, the exact automorphism determinant image is H_h={c^h:c in K*}.
+No determinant of a formal untwisted group algebra is used.
+
+For a unit a, multiplication by a is triangular on the radical filtration
+with constant diagonal a_0. Thus det(L_a)=a_0^N. Since N is a power of p,
+N is coprime to q-1, so these unit determinants fill K*.
+
+The classical unital commutative autotopism normalization, retained in PR5316
+and PR5252, writes every F(x)G(y)=H(xy) as
+
+```
+F=L_a sigma, G=L_b sigma, H=L_(ab) sigma.
+```
+
+For completeness, evaluate at 1 to get H(x)=F(x)b=aG(x), where a=F(1), b=G(1).
+Bijectivity makes both multiplication maps bijective, hence a,b are units.
+Then sigma=(ab)^-1 H is an algebra automorphism. The converse follows by
+multiplication. The covariant tensor action uses (F^-T,G^-T,H). If x,y are the
+unit determinants and z the automorphism determinant, its ordered triple is
+
+```
+(u,v,w) = (x^-1 z^-1, y^-1 z^-1, x y z).
+```
+
+The inverse equations x=vw, y=uw, z=(uvw)^-1 prove the displayed image formula.
+Conjugation preserves determinants under independent basis changes. Finally,
+the product SL group is the kernel of the determinant map from the product GL
+group; its orbits in the fixed GL orbit are the cosets of Delta(mu). This proves
+the image size and orbit count.
+
+The promised character equation can be computed without constructing A. To
+compute E_i modulo m=q-1, multiply p^(sum e_i) and p^e_i-1 modulo 2m, then
+halve the even residue. Use modular powers and gcd. This uses polynomially
+many bit operations in the supplied parameter sizes and avoids constructing
+the potentially huge integer N. The characteristic and algebra-class promise
+are inputs; this calculation does not factor q or recognize a tensor.
+
+## Evidence and reproduction
+
+```sh
+python3.12 -B scripts/research_package.py --package research/frobenius-tensor-characters
+```
+
+The standalone Python 3.12 checker uses its standard library. It implements F4
+as F2[t]/(t squared+t+1), as well as prime fields. It builds literal quotient
+multiplication tables and substitution matrices, checks all defining power
+relations, compares ambient determinants with the tangent-block formula, and
+checks basis products. Three complete automorphism domains include nonlinear
+substitutions and unequal heights. Additional bounded domains check elementary
+linear and nonlinear maps through algebra dimension 49. Unit multiplication
+matrices and the full determinant-triple sets are checked independently.
+
+Controls distinguish forbidden height mixing, equal dimensions with different
+images, the inverse-input convention, and modular exponent extraction. Normal
+and optimized checks use explicit exceptions. The written proof supplies the
+general finite-field theorem; finite matrix checks are corroboration, not
+proof-kernel verification. No predecessor executable is imported.
+
+## Sources and scope
+
+The direct handoff is [PR #5316](https://github.com/CrocSwap/integer-mult-bounds/pull/5316)
+and its [pinned univariate proof](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/truncated-tensor-characters/README.md).
+Nick Petalas's [PR #5252](https://github.com/CrocSwap/integer-mult-bounds/pull/5252)
+and [finite-etale proof](https://github.com/CrocSwap/integer-mult-bounds/blob/32890bc5de034ab8fc93ac88ead7279a6a416d04/research/etale-tensor-determinant-image/README.md)
+retain the normalization and inverse-input convention. David Ganz's atlas
+retains the character-equation and tensor-action framework. Sources are pinned
+as provenance in SOURCES.json. The all-state multivariable/determinant search
+and full tracked-note/Discussion search found no same height-flag result;
+unposted work and arbitrary historical diffs remain outside coverage.
+
+## Open next questions
+
+A next useful task is recognition of this promised algebra class from a
+multiplication tensor, with a verified transporter. Start with its radical
+filtration and recover the allowed height flag. A field factorization and
+basis-recovery algorithm with complete correctness bounds is still missing.
+Physical coefficient preparation, native realization, movement, precision and
+supplier admission remain separate and unpriced. No selected cold replay,
+Lean, Docker, independent human review or new multiplication theorem is claimed.
+
+## Credit
+
+Ali Romman's PR5316 supplies the univariate method and explicit multivariable
+question. Nick Petalas (@petalas) supplies the finite-etale normalization and
+nilpotent follow-up. David Ganz and the atlas sources retain their attribution.
+Finite local-algebra filtrations, elementary generators and cyclic power
+subgroups are classical. New proof and checks by Ali Romman with substantial
+OpenAI Codex assistance; Apache-2.0. No general literature-priority claim is made.

research/frobenius-tensor-characters/SOURCES.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446",
+      "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/truncated-tensor-characters/README.md",
+      "usage": "provenance",
+      "git_blob": "9dac5ac07eb867ff2ff44bd8f033d0ac1114fb82",
+      "sha256": "2ebd7660dc342ea7a20c3c67dd58530b8ebf3d224ca13c5f689956338d3a32d7"
+    },
+    {
+      "path": "research/etale-tensor-determinant-image/README.md",
+      "usage": "provenance",
+      "git_blob": "0f07df6ce2a8c43ea1fcc5f0081ee3532da28208",
+      "sha256": "2ec18042a1a63d5fd5da246f4f6060c5fb66cff338f25a2a1b95e3ea8b4f0fba"
+    }
+  ]
+}

research/frobenius-tensor-characters/TASK.json

@@ -0,0 +1,95 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04",
+  "original_card": {
+    "id": "formal-interface-lemma",
+    "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?",
+    "starting_points": [
+      "docs/research/research-family-status.md",
+      "certificates/selected-result.json",
+      "research/gate-operand-parity-lean/README.md",
+      "research/staged544-certified-endpoint/README.md",
+      "research/unconditional-batched-crt/README.md"
+    ],
+    "methods": [
+      "Formalize a missing boundary lemma identified by the selected review.",
+      "Audit a formal theorem-to-certificate binding independently."
+    ],
+    "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.",
+    "first_step": {
+      "command": [
+        "python3",
+        "-B",
+        "scripts/research_baseline.py"
+      ],
+      "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY",
+      "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.",
+      "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately."
+    },
+    "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.",
+    "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.",
+    "allowed_variations": [
+      "Narrow to one formal lemma or one theorem-to-certificate binding."
+    ],
+    "scope_change_triggers": [
+      "Formalizing already-covered arithmetic and claiming the full multiplication theorem."
+    ],
+    "overlap_terms": [
+      "hyperplane end",
+      "formal interface",
+      "Lean binding",
+      "3807",
+      "3857",
+      "4100",
+      "gate-operand-parity-lean",
+      "staged544-certified-endpoint",
+      "unconditional-batched-crt"
+    ],
+    "existing_checks": [
+      {
+        "scope": "PR #3807: scoped gate-operand parity formalization.",
+        "evidence": "research/gate-operand-parity-lean/README.md",
+        "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.",
+        "status": "author-checked",
+        "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #3857: certified real-power moment/endpoint arithmetic.",
+        "evidence": "research/staged544-certified-endpoint/README.md",
+        "remaining": "Uniform algorithmic implications, not another endpoint digit.",
+        "status": "author-checked",
+        "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      },
+      {
+        "scope": "PR #4100: compact-switch formalization proposed as future validation.",
+        "evidence": "research/unconditional-batched-crt/README.md",
+        "remaining": "Audit the statement and assumptions before a formal proof campaign.",
+        "status": "author-checked",
+        "source_commit": "337d04939571a637aeab54a0f58f54fde811663a",
+        "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"
+      }
+    ]
+  },
+  "scope_status": "changed",
+  "actual_scope": "Exact stabilizer determinant image for multivariable characteristic-power truncated polynomial algebras, with unequal heights.",
+  "scope_change_reason": "Take PR5316 multivariable handoff as a written algebraic interface theorem and exact checker.",
+  "bottleneck_link": "Extend the promised tensor-character class while preserving the inverse-input convention and nilpotent relations.",
+  "budget_minutes": 60,
+  "stop_rule": "Prove characters and check finite substitutions; do not claim tensor recognition or a physical supplier.",
+  "outcome": "completed",
+  "evidence": "README.md proof; verify.py literal algebra, automorphism, unit and determinant-image checks.",
+  "author": "Ali Romman",
+  "ai_assistance": "Substantial OpenAI Codex assistance.",
+  "open_questions": [
+    {
+      "question": "Can this algebra class be recognized from its multiplication tensor with a transporter?",
+      "why_it_matters": "It would remove the current orbit promise.",
+      "first_step": "Recover the radical filtration and candidate height flag.",
+      "blocked_by": "No complete basis-recovery and recognition algorithm is supplied."
+    }
+  ]
+}

research/frobenius-tensor-characters/VERIFY.json

@@ -0,0 +1,30 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact substitution matrices, complete small automorphism domains, unit characters and covariant triples."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-B",
+        "-O",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 120,
+      "checks": "Exact substitution matrices, complete small automorphism domains, unit characters and covariant triples."
+    }
+  ]
+}