Extend Frobenius tensor characters to split products

research/frobenius-product-characters/README.md

@@ -0,0 +1,170 @@
+# Determinant characters for split Frobenius products
+
+This package extends the local-algebra character interface to a nonempty finite
+product of Frobenius-truncated local algebras. It supplies a written proof,
+explicit prime-field determinant witnesses, and a checker for a supplied
+three-factor tensor certificate. It does not discover that certificate from an
+arbitrary tensor. The selected multiplication bound is unchanged.
+
+The direct next question is the product/component-matching handoff in Ali
+Romman's [PR #5637](https://github.com/CrocSwap/integer-mult-bounds/pull/5637),
+at `86389e525d3efafe236e929f6ae401c68be1d115`. The
+[canonical investigation](https://github.com/CrocSwap/integer-mult-bounds/discussions/5655)
+records the claim and public status. Base is
+`df0137efd35e11b4445734bf612bdd4c7ebc330c`, priority revision 7.
+The selected conditional kappa at that base is `62009/20000000`.
+
+## Result
+
+Let K=F_q have characteristic p and let
+
+```
+A = product_j B_j,
+B_j = K[x_1,...,x_sj]/(x_i^(p^h_ji)),   h_ji >= 1,
+N_j = p^(sum_i h_ji),
+E_ji = N_j (p^h_ji-1)/2.
+```
+
+The empty height list means B_j=K. Each factor type is its sorted height list.
+Let g be the gcd of q-1 and all E_ji, additionally including (q-1)/2 when q
+is odd and some factor type occurs at least twice. Then
+
+```
+det Aut_K(A) = {c^g : c in K*},
+Delta(mu_A) = {(u,v,w) in (K*)^3 : (uvw)^((q-1)/g) = 1}.
+```
+
+Here Delta uses the covariant action on `A* tensor A* tensor A`. The GL orbit
+of this tensor splits into exactly g orbits under SL x SL x SL.
+[PROOF.md](PROOF.md) gives the component decomposition, local characters,
+permutation signs, unit determinants, and autotopism normalization.
+
+Two distinctions are essential. Exponents use each **local** dimension N_j,
+not the total dimension. Component permutations are allowed only between
+isomorphic factors, not arbitrary equal-dimensional factors. For example,
+over F3 the local algebra F3[x]/x^9 has trivial automorphism determinant image,
+but the product of two copies acquires determinant -1 by exchanging them.
+The dimension-nine factors with heights (2) and (1,1) are not isomorphic.
+
+Even when the total dimension is not coprime to q-1, unit determinants still
+fill K*: vary a scalar on one component, whose dimension is a power of p.
+Using a single common scalar on the whole product would miss valid witnesses.
+
+## Supplied-certificate contract
+
+The executable accepts prime fields only; the written theorem covers all finite
+fields. It uses canonical residues 0,...,p-1, exact integer arithmetic, and
+standard-library Python. Matrices act on column vectors. A tensor is indexed
+by `tensor[i][j][k]`, with k the output coordinate.
+
+For a supplied product model and invertible matrices U,V,W, the checker tests
+every basis product in
+
+```
+tensor(Ua,Vb) = W mu_A(a,b).
+```
+
+Acceptance verifies the certificate; it is not an algorithm to find U,V,W or
+the component decomposition. Malformed data and incorrect certificates are
+rejected. Heights are sorted inside each component, but supplied component
+order is retained. To compare orbit labels, the checker first identifies this
+order with the canonical lexicographic order of factor types. The determinant
+of that permutation must be included: exchanging different types can change
+an unnormalized coordinate label even though it is not an algebra automorphism
+of the fixed ordered model.
+
+`model.py` exposes `make_model`, `determinant_character`, `automorphism`,
+`autotopism`, `covariant_stabilizer`, `validate_certificate`, and
+`sl_transporter`. Height parameters always define the internally sorted local
+model; supplied matrices must use that model's ordered monomials. The executable
+materializes the algebra and uses field-element enumeration; it makes no
+polynomial bit-complexity claim in binary-encoded heights or log p.
+
+The code constructs automorphism and covariant stabilizer witnesses for every
+admissible determinant request. The inverse-input convention is explicit:
+an autotopism F(a)G(b)=H(ab) acts as `(F^-T,G^-T,H)` on the tensor. It also
+constructs determinant-one maps between certified tensors with equal types
+and canonical orbit labels, checking their determinants and every transported
+basis product.
+
+## Verification
+
+From the repository root, with Python 3.12:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/frobenius-product-characters
+```
+
+For an exported package and its three declared proof-source inputs:
+
+```sh
+python3.12 -I -B research/frobenius-product-characters/verify.py
+python3.12 -I -O -B research/frobenius-product-characters/verify.py
+```
+
+Checks use explicit exceptions and remain active with optimizations enabled.
+`SOURCES.json` pins the exact retained predecessor proof bytes, and the direct
+verifier authenticates their hashes without Git. No predecessor executable is
+imported. Finite enumeration corroborates the proof only in its stated domains;
+it is not proof-kernel verification or independent human review.
+
+The separate checker enumerates all 40,487 matrices across six domains of
+dimension at most three over F2 or F3: 22,854 are invertible and 23 are algebra
+automorphisms. It checks 2,372 normalized autotopisms directly on basis products.
+Separate polynomial substitution oracles exhaust all 4,374 automorphisms of
+F3[x]/x^9 and all 500 automorphisms of F5[x]/x^5. The moderate product tests
+accept 44 determinant triples and reject 36 outside the predicted image.
+
+Literal covariant coefficient-index checks over F5 and F7 accept 104 triples
+and reject 176. Nonlinear substitution controls reject omitting the input
+transpose. Twelve malformed or changed certificate controls are rejected.
+Independent factor bases in dimension nine and component-order normalization
+in dimension ten exercise the supplied-certificate interface; equal-label
+special-linear transport succeeds and unequal-label transport is rejected.
+These are bounded finite domains, not enumeration of all larger product
+algebras. Each direct run takes about one second on the development machine.
+
+The selected-record source-binding orientation passed after materializing its
+sparse inputs. That check did not replay the selected physical construction.
+The written proof and executable were reviewed by separate Codex agents;
+this is AI-assisted internal review, not independent human acceptance.
+
+## Sources, overlap and limitations
+
+Ali Romman's [PR #5459](https://github.com/CrocSwap/integer-mult-bounds/pull/5459)
+supplies the local height-flag character formula; apoursh's
+[PR #5502](https://github.com/CrocSwap/integer-mult-bounds/pull/5502) supplies the
+intrinsic height flag. Nick Petalas's
+[PR #5252](https://github.com/CrocSwap/integer-mult-bounds/pull/5252) supplies
+the finite-etale determinant-image precedent and autotopism normalization.
+Their retained files are pinned at the base in `SOURCES.json`. David Ganz and
+the atlas lineage retain credit for the character/orbit framework. PR #5637
+is the pending handoff source, not an executable dependency of this package.
+
+Overlap checks covered current main guidance, the newest live handoffs and
+bounded all-state PR searches for product/Frobenius/component terms. Sparse
+local notes, arbitrary historical diffs and unpublished work were not completely
+searched. No literature-priority claim follows from those checks.
+`TASK.json` explicitly changes the formal-interface-lemma card to this written
+algebraic interface proof; no Lean formalization is claimed.
+
+## Open next questions
+
+- Recover the product decomposition and three factor maps from an arbitrary
+  tensor. This would remove the supplied-certificate premise. Start with the
+  nucleus regular-module test and primitive idempotents, then apply the local
+  height recognizer. A complete decomposition algorithm and complexity bound
+  remain missing here.
+- Allow nontrivial residue fields. This would cover nonsplit components. First
+  specify field embeddings and isomorphisms and account for their determinants;
+  the current proof assumes every residue field is K.
+- Realize a certified tensor in a named native producer/consumer pair. A bound
+  improvement requires paying representation, coefficients, movement, precision
+  and restoration. No such physical construction or invoice is supplied here.
+
+## Credit
+
+New product proof and implementation: apoursh, with substantial OpenAI Codex
+assistance, including a separate finite checker and proof audit. Predecessor
+methods and notices retain the attribution above. Apache-2.0. No selected cold
+replay, proof-assistant build, or independent human acceptance is claimed.

research/frobenius-product-characters/SOURCES.json

@@ -0,0 +1,36 @@
+{
+  "schema_version": 1,
+  "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c",
+  "files": [
+    {
+      "path": "certificates/selected-result.json",
+      "usage": "provenance",
+      "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8",
+      "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5"
+    },
+    {
+      "path": "docs/research/agent-task-catalog.json",
+      "usage": "provenance",
+      "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602",
+      "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72"
+    },
+    {
+      "path": "research/frobenius-tensor-characters/README.md",
+      "usage": "input",
+      "git_blob": "b62f9a906e6ed49605684cca52a221f064924461",
+      "sha256": "31573ba91ac69caff5b8e5a42ce7fd0d80a6d54673c08d7f225c9ee08e0e0893"
+    },
+    {
+      "path": "research/frobenius-algebra-recognition/PROOF.md",
+      "usage": "input",
+      "git_blob": "0a0b7d1fe48576be453df5aa5de0cc66463352fa",
+      "sha256": "726d9c294f0b4b9085e3994ffb8c93737822b78d6f5d0c63f81e36b718419e28"
+    },
+    {
+      "path": "research/etale-tensor-determinant-image/README.md",
+      "usage": "input",
+      "git_blob": "0f07df6ce2a8c43ea1fcc5f0081ee3532da28208",
+      "sha256": "2ec18042a1a63d5fd5da246f4f6060c5fb66cff338f25a2a1b95e3ea8b4f0fba"
+    }
+  ]
+}

research/frobenius-product-characters/TASK.json

@@ -0,0 +1,110 @@
+{
+  "schema_version": 1,
+  "task_id": "formal-interface-lemma",
+  "priority_revision": 7,
+  "base_commit": "df0137efd35e11b4445734bf612bdd4c7ebc330c",
+  "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": "For split products of Frobenius-truncated local algebras with supplied and checked three-factor maps, prove the component-matching and determinant-character formula and construct exact prime-field witnesses.",
+  "scope_change_reason": "Handoff-first follow-up to PR5637: the local arbitrary-tensor and extension-field cases are already covered. This is a written algebraic interface proof with finite verification, not the card's proof-assistant formalization.",
+  "bottleneck_link": "Algebraic side result: extends the determinant-character interface and SL orbit classification to split products. It does not price any native supplier or alter the selected multiplication bound.",
+  "budget_minutes": 60,
+  "stop_rule": "Stop after a self-contained product proof, explicit prime-field witnesses, independent bounded enumeration and rejection controls, and reproducible package checks; do not broaden to arbitrary tensor recognition or non-split residue fields.",
+  "outcome": "completed",
+  "evidence": "PROOF.md: general finite-field theorem. verify.py: 40487 matrices across six complete tiny GL domains (22854 invertible,23 automorphisms),2372 normalized autotopisms,4374+500 complete local substitutions,44/36 moderate determinant triple accepts/rejects,104/176 covariant accepts/rejects,nonlinear transpose controls,12 certificate mutations. Separate Codex implementation and proof review; no independent human review.",
+  "author": "apoursh",
+  "ai_assistance": "Substantial OpenAI Codex assistance: task selection, proof drafting, implementation and separate finite checker; no independent human or proof-assistant verification.",
+  "open_questions": [
+    {
+      "question": "Recover a split-product decomposition and component transporters from an arbitrary multiplication tensor.",
+      "why_it_matters": "Removes the supplied-decomposition certificate premise from this interface.",
+      "first_step": "Combine the nucleus regular-module test with primitive idempotent recovery, then apply the local height-flag recognizer componentwise and check all products.",
+      "blocked_by": "A complete decomposition algorithm with correctness and complexity guarantees is not supplied here."
+    },
+    {
+      "question": "Extend component matching and characters to nontrivial residue fields.",
+      "why_it_matters": "Covers nonsplit commutative algebras over the ground field.",
+      "first_step": "Specify field embeddings and isomorphisms and compute the determinant contribution of residue-field automorphisms before composing local factors.",
+      "blocked_by": "The split residue-field hypothesis is used throughout this proof and executable."
+    },
+    {
+      "question": "Realize a certified product tensor in a named paid native caller.",
+      "why_it_matters": "A character interface alone cannot improve kappa.",
+      "first_step": "Identify producer and consumer maps and charge representation, coefficients, movement, precision and restoration.",
+      "blocked_by": "No physical construction or complete paid invoice is provided."
+    }
+  ],
+  "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5655",
+  "chooser_seed": "681f0a658111610f1515559fc056b47e",
+  "overlap_coverage": "Current main guidance and selected bindings; newest live handoffs including PR5637; bounded all-state PR searches for product/Frobenius/component terms. Sparse local notes, arbitrary historical diffs and unpublished work remain outside coverage."
+}

research/frobenius-product-characters/VERIFY.json

@@ -0,0 +1,33 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/frobenius-tensor-characters/README.md",
+    "research/frobenius-algebra-recognition/PROOF.md",
+    "research/etale-tensor-determinant-image/README.md"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Exact split-product models, independent finite automorphism enumeration, determinant witnesses, supplied tensor certificates and failure controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "The same explicit checks with isolated imports and Python optimizations enabled."
+    }
+  ]
+}