[apoursh]

This resolves the supplied-decomposition split-product part of the open question in #5637. For a product of Frobenius-truncated local algebras, the package proves the exact automorphism determinant subgroup and covariant tensor-stabilizer image, verifies supplied three-factor certificates, and constructs determinant-one transporters between equal-label tensors. No new κ is claimed.

For component j of dimension N_j=p^(sum h_ji), set E_ji=N_j(p^h_ji−1)/2. Let g be the gcd of q−1 and all E_ji, also including (q−1)/2 when q is odd and an isomorphism type repeats. Then the covariant stabilizer image is exactly
{(u,v,w): (uvw)^((q−1)/g)=1}, and the GL orbit contains g special-linear orbits. Only isomorphic components may be permuted; equal dimension is insufficient. Supplied component order is normalized with its actual determinant sign.

For example, F3[x]/x^9 has trivial automorphism determinant image and two SL orbits, while its square admits a determinant −1 block swap and has one. Unit witnesses vary a scalar on one component: the total product dimension need not be coprime to q−1.

Proof, implementation and independent checker, scope and next questions.

Verification

At exact head b5e6e7c45f606d639d102570f9fab257e1d0d393, CPython 3.12.14:

• Complete small domains: 40,487 matrices, 22,854 invertible matrices, 23 automorphisms, and 2,372 normalized autotopisms.
• Complete local substitution domains: 4,374 maps for F3[x]/x^9 and 500 for F5[x]/x^5.
• Moderate determinant triples: 44 accepted / 36 rejected. Literal covariant coefficient checks: 104 accepted / 176 rejected; nonlinear controls detect missing input transposes.
• Twelve malformed/changed certificates rejected; independent factor bases, component-order normalization, and positive/negative SL transport checks pass.
• Registered normal and isolated optimized replays pass. Committed-byte/source-history preflight and official export integrity pass.
• Both direct commands reproduce identical reports from the read-only Git-free export; all 11 exported files retain their bytes and modes. Archive SHA256: 97e3ee501a311319d32bec50bd7d517e069633f290f9e7c199830e92df31be28.

python3.12 -B scripts/research_package.py --package research/frobenius-product-characters
python3.12 -B scripts/check_research_commit.py --package research/frobenius-product-characters --check-source-history

Scope and collaboration

Seven new files in one opt-in package; no shared code, selected frontier, or predecessor changes. Base df0137efd35e11b4445734bf612bdd4c7ebc330c, priority revision 7; canonical upstream was refreshed before work and before publication. Discussion #5655 records the advance claim and links the predecessor handoff.

The formal-interface-lemma card is explicitly marked changed to a written algebraic interface proof and exact finite verification. The theorem covers finite fields; the executable covers prime fields and requires supplied factor types and maps. Arbitrary tensor recognition, nonsplit residue fields, physical realization and a paid supplier remain open. There is no independent human review, proof-kernel acceptance, selected cold replay or literature-priority claim.

Local checks are separate from hosted CI. At this base, a shared planning failure from two missing selected-result links in docs/ci-verification.md is already reported upstream. This PR does not claim that hosted planning is green.

Prepared by apoursh, with substantial OpenAI Codex assistance, including separate proof/implementation/checker work. Credit Ali Romman (#5459 local characters and #5637 product handoff), apoursh (#5502 height criterion), Nick Petalas (#5252 normalization/etale precedent), David Ganz and the retained atlas lineage. Three retained proof sources are pinned and authenticated; no pending executable is imported. Apache-2.0.