diff --git a/research/nonsplit-frobenius-characters/PROOF.md b/research/nonsplit-frobenius-characters/PROOF.md
new file mode 100644
index 0000000000..66178c0eb7
--- /dev/null
+++ b/research/nonsplit-frobenius-characters/PROOF.md
@@ -0,0 +1,466 @@
+# Determinant characters for nonsplit Frobenius-truncated products
+
+This note extends the supplied-model character interface to local factors with
+nontrivial finite residue fields. It does not recover an algebra, its factors,
+or three factor maps from an arbitrary tensor. All vector spaces, determinants,
+algebra automorphisms and tensor actions are over one fixed base field K.
+The result is an algebraic interface theorem, not a native implementation or
+an improvement to the selected multiplication bound.
+
+## 1. Models, coordinates and the theorem
+
+Let K=F_q have characteristic p. For each residue degree d occurring in the
+input, fix an explicit field L_d/K of degree d with an ordered K-basis. Use the
+same presentation and basis for every component of that degree. Consider a
+nonempty finite product
+
+$$
+A=\prod_{j=1}^r B_j,\qquad
+B_j=L_{d_j}[x_{j1},\ldots,x_{js_j}]/
+       (x_{ji}^{p^{h_{ji}}}:1\leq i\leq s_j),\qquad h_{ji}\geq1.
+$$
+
+The empty height list is allowed and means B_j=L_{d_j}. Put
+
+$$
+M_j=\dim_{L_{d_j}}B_j=p^{\sum_i h_{ji}},\qquad
+D_j=\dim_K B_j=d_jM_j,\qquad n=\sum_jD_j,
+$$
+
+and define the integer
+
+$$
+E_{ji}=M_j(p^{h_{ji}}-1)/2.
+$$
+
+If p is odd, the second factor is even; if p=2 and a variable is present,
+M_j is even. There is no E exponent for an empty height list. In particular,
+**E uses the dimension M_j over the residue field, not the dimension D_j over K.**
+
+A component's type is (d_j, its sorted height list). Within a component, order
+the monomials lexicographically in their exponent tuples, and within each
+monomial use the fixed ordered K-basis of L_{d_j}. A supplied product may list
+its components in any order. The canonical product model orders their types
+lexicographically. Heights are sorted before defining the local model; supplied
+matrices must refer to that fixed local monomial order.
+
+Let m=q-1. Include a sign exponent T=m/2 precisely when q is odd and at least
+one of these conditions holds:
+
+1. Some residue degree d_j is even.
+2. Some type with odd residue degree occurs at least twice.
+
+Define
+
+$$
+g=\gcd(m,\{E_{ji}\}_{j,i},\ T\text{ if included}),\qquad
+H_g=\{c^g:c\in K^\times\}.
+$$
+
+The gcd of the singleton list (m) is m. When q=2, m=g=1 and H_g={1}.
+
+**Theorem.** For the K-algebra A above,
+
+$$
+\det_K\operatorname{Aut}_K(A)=H_g.
+$$
+
+For its multiplication tensor, with the covariant action on
+A* tensor A* tensor A, the full stabilizer determinant image is
+
+$$
+\Delta(\mu_A)=
+ \{(u,v,w)\in(K^\times)^3:uvw\in H_g\}
+ =\{(u,v,w):(uvw)^{m/g}=1\}.
+$$
+
+Every allowed triple is attained. This image has m^3/g elements, and the GL
+orbit of the multiplication tensor splits into exactly g orbits under
+SL_n(K) x SL_n(K) x SL_n(K). Section 8 gives a complete label for tensors
+with verified maps from the supplied product model, including component-order
+normalization. These statements hold over every finite K; finite executable
+fixtures are corroboration, not the all-dimension proof.
+
+## 2. The coefficient field is intrinsic
+
+Work first with one factor
+$B=L[x_1,\ldots,x_s]/(x_i^{p^{h_i}})$, where L=F_{q^d}.
+Its radical J=(x_1,...,x_s) is nilpotent. An element with nonzero constant term
+is a unit by a finite geometric series; an element in J is nilpotent. Thus B
+is local and B/J=L. Its only idempotents are zero and one: one of e and 1-e is
+a unit, and e(1-e)=0 then determines e.
+
+Set Q=q^d. Inside B, the embedded coefficient field is exactly
+
+$$
+L=\{a\in B:a^Q=a\}.
+$$
+
+Indeed write a=c+j with c in L and j in J. Characteristic-power Frobenius
+gives a^Q=c+j^Q. If a^Q=a then j^Q=j. Iterating this identity eventually kills
+j by nilpotence, so j=0. Conversely every c in L satisfies c^Q=c.
+This also proves uniqueness of a coefficient-field section of B/J: each
+residue has just one lift satisfying that equation.
+
+Every K-algebra automorphism preserves this intrinsic field and restricts to a
+power of the q-Frobenius $\varphi:c\mapsto c^q$ of L/K. Extend varphi to B
+by applying it to coefficients and fixing each variable. It is a K-algebra
+automorphism of order d. Composing any automorphism with the inverse of its
+coefficient Frobenius leaves an L-algebra automorphism. Therefore
+
+$$
+\operatorname{Aut}_K(B)
+ =\operatorname{Aut}_L(B)\rtimes\operatorname{Gal}(L/K).
+$$
+
+There are no additional automorphisms obtained by moving the coefficient field
+through nilpotent directions. The relevant field automorphism is q-Frobenius;
+when K is nonprime, p-Frobenius need not be K-linear.
+
+## 3. Local L-linear characters and restriction of scalars
+
+We give the local filtration argument of Ali Romman's PR5459 over L, then take
+its determinant over K. Let M=dim_L B and write
+
+$$
+V_e=(\ker(a\mapsto a^{p^e})+J^2)/J^2.
+$$
+
+These are L-subspaces, even though the power maps are semilinear. They are
+intrinsic: K-algebra isomorphisms preserve the power equations and J^2, while
+their restriction to L may be semilinear. The monomial basis shows
+
+$$
+V_e=\operatorname{span}_L\{x_i+J^2:h_i\leq e\}.
+$$
+
+To see the reverse inclusion, a nonzero linear term in a variable of height
+greater than e contributes a surviving degree-p^e monomial to the p^e power.
+Other linear terms contribute different monomials, and higher-degree terms
+cannot cancel this monomial. Thus the increments of dim_L V_e recover the
+height multiset. The residue degree and height multiset consequently classify
+the displayed local factors up to K-algebra isomorphism. Equal K-dimension
+alone does not classify them.
+
+An L-algebra automorphism has an invertible tangent map on J/J^2 preserving
+this height flag. Conversely every invertible flag-preserving linear
+substitution defines an algebra automorphism: the image of a height-h variable
+uses only variables of height at most h, so its p^h power is zero. Its inverse
+preserves the same flag and defines the inverse substitution.
+
+A general automorphism and its linear substitution induce the same map on the
+associated graded algebra for J^k. Ordering a monomial basis by total degree
+therefore gives them the same L-determinant. The flag-preserving linear group
+is generated by diagonal scalings and permitted elementary substitutions.
+An elementary substitution x_i -> x_i+c x_k is triangular on monomials ordered
+by the x_i exponent and has determinant one. Scaling x_i -> c x_i has
+L-determinant
+
+$$
+c^{E_i},\qquad
+E_i=\sum_{0\leq a_\ell<p^{h_\ell}}a_i
+   =M(p^{h_i}-1)/2.
+$$
+
+For any L-linear map S on an M-dimensional L-space,
+
+$$
+\det_K S=\operatorname{Norm}_{L/K}(\det_L S).
+$$
+
+For completeness, Gaussian elimination factors an invertible L-matrix into
+elementary matrices, diagonal entries and coordinate swaps. The identity holds
+on an elementary matrix since its K-matrix is block triangular with identity
+diagonal. A diagonal scalar c contributes its norm by the definition of the
+field norm as a multiplication determinant. An L-coordinate swap exchanges
+two K-blocks of size d and has determinant (-1)^d, equal to the norm of -1.
+Multiplicativity proves the formula.
+
+Consequently the K-determinants of the variable scalings are
+
+$$
+\operatorname{Norm}_{L/K}(c)^{E_i}.
+$$
+
+The finite-field norm is onto K*: the cyclic group L* has order q^d-1, and
+the power $(q^d-1)/(q-1)$ has image of order q-1, contained in K*.
+Thus the K-determinant image of Aut_L(B) is generated exactly by
+$\{a^{E_i}:a\in K^\times\}$. The extension degree d introduces a norm,
+not an extra factor d in E_i.
+
+## 4. Coefficient Frobenius and component permutations
+
+The normal basis theorem gives a K-basis
+$\theta,\varphi\theta,\ldots,\varphi^{d-1}\theta$ of L. In that basis
+varphi is a d-cycle, so
+
+$$
+\det_K\varphi=(-1)^{d-1}.
+$$
+
+The coefficient action on B is the direct sum of M such actions, one for each
+monomial. Therefore its determinant is
+
+$$
+(-1)^{M(d-1)}.
+$$
+
+This argument remains valid when the characteristic divides d; a permutation
+matrix still has the stated determinant. The finite-field norm, cyclicity and
+normal basis theorem are classical premises; see J. S. Milne,
+[Fields and Galois Theory](https://www.jmilne.org/math/Books/FT0.pdf), the
+sections on finite fields, normal bases, and norms. The normal basis is used
+to prove the sign, not required as the supplied coordinate basis.
+
+The nonzero primitive idempotents of A are exactly its component identities.
+An algebra automorphism permutes these idempotents and restricts to an
+isomorphism of their local factors. Section 3 shows that only equal types
+(d, sorted heights) can be permuted. Conversely all local automorphisms and
+all permutations among copies of an equal type extend to automorphisms of A;
+these generate its automorphism group.
+
+Swapping two equal factors of K-dimension D=dM exchanges D pairs of matching
+basis vectors, so its determinant is (-1)^D. This is also true for separated
+blocks, by conjugating the swap by a fixed coordinate reordering.
+
+If q is odd then p and M are odd. Coefficient Frobenius contributes -1 exactly
+when d is even, and a factor transposition contributes -1 exactly when d is
+odd. If q is even all signs equal one. Hence the two sign conditions in
+Section 1 are exact. They concern residue Frobenius and permutations of
+isomorphic whole factors, respectively; they must not be conflated.
+
+The determinant generators established so far are the E_ji power images and,
+when present, -1. Writing a generator of K* as zeta, these correspond to
+the integer exponents E_ji and m/2 modulo m. They generate exactly
+$\langle\zeta^g\rangle=H_g$, proving the first assertion of the theorem.
+
+## 5. Unit determinants remain surjective
+
+For a unit a_j in B_j, write its constant term as c_j in L_{d_j}*, so
+a_j=c_j+z_j with z_j in the radical. Multiplication by z_j raises total degree.
+On the monomial filtration, multiplication by a_j has M_j diagonal K-blocks,
+each equal to multiplication by c_j on L_{d_j}. Thus
+
+$$
+\det_K L_a=\prod_j\operatorname{Norm}_{L_{d_j}/K}(c_j)^{M_j}.
+$$
+
+This map from $A^\times$ to $K^\times$ is onto. Choose a single component j, use norm
+surjectivity there, and use gcd(M_j,q-1)=1 to invert the M_j power map on K*;
+put one in every other component. No coprimality involving the total dimension
+n or D_j=d_jM_j is needed. When q=2 the unit one already realizes the only
+possible determinant.
+
+## 6. Normalize autotopisms and obtain the full image
+
+Let invertible K-linear maps F,G,H on A satisfy
+
+$$
+F(x)G(y)=H(xy).
+$$
+
+Put a=F(1), b=G(1). Evaluation at the unit gives
+$H=L_bF=L_aG$, so L_a and L_b are invertible and a,b are units. Set
+$\sigma=L_{ab}^{-1}H$. Then sigma is invertible, sigma(1)=1, and substitution
+in the displayed identity gives sigma(x)sigma(y)=sigma(xy). Hence
+
+$$
+F=L_a\sigma,\qquad G=L_b\sigma,\qquad H=L_{ab}\sigma,
+\quad \sigma\in\operatorname{Aut}_K(A).
+$$
+
+Conversely these formulas define an autotopism for any two units and any
+algebra automorphism. This is the unital commutative normalization retained
+in PR5252 and the split product package.
+
+In the covariant tensor convention, the stabilizer element is
+$(F^{-T},G^{-T},H)$, not (F,G,H). Write
+$x=\det_K L_a$, $y=\det_K L_b$, and $z=\det_K\sigma$. Its determinant
+triple is
+
+$$
+(u,v,w)=(x^{-1}z^{-1},\ y^{-1}z^{-1},\ xyz),\qquad uvw=z^{-1}\in H_g.
+$$
+
+Conversely, given uvw in H_g, set
+
+$$
+z=(uvw)^{-1},\qquad x=vw,\qquad y=uw.
+$$
+
+Sections 4 and 5 provide an automorphism with determinant z and two units
+with multiplication determinants x and y. They realize the requested triple.
+There are m^2 choices for u,v and m/g choices for their allowed product with w,
+giving |Delta|=m^3/g.
+
+The same normalization, with multiplication on the two sides taken in two
+possibly different unital commutative algebras, shows that an invertible
+three-factor isotopy between them induces a K-algebra isomorphism. Therefore
+different type multisets do not become GL-equivalent merely by allowing
+independent input and output bases.
+
+## 7. Attainment is constructive, without a fast-search claim
+
+For z=zeta^k in H_g, choose Bezout coefficients
+
+$$
+g=b_0m+\sum_{j,i}b_{ji}E_{ji}+b_T(m/2),
+$$
+
+omitting the last term when the sign generator is absent. For each variable,
+choose c_ji in L_{d_j}* with
+$\operatorname{Norm}(c_{ji})=\zeta^{b_{ji}k/g}$, and scale that variable by
+c_ji. If necessary, compose with a fixed negative-determinant coefficient
+Frobenius or an allowed component transposition, to the power b_T k/g.
+Determinants multiply to z. Negative integer exponents are allowed because
+these maps are invertible. If H_g={1}, the identity suffices.
+
+For a requested unit determinant x, choose a component j and an integer r
+with r M_j=1 modulo m, then choose c_j with norm x^r. The componentwise unit
+with that constant and ones elsewhere has determinant x. Treat m=1 separately
+by returning the identity. Section 6 then gives every allowed triple.
+
+Explicit finite-field presentations allow finite searches for primitive
+elements, discrete logarithms and norm preimages, followed by exact checks.
+No polynomial bit-complexity assertion in log q or compressed heights follows
+from that observation. This proof does not require a field-isomorphism discovery
+algorithm, a normal-basis construction, or arbitrary tensor recognition.
+
+## 8. Supplied maps, canonical model order and SL labels
+
+Let t:K^n x K^n -> K^n be supplied with a product model and invertible matrices
+U,V,W in the convention
+
+$$
+t(Ua,Vb)=W\mu_A(a,b).
+$$
+
+Checking this equation on all n^2 model basis pairs verifies it for all inputs.
+It is a certificate check, not a method of discovering the model or the maps.
+Matrices act on columns, and all determinants in this section lie in K*.
+
+The executable requires the component types to be in canonical order already
+and uses the supplied residue polynomial's power basis. Thus its accepted
+models have R=I in the normalization below. The general reordering argument is
+a theorem about supplied models, not an assertion that the executable accepts
+unsorted components or discovers missing coordinate maps.
+
+Let R be the basis map from the canonical component order to the supplied
+order, matching complete types and each residue-basis/monomial coordinate.
+Because the residue presentations agree degree by degree, R is a permutation
+matrix and an algebra isomorphism between those two ordered models. Normalize
+the supplied maps to
+
+$$
+U_c=UR,\qquad V_c=VR,\qquad W_c=WR.
+$$
+
+The determinant product of the resulting covariant transporter
+$(U_c^{-T},V_c^{-T},W_c)$ is
+
+$$
+d(t)=\frac{\det W_c}{\det U_c\det V_c}
+    =\frac{\det W}{\det U\det V}\frac1{\det R}.
+$$
+
+The canonical special-linear label is
+
+$$
+\ell(t)=d(t)^{m/g}.
+$$
+
+Moving adjacent blocks of K-dimensions D_i,D_j contributes
+$(-1)^{D_iD_j}$ to det R. This permutation sign must be included even when
+the two types differ: R changes the ordered reference model and need not be
+an automorphism of one fixed ordered model. Merely sorting type metadata and
+leaving the maps unchanged can give the wrong label. Different matchings of
+equal copies change R by an algebra automorphism and leave the label invariant.
+
+To prove completeness, let G=GL_n(K)^3 and S=SL_n(K)^3. The determinant map
+G -> (K*)^3 is onto with kernel S. The S-orbits inside G/Stab(mu_A) are therefore
+classified by (K*)^3/Delta(mu_A). Section 6 identifies this quotient with
+K*/H_g by taking the product of the three determinants. The power
+d -> d^(m/g) has kernel H_g and image of size g. Thus the label is independent
+of the valid supplied certificate, and two certified tensors of the same
+canonical type multiset are SL-equivalent if and only if their labels agree.
+This proves the orbit count as well. It does not assert that the executable
+constructs an SL transporter.
+
+If different explicit presentations of a residue field of the same degree
+are supplied, equality of their degree metadata is not a coordinate map.
+First supply and verify a K-field isomorphism and extend it coefficientwise
+to each monomial. Include that full K-linear model identification in R and
+include its determinant in the normalization above. Abstract existence follows
+from uniqueness of finite fields of a given order, but this interface does not
+discover such isomorphisms. Automorphisms of the base field K are never among
+the allowed K-linear factor maps.
+
+## 9. A nonprime-base discriminant for the missing norm
+
+Take
+
+$$
+K=\mathbb F_3[t]/(t^2+1),\qquad \beta=1+t.
+$$
+
+The polynomial has no root in F3. In K, beta^2=2t and beta^4=-1, so beta has
+order eight and is a nonsquare. Thus
+$L=K[u]/(u^2-\beta)$ is a quadratic field extension and
+$\operatorname{Norm}_{L/K}(u)=-\beta=\beta^5$.
+
+For B=L[x]/(x^3), M=3, D=6 and E=3. The automorphism x -> u x has
+L-determinant u^(0+1+2)=u^3 and K-determinant
+
+$$
+\operatorname{Norm}(u)^3=\beta^{15}=\beta^7.
+$$
+
+This element has order eight, so Aut_K(B) has the full K* determinant image.
+The theorem gives gcd(8,3,4)=1. Erroneously replacing M by D makes E=6 and
+predicts gcd(8,6,4)=2, missing every nonsquare determinant. The coefficient
+Frobenius sign cannot repair that error because -1=beta^4 is already a square.
+This fixture distinguishes the nonsplit nilpotent calculation from either
+the split local formula alone or the finite-etale sign formula alone.
+
+It also distinguishes q-Frobenius from p-Frobenius: here q=9 and p=3.
+The map c -> c^3 sends t to -t and does not fix K pointwise, whereas the
+coefficient map c -> c^9 is the K-linear generator of Gal(L/K).
+
+## 10. Provenance, limits and open questions
+
+The retained inputs and their exact heads are:
+
+- Ali Romman's [PR5459](https://github.com/CrocSwap/integer-mult-bounds/pull/5459),
+  `bef3575ddb19c44434a7e2460a353eac7c4d9387`,
+  `research/frobenius-tensor-characters/README.md`: the local height flag,
+  triangular determinant argument and local exponents over the coefficient field.
+- apoursh's [PR5656](https://github.com/CrocSwap/integer-mult-bounds/pull/5656),
+  `b5e6e7c45f606d639d102570f9fab257e1d0d393`,
+  `research/frobenius-product-characters/PROOF.md`: the split product interface,
+  type matching, component-order normalization and supplied-certificate labels.
+- Nick Petalas's [PR5252](https://github.com/CrocSwap/integer-mult-bounds/pull/5252),
+  `07e6f55d18d2d3fd6dcea19bd642d71657c5fe14`,
+  `research/etale-tensor-determinant-image/README.md`: finite-etale residue signs,
+  norm surjectivity and autotopism normalization.
+
+Ali Romman's PR5637 at `86389e525d3efafe236e929f6ae401c68be1d115` also retains
+credit for field and linear-algebra helpers reused by the executable. David
+Ganz and the retained atlas lineage retain credit for the character/orbit
+framework. Norms, restriction of scalars, normal bases and local filtrations
+are classical algebra; no general literature-priority claim is made.
+
+This contribution combines nontrivial residue fields and nilpotent truncations
+in the supplied product interface. It does not perform the separately claimed
+arbitrary-tensor/product-recognition task, recover field presentations, or
+import a pending recognition executable as a mathematical premise.
+
+Open next questions are to recover nonsplit factors and compatible residue-field
+maps from an arbitrary tensor, and to give efficient witness construction with
+explicit complexity guarantees in variable field size. A physical application
+would additionally require coefficient preparation, native representation,
+movement, precision, restoration and the complete supplier/caller invoice.
+None of those conclusions follows from the character theorem alone.
+
+Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0.
+The written proof and finite checks are not independent human review or a
+formal proof-kernel verification.
diff --git a/research/nonsplit-frobenius-characters/README.md b/research/nonsplit-frobenius-characters/README.md
new file mode 100644
index 0000000000..cd60d2ac20
--- /dev/null
+++ b/research/nonsplit-frobenius-characters/README.md
@@ -0,0 +1,166 @@
+# Nonsplit Frobenius-product determinant characters
+
+This package extends the supplied-decomposition tensor interface to products
+whose residue fields are nontrivial finite extensions of the ground field.
+It proves the exact automorphism and covariant stabilizer determinant images,
+constructs witnesses, and checks supplied three-factor maps and their
+special-linear orbit labels. It does not recover a decomposition from an
+arbitrary tensor or supply a paid multiplication algorithm. No new kappa is
+claimed.
+
+## Result
+
+Fix K=F_q of characteristic p. For each component choose an explicit extension
+L_j=F_(q^d_j) and let
+
+```
+A = product_j L_j[x_i]/(x_i^(p^h_ji)),
+N_j = p^(sum_i h_ji),
+E_ji = N_j (p^h_ji - 1)/2.
+```
+
+An empty height list means the residue field itself. The intrinsic type of a
+component is `(d_j, sorted heights)`. Set g to the gcd of q-1 and all E_ji,
+also including (q-1)/2 if q is odd and either an even residue degree occurs
+or an identical odd-degree type repeats. Then
+
+```
+det Aut_K(A) = (K*)^g,
+Delta(mu_A) = {(u,v,w): (uvw)^((q-1)/g) = 1}.
+```
+
+The GL orbit splits into exactly g orbits under SL x SL x SL. For checked maps
+`t(Ua,Vb)=W mu_A(a,b)` relative to the same ordered model, the complete label is
+
+```
+(det(W)/(det(U)det(V)))^((q-1)/g).
+```
+
+[PROOF.md](PROOF.md) proves the coefficient-field section, norm characters,
+Frobenius signs, matching of factors, unit determinant surjectivity and the
+covariant convention. The decisive dimension in E_ji is N_j over L_j, not
+d_j N_j over K. Coefficient Frobenius contributes a separate sign, and only
+identical full types may be exchanged.
+
+For a discriminating example, take K=F9=F3[t]/(t^2+1), beta=1+t, and
+L=K[u]/(u^2-beta). On L[x]/x^3 the substitution x -> u x has determinant
+Norm(u)^3=beta^7 of order eight. Multiplying E by the residue degree would
+incorrectly restrict this determinant to squares. Separately, on F9[x]/x^9
+viewed over F3, coefficient Frobenius supplies determinant -1 even though
+all residue-linear automorphisms have determinant one.
+
+## Supplied presentation and executable contract
+
+`model.py` uses exact finite-field arithmetic and standard-library Python.
+The unchanged, authenticated `vendor/local.py` from PR5637 supplies the ground
+field and matrix operations. `Field(p, modulus)` presents K with canonical
+base-p digits. `Extension(base, modulus)` presents a residue field with
+constant-first monic coefficients in K and canonical base-q digit encoding;
+it rejects reducible moduli by checking every nonzero element is invertible.
+This supports extension ground fields as well as prime fields.
+
+`make_model(base, components, residues)` requires a nonempty, lexicographically
+sorted list of `(degree, sorted positive heights)` and one explicit residue
+presentation per used degree. The degree-one field can be omitted and is K.
+The basis is ordered first by component, then lexicographic truncated monomial,
+then polynomial coefficient-field power. This order is part of the certificate.
+Unsorted types are rejected. If an external decomposition has a different
+order, its supplied factor maps must include that actual permutation; its
+sign must not be discarded.
+
+`model_isomorphism` matches identical supplied presentations. It rejects a
+different residue polynomial even when the abstract fields are isomorphic.
+Comparing those presentations requires a separately supplied and checked field
+isomorphism, with its determinant included. The code does not discover field
+embeddings or infer them from equal dimensions.
+
+The public witness operations are `variable_scaling`, `coefficient_frobenius`,
+`component_swap` and `unit_multiplication`. `automorphism(model, determinant)`
+constructs an admissible determinant or rejects it; `autotopism` and
+`covariant_stabilizer` construct requested determinant triples. Every constructed
+autotopism checks all basis products. The covariant action is `(U^-T,V^-T,W)`.
+`validate_certificate(model, table, U, V, W)` checks shape, canonical entries,
+invertibility and every basis product before returning the label.
+
+Theorems cover all finite fields and all finite supplied types. The executable
+materializes field tables and dense algebra tensors and enumerates field
+scalars, primitive elements and discrete logarithms. No polynomial complexity
+in log(q), binary-encoded heights, or growing residue degrees is claimed.
+No general tensor recognizer or special-linear transporter between arbitrary
+input tensors is supplied here.
+
+## Verification
+
+From the repository root with CPython 3.12:
+
+```sh
+python3 -B scripts/research_package.py --package research/nonsplit-frobenius-characters
+python3 -B scripts/check_research_commit.py --package research/nonsplit-frobenius-characters --check-source-history
+```
+
+The registered commands use warning-strict isolated normal and optimized modes.
+The checker authenticates all five live source inputs before importing the
+model. Its direct matrix and orbit checks are separate from the constructive
+witness routines. Exact counts and execution boundaries are recorded in
+[VALIDATION.md](VALIDATION.md); the finite checks corroborate the written theorem
+without replacing it.
+
+## Sources, scope and coordination
+
+Canonical base is `df0137efd35e11b4445734bf612bdd4c7ebc330c`, priority revision 7,
+selected conditional kappa `62009/20000000`. The prescribed source-binding
+baseline passed after materializing tracked files omitted by the sparse
+checkout. It is a metadata check, not a scientific replay.
+
+The [canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/5655#discussioncomment-19187845)
+and [TASK.json](TASK.json) record the handoff-first choice and family-expansion
+decision. The split-product recognizer was already claimed and is now
+[PR5661](https://github.com/CrocSwap/integer-mult-bounds/pull/5661), at
+`5d722279f4292c63361f1e958ff4ed5a6ec638aa`; it explicitly excludes nonsplit
+residue fields. This contribution answers the separate nonsplit-character
+question in it and PR5656. The formal-interface-lemma card is retained verbatim
+but scope is explicitly changed to a written algebraic theorem rather than a
+proof-assistant development.
+
+Compared alternative: PR5658 already supplies field-level routing prefix and
+suffix bounds. Its remaining physical-cost question requires an actual caller;
+this algebraic handoff has a bounded exact acceptance test. Fresh all-state PR
+searches, live handoffs and the product investigation were checked. Sparse
+historical notes, arbitrary old diffs and unpublished work remain coverage limits.
+
+[SOURCES.json](SOURCES.json) pins the live proofs and reused executable.
+[vendor/ORIGINS.json](vendor/ORIGINS.json) binds retained copies to their original
+public commits and paths. Vendor bytes and frozen predecessor packages are
+unchanged. The local determinant theorem and classical finite-field facts are
+credited dependencies, not newly claimed results.
+
+## Open next questions
+
+- Recognize nonsplit products from arbitrary tensors. Recover compatible
+  coefficient-field sections and local maps; the split recognizer cannot simply
+  drop its residue-field test. This would remove the supplied-model premise.
+- Compare different residue-field presentations. Supply a checked field
+  isomorphism and account for its ground-field determinant in each factor map.
+  The present executable intentionally requires common presentations.
+- Use this interface in a named native producer and consumer. Charge field
+  representation, coefficients, movement, precision and restoration before
+  deriving any multiplication-bound consequence. No such caller is supplied.
+
+Structured questions and their blockers are in [TASK.json](TASK.json).
+
+## Credit
+
+New nonsplit proof, construction and finite checker: apoursh, with substantial
+OpenAI Codex assistance from a coordinator and separate implementation, proof
+and verification agents. No independent human or proof-kernel review is claimed.
+Nick Petalas's PR5252 (`07e6f55d18d2d3fd6dcea19bd642d71657c5fe14`) supplies the
+etale norm/Frobenius/permutation interface. Ali Romman's PR5459
+(`bef3575ddb19c44434a7e2460a353eac7c4d9387`) supplies local nilpotent characters;
+PR5637 (`86389e525d3efafe236e929f6ae401c68be1d115`) supplies reused field/matrix
+code. apoursh's PR5656 (`b5e6e7c45f606d639d102570f9fab257e1d0d393`) supplies the
+split-product argument and handoff; PR5502 supplies the height-type lineage.
+David Ganz and the retained tensor-atlas authors retain their notices. Norms,
+normal bases, finite-field structure and regular-module arguments are classical.
+New work is Apache-2.0, with all retained notices preserved; no global literature
+priority claim is made. No selected cold replay, Lean or Docker run is required
+or claimed for this isolated algebraic contribution.
diff --git a/research/nonsplit-frobenius-characters/RESULT.json b/research/nonsplit-frobenius-characters/RESULT.json
new file mode 100644
index 0000000000..60f73042ea
--- /dev/null
+++ b/research/nonsplit-frobenius-characters/RESULT.json
@@ -0,0 +1,324 @@
+{
+  "authenticated_source_files": 5,
+  "certificate_controls": {
+    "changed_or_malformed_certificates_rejected": 14,
+    "different_coset_labels_distinguished": true,
+    "dimension": 9,
+    "independent_three_factor_bases_checked": true
+  },
+  "covariant_controls": {
+    "accepted_covariant_triples": 128,
+    "base_field_size": 9,
+    "dimension": 9,
+    "nonlinear_missing_transpose_rejected": true,
+    "rejected_covariant_triples": 384
+  },
+  "nilpotent_substitution_exhaustions": [
+    {
+      "complete_automorphism_substitutions": 6,
+      "determinant_image": [
+        1
+      ],
+      "dimension": 4,
+      "height": 1,
+      "p": 2,
+      "residue_degree": 2
+    },
+    {
+      "complete_automorphism_substitutions": 144,
+      "determinant_image": [
+        1,
+        2
+      ],
+      "dimension": 6,
+      "height": 1,
+      "p": 3,
+      "residue_degree": 2
+    }
+  ],
+  "presentation_controls": {
+    "presentation_or_type_rejections": 8,
+    "same_dimension_different_types_checked": true
+  },
+  "scope": "Finite exact matrices support the separate theorem; large automorphism groups and tensor recognition are not exhausted.",
+  "status": "PASS_NONSPLIT_FROBENIUS_CHARACTERS",
+  "strong_norm_and_frobenius_controls": {
+    "F27_pair_over_F3_component_swap_determinant": 2,
+    "F81_linear_scaling_image": [
+      1,
+      2,
+      3,
+      4,
+      5,
+      6,
+      7,
+      8
+    ],
+    "F9_x9_over_F3_coefficient_frobenius_determinant": 2,
+    "F9_x9_over_F3_scaling_determinants": [
+      1
+    ],
+    "base_field_size": 9,
+    "beta": 4,
+    "checked_F81_substitutions": 88,
+    "determinant_order": 8,
+    "independent_extension_products": 6561,
+    "independent_norm_checks": 80,
+    "residue_field_size": 81,
+    "scaling_x_to_u_x_determinant": 5,
+    "scope": "80 linear and 8 nonlinear F81 substitutions checked, not all12960 automorphisms.",
+    "wrong_extra_degree_image": [
+      1,
+      2,
+      3,
+      6
+    ]
+  },
+  "tiny_full_GL_exhaustions": [
+    {
+      "all_matrices": 16,
+      "automorphisms": 2,
+      "components": [
+        [
+          2,
+          []
+        ]
+      ],
+      "determinant_image": [
+        1
+      ],
+      "determinant_triples": [
+        [
+          1,
+          1,
+          1
+        ]
+      ],
+      "dimension": 2,
+      "invertible_matrices": 6,
+      "normalized_autotopisms": 18,
+      "p": 2,
+      "units": 3
+    },
+    {
+      "all_matrices": 81,
+      "automorphisms": 2,
+      "components": [
+        [
+          2,
+          []
+        ]
+      ],
+      "determinant_image": [
+        1,
+        2
+      ],
+      "determinant_triples": [
+        [
+          1,
+          1,
+          1
+        ],
+        [
+          1,
+          1,
+          2
+        ],
+        [
+          1,
+          2,
+          1
+        ],
+        [
+          1,
+          2,
+          2
+        ],
+        [
+          2,
+          1,
+          1
+        ],
+        [
+          2,
+          1,
+          2
+        ],
+        [
+          2,
+          2,
+          1
+        ],
+        [
+          2,
+          2,
+          2
+        ]
+      ],
+      "dimension": 2,
+      "invertible_matrices": 48,
+      "normalized_autotopisms": 128,
+      "p": 3,
+      "units": 8
+    },
+    {
+      "all_matrices": 512,
+      "automorphisms": 3,
+      "components": [
+        [
+          3,
+          []
+        ]
+      ],
+      "determinant_image": [
+        1
+      ],
+      "determinant_triples": [
+        [
+          1,
+          1,
+          1
+        ]
+      ],
+      "dimension": 3,
+      "invertible_matrices": 168,
+      "normalized_autotopisms": 147,
+      "p": 2,
+      "units": 7
+    },
+    {
+      "all_matrices": 19683,
+      "automorphisms": 3,
+      "components": [
+        [
+          3,
+          []
+        ]
+      ],
+      "determinant_image": [
+        1
+      ],
+      "determinant_triples": [
+        [
+          1,
+          1,
+          1
+        ],
+        [
+          1,
+          2,
+          2
+        ],
+        [
+          2,
+          1,
+          2
+        ],
+        [
+          2,
+          2,
+          1
+        ]
+      ],
+      "dimension": 3,
+      "invertible_matrices": 11232,
+      "normalized_autotopisms": 2028,
+      "p": 3,
+      "units": 26
+    },
+    {
+      "all_matrices": 512,
+      "automorphisms": 2,
+      "components": [
+        [
+          1,
+          []
+        ],
+        [
+          2,
+          []
+        ]
+      ],
+      "determinant_image": [
+        1
+      ],
+      "determinant_triples": [
+        [
+          1,
+          1,
+          1
+        ]
+      ],
+      "dimension": 3,
+      "invertible_matrices": 168,
+      "normalized_autotopisms": 18,
+      "p": 2,
+      "units": 3
+    },
+    {
+      "all_matrices": 19683,
+      "automorphisms": 2,
+      "components": [
+        [
+          1,
+          []
+        ],
+        [
+          2,
+          []
+        ]
+      ],
+      "determinant_image": [
+        1,
+        2
+      ],
+      "determinant_triples": [
+        [
+          1,
+          1,
+          1
+        ],
+        [
+          1,
+          1,
+          2
+        ],
+        [
+          1,
+          2,
+          1
+        ],
+        [
+          1,
+          2,
+          2
+        ],
+        [
+          2,
+          1,
+          1
+        ],
+        [
+          2,
+          1,
+          2
+        ],
+        [
+          2,
+          2,
+          1
+        ],
+        [
+          2,
+          2,
+          2
+        ]
+      ],
+      "dimension": 3,
+      "invertible_matrices": 11232,
+      "normalized_autotopisms": 512,
+      "p": 3,
+      "units": 16
+    }
+  ]
+}
diff --git a/research/nonsplit-frobenius-characters/SOURCES.json b/research/nonsplit-frobenius-characters/SOURCES.json
new file mode 100644
index 0000000000..89beb6774e
--- /dev/null
+++ b/research/nonsplit-frobenius-characters/SOURCES.json
@@ -0,0 +1,51 @@
+{
+  "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/etale-tensor-determinant-image/README.md",
+      "usage": "input",
+      "git_blob": "0f07df6ce2a8c43ea1fcc5f0081ee3532da28208",
+      "sha256": "2ec18042a1a63d5fd5da246f4f6060c5fb66cff338f25a2a1b95e3ea8b4f0fba"
+    },
+    {
+      "path": "research/frobenius-tensor-characters/README.md",
+      "usage": "input",
+      "git_blob": "b62f9a906e6ed49605684cca52a221f064924461",
+      "sha256": "31573ba91ac69caff5b8e5a42ce7fd0d80a6d54673c08d7f225c9ee08e0e0893"
+    },
+    {
+      "path": "research/nonsplit-frobenius-characters/vendor/local.py",
+      "usage": "input",
+      "git_blob": "1066bb74c19d180bfef7d9dd1c0650ec6bbd7780",
+      "sha256": "6daa160346d04691c6ca3c9c820b3df8982de4320ec01e5db10e3cb932f42c00",
+      "pin": "head:808d31b2016ee666ef637e2cc5d1118f5fdd29c0:research/nonsplit-frobenius-characters/vendor/local.py"
+    },
+    {
+      "path": "research/nonsplit-frobenius-characters/vendor/split-proof.md",
+      "usage": "input",
+      "git_blob": "a9f931a378ebf7a67881d209f46c2f7fe47d1041",
+      "sha256": "0eb6c9f9eba70dc339e54b72a98b5b0fdcef706bcff5e02546ab2d0426a85ad9",
+      "pin": "head:808d31b2016ee666ef637e2cc5d1118f5fdd29c0:research/nonsplit-frobenius-characters/vendor/split-proof.md"
+    },
+    {
+      "path": "research/nonsplit-frobenius-characters/vendor/ORIGINS.json",
+      "usage": "input",
+      "git_blob": "7c1142e2fc6866f0d19b71cc3ea7d46db8f75949",
+      "sha256": "a8b552fbea489bd9bf5a72e6f5212a0741ccded6acfd5901e055811c3126518f",
+      "pin": "head:808d31b2016ee666ef637e2cc5d1118f5fdd29c0:research/nonsplit-frobenius-characters/vendor/ORIGINS.json"
+    }
+  ]
+}
diff --git a/research/nonsplit-frobenius-characters/TASK.json b/research/nonsplit-frobenius-characters/TASK.json
new file mode 100644
index 0000000000..b206430a21
--- /dev/null
+++ b/research/nonsplit-frobenius-characters/TASK.json
@@ -0,0 +1,111 @@
+{
+  "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": "Supplied-decomposition nonsplit Frobenius products: norm characters, coefficient-Frobenius and component permutation signs, determinant witnesses and supplied-map orbit labels.",
+  "scope_change_reason": "Handoff-first selection of the nontrivial-residue-field question in PR5656/5661. The exact split-product recognizer was already claimed and completed by aliromman. This is a written algebraic interface theorem with finite checks, not proof-assistant formalization.",
+  "bottleneck_link": "Algebraic side result extending the tensor atlas beyond split residue fields. No paid native supplier or kappa improvement is claimed.",
+  "budget_minutes": 60,
+  "stop_rule": "Finish the nonsplit character proof, exact independent ground-field matrix checks, meaningful failure controls and reproducible package; do not expand into arbitrary nonsplit recognition or physical pricing.",
+  "outcome": "completed",
+  "evidence": "PROOF.md supplies the general finite-field theorem. Independent exact checker covers 40487 matrices (22854 invertible), 14 automorphisms and 2851 normalized autotopisms in six complete tiny GL domains; 150 complete nilpotent substitutions; 6561 F81 products, 80 norm determinants and 88 F81 substitutions; 512 covariant determinant triples (128 accepted,384 rejected); 14 certificate and eight presentation/type rejection controls. No arbitrary tensor recognition or independent human review.",
+  "author": "apoursh",
+  "ai_assistance": "Substantial OpenAI Codex assistance, including separate implementation, proof and independent finite-check agents; no independent human or proof-kernel review.",
+  "open_questions": [
+    {
+      "question": "Recognize nonsplit Frobenius products from arbitrary tensors.",
+      "why_it_matters": "Removes the supplied decomposition and coefficient-field premise.",
+      "first_step": "Recover the radical, residue fields and their coefficient-field sections, then construct compatible local maps and authenticate their field embeddings.",
+      "blocked_by": "This package only checks supplied models/maps; PR5661 recognizes split residue fields."
+    },
+    {
+      "question": "Transport certificates between different presentations of the same residue field.",
+      "why_it_matters": "Intrinsic types alone do not identify ordered coordinate bases.",
+      "first_step": "Supply and verify a field isomorphism and include its restriction-of-scalars determinant in each model map.",
+      "blocked_by": "The executable fixes one explicit residue presentation per degree."
+    },
+    {
+      "question": "Use the interface in a paid native producer and consumer.",
+      "why_it_matters": "An algebraic determinant result alone does not improve the multiplication bound.",
+      "first_step": "Name the actual maps and price coefficients, movement, precision and restoration.",
+      "blocked_by": "No physical caller or complete invoice is supplied."
+    }
+  ],
+  "coordination": "https://github.com/CrocSwap/integer-mult-bounds/discussions/5655#discussioncomment-19187845",
+  "overlap_coverage": "Fresh canonical main and selected guidance; live handoffs1166 and investigation5655; bounded all-state PR searches. Exact split recognition was claimed in19187666 and published as5661 at5d722279f4292c63361f1e958ff4ed5a6ec638aa. Sparse historical notes, arbitrary old diffs and unpublished work remain outside coverage.",
+  "expansion_decision": "Compare PR5658 sector routing: field-level prefix/suffix bounds already exist; missing physical pricing needs a named caller. The nonsplit-character handoff instead provides a bounded interface implication with explicit norm/sign controls.",
+  "baseline": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY after materializing omitted tracked source files; no selected scientific replay."
+}
diff --git a/research/nonsplit-frobenius-characters/VALIDATION.md b/research/nonsplit-frobenius-characters/VALIDATION.md
new file mode 100644
index 0000000000..0ffc9034c1
--- /dev/null
+++ b/research/nonsplit-frobenius-characters/VALIDATION.md
@@ -0,0 +1,77 @@
+# Validation and execution boundaries
+
+Environment: CPython 3.12.14, macOS arm64, standard library only. The coordinator
+ran the registered package after the separate verifier agent's development
+checks. Both registered warning-strict, isolated normal and optimized commands
+passed and printed identical complete JSON reports. [RESULT.json](RESULT.json)
+is that deterministic report with its success marker retained.
+
+```sh
+python3 -B scripts/research_package.py --package research/nonsplit-frobenius-characters
+```
+
+The registered manifest contains these direct commands:
+
+```sh
+python3 -I -W error -B research/nonsplit-frobenius-characters/verify.py
+python3 -I -W error -O -B research/nonsplit-frobenius-characters/verify.py
+```
+
+`--json` prints the full report as one JSON object. Explicit exceptions retain
+the checks under optimization. Five live source inputs are authenticated before
+model import. The reused field/matrix module is separately hash-checked and
+compiled from those exact bytes, avoiding stale bytecode for that dependency.
+
+## Finite coverage
+
+Six tiny complete matrix domains cover F4/F2, F9/F3, F8/F2, F27/F3,
+F2 x F4 over F2, and F3 x F9 over F3. The checker examines 40,487 matrices,
+22,854 invertible matrices and all 14 algebra automorphisms in those domains.
+All 2,851 normalized autotopisms obtained from their full unit groups are
+checked by products; the autotopism normalization theorem supplies completeness
+of that parametrization, rather than an enumeration of every pair of matrices.
+
+Two complete nilpotent substitution domains cover all six automorphisms of
+F4[x]/x^2 over F2 and all 144 automorphisms of F9[x]/x^3 over F3, using coefficient
+Frobenius and every allowed polynomial substitution. Their multiplication
+matrices and determinants are checked independently.
+
+Over the extension ground field F9, independent polynomial-remainder arithmetic
+checks all 6,561 F81 products and all 80 nonzero norm determinants. The nilpotent
+fixture checks 80 linear and eight nonlinear substitutions on F81[x]/x^3;
+it does not enumerate that full 12,960-element automorphism group. The explicit
+x -> u x witness has determinant beta^7 of order eight. A deliberately incorrect
+extra residue-degree exponent produces only four squares. Further controls
+check coefficient Frobenius on F9[x]/x^9 over F3 and an odd-degree F27 component
+swap, both by literal ground-field matrices.
+
+All 512 nonzero determinant triples over F9 are tested on a proper-subgroup
+fixture: 128 are accepted with literal covariant coefficient checks and 384
+are rejected. A nonlinear automorphism catches omission of the inverse-input
+transposes. Independent changes in all three tensor factors are checked;
+different determinant cosets produce different labels. Fourteen changed or
+malformed certificates and eight presentation/type mismatches are rejected,
+including equal-dimensional but different algebras and a separately valid
+alternate field presentation.
+
+## Review and limitations
+
+Separate Codex agents implemented the model, wrote the proof and implemented
+the independent checker. The coordinator reviewed the proof and implementation,
+and an implementation agent independently reviewed the final proof/API agreement.
+These are automated checks, not independent human review or proof-kernel acceptance.
+The independent verifier shares only the retained ground-field primitive; its
+extension arithmetic, elimination, multiplication-table and coefficient checks
+are separate from the constructor. The classical/local character proofs are
+retained dependencies.
+
+The source-binding baseline passed after materializing tracked files omitted
+from the sparse checkout. No selected scientific replay, previous full package
+suite, Lean, Docker, native supplier, physical pricing, arbitrary nonsplit tensor
+recognition or complete multiplication theorem was run or established. Different
+field presentations require an explicit checked field isomorphism outside this
+API. No polynomial-in-log(q) performance claim is made.
+
+Committed-byte, source-history, official export and Git-free publication evidence
+is reported with the exact published commit in the PR. Hosted CI is separate
+from the local scientific checks and does not establish the general theorem.
diff --git a/research/nonsplit-frobenius-characters/VERIFY.json b/research/nonsplit-frobenius-characters/VERIFY.json
new file mode 100644
index 0000000000..a83399b0cf
--- /dev/null
+++ b/research/nonsplit-frobenius-characters/VERIFY.json
@@ -0,0 +1,40 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [
+    "research/etale-tensor-determinant-image/README.md",
+    "research/frobenius-tensor-characters/README.md",
+    "research/nonsplit-frobenius-characters/vendor/local.py",
+    "research/nonsplit-frobenius-characters/vendor/split-proof.md",
+    "research/nonsplit-frobenius-characters/vendor/ORIGINS.json"
+  ],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "Independent exact nonsplit-product matrix, norm, Frobenius, character, supplied-certificate and rejection controls."
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-O",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 180,
+      "checks": "The same explicit checks with optimization enabled."
+    }
+  ]
+}
diff --git a/research/nonsplit-frobenius-characters/model.py b/research/nonsplit-frobenius-characters/model.py
new file mode 100644
index 0000000000..c83c5f7745
--- /dev/null
+++ b/research/nonsplit-frobenius-characters/model.py
@@ -0,0 +1,416 @@
+#!/usr/bin/env python3
+"""Explicit nonsplit Frobenius-product determinant witnesses.
+
+Input fields and residue polynomials are supplied, not recognized. The base is
+the retained Field implementation. Extension elements use base-q digits, and
+model basis index is offset + monomial_index * residue_degree + coefficient
+exponent. Matrices use row-major storage and columns are basis images.
+Certificates use tensor(Ua,Vb) = W * model(a,b). All input coordinates must be
+canonical field integers. Components must already be in canonical type order.
+
+Finite field-table construction, primitive-element search and discrete-log
+enumeration are bounded-fixture algorithms, not polynomial bit-complexity
+claims. No arbitrary tensor recognition or cross-presentation field matching
+is implemented. Prepared by apoursh with substantial OpenAI Codex assistance.
+New work is Apache-2.0; the unchanged vendor retains its own notice.
+"""
+
+import hashlib
+from itertools import product
+from math import gcd
+from pathlib import Path
+from types import ModuleType
+
+
+VENDOR_SHA256 = "6daa160346d04691c6ca3c9c820b3df8982de4320ec01e5db10e3cb932f42c00"
+_vendor_path = Path(__file__).with_name("vendor") / "local.py"
+_vendor_bytes = _vendor_path.read_bytes()
+if hashlib.sha256(_vendor_bytes).hexdigest() != VENDOR_SHA256:
+    raise ValueError("retained finite-field source hash mismatch")
+local = ModuleType("nonsplit_retained_local")
+exec(compile(_vendor_bytes, str(_vendor_path), "exec"), local.__dict__)
+Field = local.Field
+
+
+def _integer(value):
+    return type(value) is int
+
+
+def _base_signature(base):
+    if not isinstance(base, Field):
+        raise ValueError("base must be the retained explicit Field")
+    return base.p, base.modulus
+
+
+def _element(value, field, name="element", nonzero=False):
+    if not _integer(value) or not (int(nonzero) <= value < field.q):
+        raise ValueError(name + " must be a canonical field integer" + (" and nonzero" if nonzero else ""))
+
+
+class Extension:
+    """Finite residue field over an explicit base Field, with constant-first modulus."""
+
+    def __init__(self, base, modulus):
+        _base_signature(base)
+        if (not isinstance(modulus, (list, tuple)) or len(modulus) < 2
+                or any(not _integer(c) or not 0 <= c < base.q for c in modulus)
+                or modulus[-1] != 1):
+            raise ValueError("residue modulus must be monic with canonical base-field coefficients")
+        self.base, self.modulus = base, tuple(modulus)
+        self.degree, self.p = len(modulus) - 1, base.p
+        self.q = base.q ** self.degree
+        self.digits = [[(a // base.q ** i) % base.q for i in range(self.degree)] for a in range(self.q)]
+        self.add = [[sum(base.add[x][y] * base.q ** i for i, (x, y) in enumerate(zip(a, b)))
+                     for b in self.digits] for a in self.digits]
+        self.neg = [sum(base.neg[x] * base.q ** i for i, x in enumerate(a)) for a in self.digits]
+        self.mul = []
+        for a in self.digits:
+            row = []
+            for b in self.digits:
+                coefficients = [0] * (2 * self.degree - 1)
+                for i, x in enumerate(a):
+                    for j, y in enumerate(b):
+                        coefficients[i + j] = base.add[coefficients[i + j]][base.mul[x][y]]
+                for k in range(len(coefficients) - 1, self.degree - 1, -1):
+                    for j in range(self.degree):
+                        correction = base.neg[base.mul[coefficients[k]][modulus[j]]]
+                        coefficients[k - self.degree + j] = base.add[coefficients[k - self.degree + j]][correction]
+                row.append(sum(coefficients[i] * base.q ** i for i in range(self.degree)))
+            self.mul.append(row)
+        self.inv = [0] + [self.power(a, self.q - 2) for a in range(1, self.q)]
+        if any(self.mul[a][self.inv[a]] != 1 for a in range(1, self.q)):
+            raise ValueError("residue modulus is reducible over the supplied base field")
+
+    def power(self, a, exponent):
+        _element(a, self)
+        if not _integer(exponent) or exponent < 0:
+            raise ValueError("power exponent must be a nonnegative integer")
+        result = 1
+        while exponent:
+            if exponent & 1:
+                result = self.mul[result][a]
+            a = self.mul[a][a]
+            exponent //= 2
+        return result
+
+    def norm(self, a):
+        value = self.power(a, (self.q - 1) // (self.base.q - 1))
+        if any(self.digits[value][1:]):
+            raise RuntimeError("norm did not land in the supplied base field")
+        return self.digits[value][0]
+
+    def frobenius(self, a):
+        return self.power(a, self.base.q)
+
+
+def _components(components):
+    if not isinstance(components, (list, tuple)) or not components:
+        raise ValueError("a product must have at least one component")
+    result = []
+    for component in components:
+        if not isinstance(component, (list, tuple)) or len(component) != 2:
+            raise ValueError("a component must be (residue degree, heights)")
+        degree, heights = component
+        if not _integer(degree) or degree < 1:
+            raise ValueError("residue degree must be a positive integer")
+        if not isinstance(heights, (list, tuple)) or any(not _integer(h) or h < 1 for h in heights):
+            raise ValueError("heights must be positive integers")
+        if list(heights) != sorted(heights):
+            raise ValueError("heights must be sorted")
+        result.append((degree, tuple(heights)))
+    if result != sorted(result):
+        raise ValueError("components must be in canonical degree-and-height order")
+    return result
+
+
+def make_model(base, components, residues=None):
+    """Construct the ground-field table, using one residue presentation per degree."""
+    signature = _base_signature(base)
+    types = _components(components)
+    degrees = {degree for degree, _ in types}
+    if residues is None:
+        residues = {}
+    if not isinstance(residues, dict):
+        raise ValueError("residues must map degrees to explicit Extension objects")
+    supplied = dict(residues)
+    if 1 in degrees and 1 not in supplied:
+        supplied[1] = Extension(base, [0, 1])
+    if any(not _integer(d) or d not in degrees for d in supplied):
+        raise ValueError("residue dictionary has an invalid or unused degree")
+    if set(supplied) != degrees:
+        raise ValueError("one explicit residue field is required for each degree")
+    for degree, residue in supplied.items():
+        if not isinstance(residue, Extension) or residue.degree != degree:
+            raise ValueError("residue field degree does not match its key")
+        if _base_signature(residue.base) != signature:
+            raise ValueError("residue field uses a different base presentation")
+    local_dimensions = [base.p ** sum(heights) for _, heights in types]
+    dimensions = [degree * size for (degree, _), size in zip(types, local_dimensions)]
+    offsets, offset = [], 0
+    exponents = []
+    for (_, heights), size in zip(types, dimensions):
+        offsets.append(offset)
+        offset += size
+        exponents.append([list(a) for a in product(*(range(base.p ** h) for h in heights))])
+    n = sum(dimensions)
+    table = [[[0] * n for _ in range(n)] for _ in range(n)]
+    unit = [0] * n
+    for (degree, heights), start, monomials in zip(types, offsets, exponents):
+        residue = supplied[degree]
+        monomial_index = {tuple(a): i for i, a in enumerate(monomials)}
+        bounds = [base.p ** h for h in heights]
+        unit[start] = 1
+        for i, a in enumerate(monomials):
+            for j, b in enumerate(monomials):
+                combined = tuple(x + y for x, y in zip(a, b))
+                if any(x >= bound for x, bound in zip(combined, bounds)):
+                    continue
+                target = start + degree * monomial_index[combined]
+                for r in range(degree):
+                    for s in range(degree):
+                        coefficients = residue.digits[residue.mul[base.q ** r][base.q ** s]]
+                        for k, value in enumerate(coefficients):
+                            table[start + degree * i + r][start + degree * j + s][target + k] = value
+    return {"base": base, "components": [[d, list(h)] for d, h in types],
+            "residues": supplied, "local_dimensions": local_dimensions,
+            "dimensions": dimensions, "offsets": offsets, "exponents": exponents,
+            "n": n, "table": table, "unit": unit}
+
+
+def model_isomorphism(first, second):
+    """Match identical supplied presentations; alternative field isomorphisms are not provided."""
+    if _base_signature(first["base"]) != _base_signature(second["base"]):
+        raise ValueError("base-field presentations differ")
+    if first["components"] != second["components"]:
+        raise ValueError("component degree-and-height types differ")
+    if any(first["residues"][d].modulus != second["residues"][d].modulus for d in first["residues"]):
+        raise ValueError("residue presentations differ; supply a separate checked field isomorphism")
+    return local.identity(first["n"])
+
+
+def determinant_character(base, components):
+    _base_signature(base)
+    types = _components(components)
+    exponents = [[base.p ** sum(heights) * (base.p ** h - 1) // 2 for h in heights]
+                 for _, heights in types]
+    g = base.q - 1
+    for row in exponents:
+        for exponent in row:
+            g = gcd(g, exponent)
+    signs = []
+    if base.q % 2:
+        signs.extend({"kind": "frobenius", "component": i} for i, (d, _) in enumerate(types) if d % 2 == 0)
+        seen = {}
+        for i, kind in enumerate(types):
+            if kind in seen and kind[0] % 2:
+                signs.append({"kind": "swap", "components": [seen[kind], i]})
+            seen.setdefault(kind, i)
+        if signs:
+            g = gcd(g, (base.q - 1) // 2)
+    return {"index": g, "label_exponent": (base.q - 1) // g,
+            "local_exponents": exponents, "sign_generators": signs}
+
+
+def _component(model, component):
+    if not _integer(component) or not 0 <= component < len(model["components"]):
+        raise ValueError("invalid component index")
+    degree, heights = model["components"][component]
+    return degree, heights, model["residues"][degree]
+
+
+def _coefficient_matrix(model, component, images):
+    degree, _, residue = _component(model, component)
+    matrix = local.identity(model["n"])
+    start = model["offsets"][component]
+    for monomial in range(model["local_dimensions"][component]):
+        block = start + degree * monomial
+        for column in range(degree):
+            image = images(monomial, residue.base.q ** column)
+            for row, value in enumerate(residue.digits[image]):
+                matrix[block + row][block + column] = value
+    return matrix
+
+
+def variable_scaling(model, component, variable, scalar):
+    _, heights, residue = _component(model, component)
+    if not _integer(variable) or not 0 <= variable < len(heights):
+        raise ValueError("invalid variable index")
+    _element(scalar, residue, "scaling coefficient", True)
+    return _coefficient_matrix(model, component, lambda m, a: residue.mul[a][
+        residue.power(scalar, model["exponents"][component][m][variable])])
+
+
+def coefficient_frobenius(model, component):
+    _, _, residue = _component(model, component)
+    return _coefficient_matrix(model, component, lambda m, a: residue.frobenius(a))
+
+
+def component_swap(model, first, second):
+    _component(model, first)
+    _component(model, second)
+    if first == second or model["components"][first] != model["components"][second]:
+        raise ValueError("swap requires two distinct components of identical type")
+    matrix = local.identity(model["n"])
+    for k in range(model["dimensions"][first]):
+        a, b = model["offsets"][first] + k, model["offsets"][second] + k
+        matrix[a], matrix[b] = matrix[b], matrix[a]
+    return matrix
+
+
+def unit_multiplication(model, component, scalar):
+    _, _, residue = _component(model, component)
+    _element(scalar, residue, "unit coefficient", True)
+    return _coefficient_matrix(model, component, lambda m, a: residue.mul[scalar][a])
+
+
+def _primitive_element(field):
+    for candidate in range(1, field.q):
+        value, seen = 1, set()
+        while value not in seen:
+            seen.add(value)
+            value = field.mul[value][candidate]
+        if len(seen) == field.q - 1:
+            return candidate
+    raise RuntimeError("no primitive element in checked field")
+
+
+def _norm_preimage(residue, desired):
+    _element(desired, residue.base, "desired norm", True)
+    for candidate in range(1, residue.q):
+        if residue.norm(candidate) == desired:
+            return candidate
+    raise RuntimeError("checked finite-field norm was not surjective")
+
+
+def _exponent_word(base, exponents, desired):
+    root = _primitive_element(base)
+    value, logarithm = 1, 0
+    while value != desired:
+        value = base.mul[value][root]
+        logarithm += 1
+        if logarithm >= base.q - 1:
+            raise ValueError("desired determinant is not a nonzero base-field element")
+    divisor, coefficients = base.q - 1, []
+    for exponent in exponents:
+        divisor, left, right = local.bezout(divisor, exponent)
+        coefficients = [left * c for c in coefficients] + [right]
+    if logarithm % divisor:
+        raise ValueError("desired determinant lies outside the automorphism image")
+    return root, [c * (logarithm // divisor) for c in coefficients]
+
+
+def _check_products(model, target, U, V, W):
+    f, n = model["base"], model["n"]
+    for i in range(n):
+        for j in range(n):
+            if local.tensor_value(target, local.column(U, i), local.column(V, j), f) != local.mv(W, model["table"][i][j], f):
+                raise ValueError("three-factor certificate fails a basis-product identity")
+
+
+def automorphism(model, desired_det):
+    base = model["base"]
+    _element(desired_det, base, "desired determinant", True)
+    character = determinant_character(base, model["components"])
+    instructions, exponents = [], []
+    for component, row in enumerate(character["local_exponents"]):
+        for variable, exponent in enumerate(row):
+            instructions.append({"kind": "scale", "component": component, "variable": variable})
+            exponents.append(exponent)
+    for sign in character["sign_generators"]:
+        instructions.append(sign)
+        exponents.append((base.q - 1) // 2)
+    root, coefficients = _exponent_word(base, exponents, desired_det)
+    matrix, operations = local.identity(model["n"]), []
+    for instruction, coefficient in zip(instructions, coefficients):
+        kind = instruction["kind"]
+        if kind == "scale":
+            component = instruction["component"]
+            residue = model["residues"][model["components"][component][0]]
+            scalar = _norm_preimage(residue, base.power(root, coefficient % (base.q - 1)))
+            operation = variable_scaling(model, component, instruction["variable"], scalar)
+            operations.append({**instruction, "scalar": scalar})
+        elif coefficient % 2:
+            operation = coefficient_frobenius(model, instruction["component"]) if kind == "frobenius" else component_swap(model, *instruction["components"])
+            operations.append(dict(instruction))
+        else:
+            continue
+        matrix = local.mm(operation, matrix, base)
+    if local.determinant(matrix, base) != desired_det:
+        raise RuntimeError("automorphism determinant mismatch")
+    if local.mv(matrix, model["unit"], base) != model["unit"]:
+        raise RuntimeError("automorphism does not preserve the unit")
+    _check_products(model, model["table"], matrix, matrix, matrix)
+    return {"matrix": matrix, "determinant": desired_det, "operations": operations, "index": character["index"]}
+
+
+def _unit_with_determinant(model, desired):
+    base = model["base"]
+    degree = model["components"][0][0]
+    exponent = 0 if base.q == 2 else pow(model["local_dimensions"][0], -1, base.q - 1)
+    scalar = _norm_preimage(model["residues"][degree], base.power(desired, exponent))
+    matrix = unit_multiplication(model, 0, scalar)
+    if local.determinant(matrix, base) != desired:
+        raise RuntimeError("unit determinant mismatch")
+    return matrix, scalar
+
+
+def autotopism(model, a, b, c):
+    base = model["base"]
+    for value in (a, b, c):
+        _element(value, base, "requested determinant", True)
+    delta = base.mul[base.mul[a][b]][base.inv[c]]
+    phi = automorphism(model, delta)
+    left, left_scalar = _unit_with_determinant(model, base.mul[a][base.inv[delta]])
+    right, right_scalar = _unit_with_determinant(model, base.mul[b][base.inv[delta]])
+    U, V = local.mm(left, phi["matrix"], base), local.mm(right, phi["matrix"], base)
+    W = local.mm(local.mm(left, right, base), phi["matrix"], base)
+    determinants = [local.determinant(matrix, base) for matrix in (U, V, W)]
+    if determinants != [a, b, c]:
+        raise RuntimeError("autotopism determinant mismatch")
+    _check_products(model, model["table"], U, V, W)
+    return {"U": U, "V": V, "W": W, "determinants": determinants,
+            "left_unit_scalar": left_scalar, "right_unit_scalar": right_scalar, "automorphism": phi}
+
+
+def covariant_stabilizer(model, a, b, c):
+    base = model["base"]
+    for value in (a, b, c):
+        _element(value, base, "requested determinant", True)
+    witness = autotopism(model, base.inv[a], base.inv[b], c)
+    A = list(map(list, zip(*local.inverse(witness["U"], base))))
+    B = list(map(list, zip(*local.inverse(witness["V"], base))))
+    C = witness["W"]
+    if [local.determinant(matrix, base) for matrix in (A, B, C)] != [a, b, c]:
+        raise RuntimeError("covariant determinant mismatch")
+    return {"A": A, "B": B, "C": C, "determinants": [a, b, c], "autotopism": witness}
+
+
+def _matrix(matrix, n, base, name):
+    if not isinstance(matrix, (list, tuple)) or len(matrix) != n:
+        raise ValueError(name + " must be an n by n matrix")
+    result = []
+    for row in matrix:
+        if not isinstance(row, (list, tuple)) or len(row) != n:
+            raise ValueError(name + " must be an n by n matrix")
+        for value in row:
+            _element(value, base, name + " entry")
+        result.append(list(row))
+    return result
+
+
+def validate_certificate(model, table, U, V, W):
+    """Validate a supplied three-factor decomposition and compute its canonical orbit label."""
+    base, n = model["base"], model["n"]
+    if not isinstance(table, (list, tuple)) or len(table) != n:
+        raise ValueError("tensor must have shape n by n by n")
+    table = [_matrix(plane, n, base, "tensor plane") for plane in table]
+    U, V, W = [_matrix(matrix, n, base, name) for matrix, name in ((U, "U"), (V, "V"), (W, "W"))]
+    determinants = [local.determinant(matrix, base) for matrix in (U, V, W)]
+    if not all(determinants):
+        raise ValueError("certificate factor maps must be invertible")
+    _check_products(model, table, U, V, W)
+    d = base.mul[determinants[2]][base.inv[base.mul[determinants[0]][determinants[1]]]]
+    character = determinant_character(base, model["components"])
+    return {"n": n, "components": model["components"], "determinants": determinants,
+            "d": d, "label": base.power(d, character["label_exponent"]),
+            "index": character["index"], "basis_products_checked": n * n}
diff --git a/research/nonsplit-frobenius-characters/vendor/ORIGINS.json b/research/nonsplit-frobenius-characters/vendor/ORIGINS.json
new file mode 100644
index 0000000000..7c1142e2fc
--- /dev/null
+++ b/research/nonsplit-frobenius-characters/vendor/ORIGINS.json
@@ -0,0 +1,21 @@
+{
+  "scope": "Unmodified sources reused for field/matrix arithmetic and the split-product character proof; source-specific notices retained.",
+  "files": [
+    {
+      "path": "vendor/local.py",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "86389e525d3efafe236e929f6ae401c68be1d115",
+      "source_path": "research/extension-field-tensor-recognition/recognize.py",
+      "git_blob": "1066bb74c19d180bfef7d9dd1c0650ec6bbd7780",
+      "sha256": "6daa160346d04691c6ca3c9c820b3df8982de4320ec01e5db10e3cb932f42c00"
+    },
+    {
+      "path": "vendor/split-proof.md",
+      "repository": "CrocSwap/integer-mult-bounds",
+      "commit": "b5e6e7c45f606d639d102570f9fab257e1d0d393",
+      "source_path": "research/frobenius-product-characters/PROOF.md",
+      "git_blob": "a9f931a378ebf7a67881d209f46c2f7fe47d1041",
+      "sha256": "0eb6c9f9eba70dc339e54b72a98b5b0fdcef706bcff5e02546ab2d0426a85ad9"
+    }
+  ]
+}
diff --git a/research/nonsplit-frobenius-characters/vendor/local.py b/research/nonsplit-frobenius-characters/vendor/local.py
new file mode 100644
index 0000000000..1066bb74c1
--- /dev/null
+++ b/research/nonsplit-frobenius-characters/vendor/local.py
@@ -0,0 +1,370 @@
+"""Exact finite-field tensor recognition. Ali Romman with OpenAI Codex. Apache-2.0."""
+from itertools import product
+from math import gcd, isqrt
+
+
+class Field:
+    """Use base-p digits and a monic polynomial, in constant-first order."""
+
+    def __init__(self, p, modulus):
+        if type(p) is not int or p < 2 or any(p % d == 0 for d in range(2, isqrt(p) + 1)):
+            raise ValueError('p must be prime')
+        if (not isinstance(modulus, (tuple, list)) or len(modulus) < 2
+                or modulus[-1] != 1
+                or any(type(c) is not int or not 0 <= c < p for c in modulus)):
+            raise ValueError('modulus must be monic with canonical prime-field coefficients')
+        self.p, self.e = p, len(modulus) - 1
+        self.modulus = tuple(modulus)
+        self.q = p ** self.e
+        digits = [[(a // p ** i) % p for i in range(self.e)] for a in range(self.q)]
+        self.add = [[sum(((x + y) % p) * p ** i for i, (x, y) in enumerate(zip(a, b)))
+                     for b in digits] for a in digits]
+        self.neg = [sum((-x % p) * p ** i for i, x in enumerate(a)) for a in digits]
+        self.mul = []
+        for a in digits:
+            row = []
+            for b in digits:
+                c = [0] * (2 * self.e - 1)
+                for i, x in enumerate(a):
+                    for j, y in enumerate(b):
+                        c[i + j] = (c[i + j] + x * y) % p
+                for k in range(len(c) - 1, self.e - 1, -1):
+                    for j in range(self.e):
+                        c[k - self.e + j] = (c[k - self.e + j] - c[k] * modulus[j]) % p
+                row.append(sum(c[i] * p ** i for i in range(self.e)))
+            self.mul.append(row)
+        self.inv = [0] + [self.power(a, self.q - 2) for a in range(1, self.q)]
+        if any(self.mul[a][self.inv[a]] != 1 for a in range(1, self.q)):
+            raise ValueError('modulus is reducible')
+
+    def power(self, a, n):
+        if n < 0:
+            raise ValueError('negative exponent')
+        r = 1
+        while n:
+            if n & 1:
+                r = self.mul[r][a]
+            a = self.mul[a][a]
+            n //= 2
+        return r
+
+    def total(self, xs):
+        r = 0
+        for x in xs:
+            r = self.add[r][x]
+        return r
+
+
+def identity(n):
+    return [[int(i == j) for j in range(n)] for i in range(n)]
+
+
+def columns(xs, n):
+    return [[v[i] for v in xs] for i in range(n)]
+
+
+def column(a, j):
+    return [r[j] for r in a]
+
+
+def rref(a, width, f):
+    rows = [r[:] for r in a]
+    pivots = []
+    k = 0
+    for j in range(width):
+        pivot = next((i for i in range(k, len(rows)) if rows[i][j]), None)
+        if pivot is None:
+            continue
+        rows[k], rows[pivot] = rows[pivot], rows[k]
+        rows[k] = [f.mul[f.inv[rows[k][j]]][x] for x in rows[k]]
+        for i in range(len(rows)):
+            if i != k and rows[i][j]:
+                c = f.neg[rows[i][j]]
+                rows[i] = [f.add[x][f.mul[c][y]] for x, y in zip(rows[i], rows[k])]
+        pivots.append(j)
+        k += 1
+        if k == len(rows):
+            break
+    return rows, pivots
+
+
+def rank(a, f):
+    return len(rref(a, len(a[0]) if a else 0, f)[1])
+
+
+def kernel(a, width, f):
+    rows, pivots = rref(a, width, f)
+    out = []
+    for j in range(width):
+        if j in pivots:
+            continue
+        v = [0] * width
+        v[j] = 1
+        for i, p in enumerate(pivots):
+            v[p] = f.neg[rows[i][j]]
+        out.append(v)
+    return out
+
+
+def inverse(a, f):
+    n = len(a)
+    rows, pivots = rref([r + e for r, e in zip(a, identity(n))], n, f)
+    if len(pivots) != n:
+        raise ValueError('singular matrix')
+    return [r[n:] for r in rows]
+
+
+def mv(a, v, f):
+    return [f.total(f.mul[x][y] for x, y in zip(r, v)) for r in a]
+
+
+def mm(a, b, f):
+    return columns([mv(a, column(b, j), f) for j in range(len(b[0]))], len(a))
+
+
+def determinant(a, f):
+    rows = [r[:] for r in a]
+    d = 1
+    for j in range(len(rows)):
+        k = next((i for i in range(j, len(rows)) if rows[i][j]), None)
+        if k is None:
+            return 0
+        if k != j:
+            rows[k], rows[j] = rows[j], rows[k]
+            d = f.neg[d]
+        c = rows[j][j]
+        d = f.mul[d][c]
+        for i in range(j + 1, len(rows)):
+            z = f.neg[f.mul[rows[i][j]][f.inv[c]]]
+            rows[i] = [f.add[x][f.mul[z][y]] for x, y in zip(rows[i], rows[j])]
+    return d
+
+
+def tensor_value(t, u, v, f):
+    n = len(t)
+    out = [0] * n
+    for i, x in enumerate(u):
+        if x:
+            for j, y in enumerate(v):
+                if y:
+                    c = f.mul[x][y]
+                    out = [f.add[z][f.mul[c][a]] for z, a in zip(out, t[i][j])]
+    return out
+
+
+def algebra_power(t, u, exponent, unit, f):
+    r = unit[:]
+    while exponent:
+        if exponent & 1:
+            r = tensor_value(t, r, u, f)
+        u = tensor_value(t, u, u, f)
+        exponent //= 2
+    return r
+
+
+def model(heights, f):
+    bounds = [f.p ** h for h in heights]
+    exponents = list(product(*(range(b) for b in bounds)))
+    ix = {v: i for i, v in enumerate(exponents)}
+    n = len(exponents)
+    t = [[[0] * n for _ in range(n)] for _ in range(n)]
+    for i, a in enumerate(exponents):
+        for j, b in enumerate(exponents):
+            c = tuple(x + y for x, y in zip(a, b))
+            if all(x < bound for x, bound in zip(c, bounds)):
+                t[i][j][ix[c]] = 1
+    return t, exponents
+
+
+def semilinear_kernel(t, unit, h, f):
+    """Return ker(a -> a^(p^h)), with the coefficient twist removed."""
+    n = len(t)
+    c = columns([algebra_power(t, v, f.p ** h, unit, f) for v in identity(n)], n)
+    untwist = f.p ** ((-h) % f.e)
+    return [[f.power(x, untwist) for x in v] for v in kernel(c, n, f)]
+
+
+def validate_tensor(t, f):
+    if not isinstance(f, Field):
+        raise ValueError('field contract required')
+    if not isinstance(t, (list, tuple)) or not t:
+        raise ValueError('positive square tensor required')
+    n = len(t)
+    if any(not isinstance(a, (list, tuple)) or len(a) != n for a in t):
+        raise ValueError('input dimensions differ')
+    for a in t:
+        for b in a:
+            if not isinstance(b, (list, tuple)) or len(b) != n:
+                raise ValueError('output dimension differs')
+            if any(type(x) is not int or not 0 <= x < f.q for x in b):
+                raise ValueError('noncanonical field entry')
+
+
+def check_certificate(t, cert, f):
+    """Check the factor maps by all basis products, without nucleus tests."""
+    n = len(t)
+    mu, _ = model(cert['heights'], f)
+    if len(mu) != n:
+        return False
+    u, v, w = (cert[k] for k in ('U', 'V', 'W'))
+    if any(determinant(a, f) == 0 for a in (u, v, w)):
+        return False
+    for i in range(n):
+        for j in range(n):
+            if tensor_value(t, column(u, i), column(v, j), f) != mv(w, mu[i][j], f):
+                return False
+    return True
+
+
+def recognize(t, f):
+    """Return (certificate, None), or (None, mathematical rejection reason)."""
+    validate_tensor(t, f)
+    n = len(t)
+    equations = []
+    for i, j, k in product(range(n), repeat=3):
+        row = [0] * (2 * n * n)
+        for a in range(n):
+            row[a * n + i] = f.add[row[a * n + i]][t[a][j][k]]
+            index = n * n + k * n + a
+            row[index] = f.add[row[index]][f.neg[t[i][j][a]]]
+        equations.append(row)
+    basis = kernel(equations, 2 * n * n, f)
+    if len(basis) != n:
+        return None, 'nucleus dimension'
+    xb = [[b[i * n:(i + 1) * n] for i in range(n)] for b in basis]
+    yb = [[b[n * n + i * n:n * n + (i + 1) * n] for i in range(n)] for b in basis]
+    if rank([b[:n*n] for b in basis], f) != n or rank([b[n*n:] for b in basis], f) != n:
+        return None, 'nucleus projection'
+    if any(mm(a, b, f) != mm(b, a, f) for a in yb for b in yb):
+        return None, 'noncommutative nucleus'
+    right = [[t[i][j][k] for j in range(n)] for i in range(n) for k in range(n)]
+    if rank(right, f) != n:
+        return None, 'right kernel'
+    flat = [sum(a, []) for a in yb]
+    _, positions = rref(flat, n * n, f)
+    coord_inverse = inverse([[a[j] for a in flat] for j in positions], f)
+
+    def coordinates(a):
+        v = sum(a, [])
+        c = mv(coord_inverse, [v[j] for j in positions], f)
+        if [f.total(f.mul[c[k]][flat[k][j]] for k in range(n)) for j in range(n*n)] != v:
+            raise ArithmeticError('nucleus closure')
+        return c
+
+    table = [[coordinates(mm(a, b, f)) for b in yb] for a in yb]
+    unit = coordinates(identity(n))
+    exponent = 1
+    while exponent < n:
+        exponent *= f.q
+    qmap = columns([algebra_power(table, v, exponent, unit, f) for v in identity(n)], n)
+    radical = kernel(qmap, n, f)
+    if len(radical) != n - 1:
+        return None, 'residue field or number of components'
+
+    def cyclic(module):
+        actions = [[[f.total(f.mul[c[k]][module[k][i][j]] for k in range(n))
+                     for j in range(n)] for i in range(n)] for c in radical]
+        jm = [column(a, j) for a in actions for j in range(n)]
+        if rank(jm, f) != n - 1:
+            return None
+        seed = next(v for v in identity(n) if rank(jm + [v], f) == n)
+        return columns([mv(a, seed, f) for a in module], n), seed
+
+    ux, wy = cyclic(xb), cyclic(yb)
+    if ux is None or wy is None:
+        return None, 'nonregular nucleus module'
+    u, u0 = ux
+    w, _ = wy
+    phi = columns([tensor_value(t, u0, e, f) for e in identity(n)], n)
+    v = mm(inverse(phi, f), w, f)
+    span = [tensor_value(table, a, b, f) for a in radical for b in radical]
+    current = rank(span, f)
+    generators, heights = [], []
+    h, power = 0, 1
+    while power < n:
+        h += 1
+        power *= f.p
+        for a in semilinear_kernel(table, unit, h, f):
+            new_rank = rank(span + [a], f)
+            if new_rank > current:
+                span.append(a)
+                generators.append(a)
+                heights.append(h)
+                current = new_rank
+    if f.p ** sum(heights) != n:
+        return None, 'height dimension'
+    mu, exponents = model(heights, f)
+    images = []
+    for exps in exponents:
+        value = unit[:]
+        for g, e in zip(generators, exps):
+            value = tensor_value(table, value, algebra_power(table, g, e, unit, f), f)
+        images.append(value)
+    c = columns(images, n)
+    if determinant(c, f) == 0:
+        raise ArithmeticError('height criterion did not produce a basis')
+    cert = {'heights': heights, 'U': mm(u, c, f), 'V': mm(v, c, f), 'W': mm(w, c, f)}
+    if not check_certificate(t, cert, f):
+        raise ArithmeticError('transported product mismatch')
+    index = gcd(f.q - 1, *(n * (f.p ** h - 1) // 2 for h in heights))
+    detu, detv, detw = (determinant(cert[k], f) for k in ('U', 'V', 'W'))
+    delta = f.mul[detw][f.inv[f.mul[detu][detv]]]
+    cert['sl_orbit_count'] = index
+    cert['sl_orbit_label'] = f.power(delta, (f.q - 1) // index)
+    return cert, None
+
+
+def bezout(a, b):
+    x, y, u, v = 1, 0, 0, 1
+    while b:
+        quotient, remainder = divmod(a, b)
+        a, b = b, remainder
+        x, u = u, x - quotient * u
+        y, v = v, y - quotient * v
+    return a, x, y
+
+
+def sl_transporter(first, second, f):
+    """Return determinant-one maps F,G,H with second(Fu,Gv)=H first(u,v)."""
+    a, why = recognize(first, f)
+    if a is None:
+        return None, 'first tensor: ' + why
+    b, why = recognize(second, f)
+    if b is None:
+        return None, 'second tensor: ' + why
+    if a['heights'] != b['heights'] or a['sl_orbit_label'] != b['sl_orbit_label']:
+        return None, 'different special-linear orbits'
+    n, m = len(first), f.q - 1
+    du, dv, dw = [f.mul[determinant(a[k], f)][f.inv[determinant(b[k], f)]]
+                  for k in ('U', 'V', 'W')]
+    z = f.mul[f.mul[du][dv]][f.inv[dw]]
+    primitive = next(c for c in range(1, f.q)
+                     if len({f.power(c, i) for i in range(m)}) == m)
+    logz = next(i for i in range(m) if f.power(primitive, i) == z)
+    g, coefficients = m, []
+    for h in a['heights']:
+        g, x, y = bezout(g, n * (f.p ** h - 1) // 2)
+        coefficients = [x * c for c in coefficients] + [y]
+    if logz % g:
+        raise ArithmeticError('orbit label disagrees with determinant image')
+    scalars = [f.power(primitive, (c * (logz // g)) % m) for c in coefficients]
+    _, exponents = model(a['heights'], f)
+    diagonal = [1] * n
+    for j, es in enumerate(exponents):
+        for c, e in zip(scalars, es):
+            diagonal[j] = f.mul[diagonal[j]][f.power(c, e)]
+    inverse_n = pow(n, -1, m)
+    unit_a = f.power(f.mul[du][f.inv[z]], inverse_n)
+    unit_b = f.power(f.mul[dv][f.inv[z]], inverse_n)
+    factors = [unit_a, unit_b, f.mul[unit_a][unit_b]]
+    out = {}
+    for key, target, scalar in zip(('U', 'V', 'W'), ('F', 'G', 'H'), factors):
+        middle = [[f.mul[scalar][diagonal[i]] if i == j else 0 for j in range(n)] for i in range(n)]
+        out[target] = mm(mm(b[key], middle, f), inverse(a[key], f), f)
+        if determinant(out[target], f) != 1:
+            raise ArithmeticError('determinant correction failed')
+    for i in range(n):
+        for j in range(n):
+            if tensor_value(second, column(out['F'], i), column(out['G'], j), f) != mv(out['H'], first[i][j], f):
+                raise ArithmeticError('special-linear product mismatch')
+    return out, None
diff --git a/research/nonsplit-frobenius-characters/vendor/split-proof.md b/research/nonsplit-frobenius-characters/vendor/split-proof.md
new file mode 100644
index 0000000000..a9f931a378
--- /dev/null
+++ b/research/nonsplit-frobenius-characters/vendor/split-proof.md
@@ -0,0 +1,350 @@
+# Determinant characters for split products of Frobenius-truncated algebras
+
+This note answers the split-product part of the open question in
+[Ali Romman's PR5637](https://github.com/CrocSwap/integer-mult-bounds/pull/5637).
+The local factor models and a decomposition certificate are supplied. We
+derive their product's automorphism determinant image, full covariant tensor
+stabilizer image, special-linear orbit label and constructive transporters.
+We do not recognize an arbitrary tensor or recover a decomposition from it.
+The result is an algebraic interface statement and does not improve kappa.
+
+## 1. Models and the main formula
+
+Fix one explicit finite field K = F_q of characteristic p. All algebra
+automorphisms and tensor factor maps below are K-linear; coefficient-field
+automorphisms are not allowed. Let s >= 1
+and define
+
+    B_j = K[x_(j,1),...,x_(j,r_j)] / (x_(j,i)^(p^h_(j,i))),
+    A = product_(j=1)^s B_j,
+    N_j = dim_K B_j = p^(sum_i h_(j,i)),
+    n = dim_K A = sum_j N_j.
+
+Each height is a positive integer. An empty height list means B_j = K
+and N_j = 1. A factor's **type** is its sorted height list. Within a factor,
+use the monomial basis with lexicographically ordered exponent tuples. The
+canonical product model orders factor types lexicographically; equal types
+are consecutive copies of the same model.
+
+Set L = q-1, and for every variable define the integer
+
+    E_(j,i) = N_j * (p^h_(j,i) - 1) / 2.
+
+It is integral: for odd p the second factor is even; for p = 2 every factor
+containing a variable has even dimension. Include a swap generator precisely
+when q is odd and some type occurs at least twice with odd component
+dimension. Its exponent is T = L/2. Set
+
+    g = gcd(L, all E_(j,i), T if that swap generator exists),
+    H_g = {c^g : c in K*}.
+
+The gcd of the singleton list (L) is L. This includes field factors with
+empty height lists and q = 2, where L = g = 1. Every N_j in this family is
+odd when q is odd; the dimension condition identifies the sign's source.
+
+**Theorem.** The image of Aut_K(A) under determinant is exactly H_g. For
+multiplication mu_A and the covariant action on A* tensor A* tensor A, the
+full stabilizer determinant image is
+
+    Delta(mu_A) = {(u,v,w) in (K*)^3 : uvw in H_g}
+                = {(u,v,w) : (uvw)^(L/g) = 1}.
+
+It has L^3/g elements. The general-linear orbit of mu_A contains exactly g
+orbits under SL_n(K)^3. Every allowed determinant triple is attained by an
+explicit autotopism. For tensors supplied with verified factor maps, the
+canonical type multiset and Section 6's label completely decide
+special-linear equivalence.
+
+## 2. Local type and local determinant character
+
+We restate the local argument of PR5459 to identify the input to the product
+calculation. In B = K[x_1,...,x_r]/(x_i^(p^h_i)), let J = (x_1,...,x_r).
+An element with nonzero constant term is a unit by a finite geometric
+series; all elements of J are nilpotent. Thus B is local with residue field
+K. Its only idempotents are zero and one: one of e and 1-e is a unit, and
+e(1-e) = 0 determines an idempotent e.
+
+The tangent quotient J/J^2 has the variables as a basis. Its intrinsic
+height flag is
+
+    V_e = (ker(a -> a^(p^e)) + J^2)/J^2.
+
+These kernels are K-subspaces even though the power map is semilinear over
+an extension field. Frobenius removes mixed terms. A nonzero linear term
+in x_i survives the p^e power exactly when h_i > e, and no term of degree
+at least two can cancel its degree-p^e monomial. Therefore V_e is exactly
+the span of variables of height at most e. Its dimension increments recover
+the height multiset. Two displayed local factors are isomorphic if and only
+if their types agree; equal dimension alone is insufficient.
+
+An automorphism's tangent map preserves this flag. Conversely, an invertible
+flag-preserving linear substitution respects the defining power relations:
+a variable of height h is sent only to variables whose heights are at most
+h. Its inverse preserves the same flag, so this substitution is an
+automorphism. A general automorphism and its linear substitution induce the
+same map on the associated graded algebra for powers of J. A monomial basis
+ordered by total degree shows that they have equal determinants.
+
+The flag-preserving group is generated by allowed elementary substitutions
+and diagonal scalings. For an allowed substitution x_i -> x_i + c*x_k,
+the monomial expansion is triangular when ordered by x_i exponent, with
+diagonal one. Its determinant is one. Scaling x_i -> c*x_i has determinant
+c^E_i: the sum of the x_i exponents over the N monomials is
+
+    E_i = N * (p^h_i - 1) / 2.
+
+Elementary and diagonal matrices generate the full general-linear group
+within each equal-height block, while the other allowed elementary matrices
+generate the off-diagonal flag-preserving part. Thus the local determinant
+image is generated exactly by the subgroups {c^E_i : c in K*}. With an empty
+height list, the K-algebra K has only the identity automorphism.
+
+## 3. Primitive idempotents and the permutation contribution
+
+An idempotent of A has each coordinate zero or one. The nonzero primitive
+idempotents are precisely the e_j supported on a single factor: any
+idempotent supported on more than one factor splits into nonzero orthogonal
+idempotents. Algebra automorphisms preserve this intrinsic property.
+
+An automorphism sending e_j to e_k restricts to an isomorphism e_j A -> e_k A,
+so those factors have the same type. Conversely, any permutation among
+copies of one type, together with an independent automorphism on each factor,
+defines an automorphism of A. These are all the possibilities; there are
+no additional maps mixing primitive factors.
+
+Factorwise automorphisms contribute the product of their local determinants.
+Swapping two identical factors of dimension N swaps N pairs of matching
+basis vectors, so its determinant is (-1)^N. This remains true for blocks
+separated by other blocks: those same N basis-vector transpositions describe
+the operation. Equivalently, conjugate by a fixed reordering that places the
+copies together. For any allowed permutation the sign contribution is
+
+    product_over_types type_permutation_sign^(dimension_of_that_type).
+
+Hence signs contribute only for repeated isomorphic odd-dimensional factors
+in odd characteristic. In characteristic two every sign is one. Unequal
+types cannot be swapped, even when they have the same dimension.
+
+The finite group K* is cyclic of order L. Relative to a generator zeta, the
+determinant generators have exponents E_(j,i) and, when present, T = L/2.
+They generate precisely <zeta^g> = H_g. Each generator is attained by a
+literal variable scaling or permitted block transposition. This proves
+the automorphism image and its attainment.
+
+## 4. Unit determinants and the full tensor stabilizer
+
+For a unit a = (a_j), multiplication by a_j is triangular on its monomials
+ordered by total degree. Its constant term c_j is on every diagonal entry.
+Consequently
+
+    det(L_a) = product_j c_j^N_j.
+
+This map is onto K*: choose one component and let all other components
+equal one. The chosen N_j is a power of p and is coprime to L, so its scalar
+constant can attain any desired determinant. For q = 2 the unit one suffices.
+This uses one component dimension N_j, not the total dimension n, which
+need not be coprime to L.
+
+We use the classical unital commutative autotopism normalization retained in
+PR5252 and PR5459. Suppose invertible F,G,H satisfy
+
+    F(x) * G(y) = H(x*y).
+
+Put a = F(1), b = G(1). Evaluation at one gives H(x) = F(x)*b = a*G(x).
+Invertibility of F,G,H implies that multiplication by a and b is invertible,
+so a and b are units. Then sigma = L_(ab)^(-1) H is a unital algebra
+automorphism and
+
+    F = L_a sigma,   G = L_b sigma,   H = L_(ab) sigma.
+
+Conversely these maps always form an autotopism. Write x = det L_a,
+y = det L_b, z = det sigma. The corresponding covariant stabilizer element
+is (F^(-T),G^(-T),H), with determinant triple
+
+    (u,v,w) = (x^(-1) z^(-1), y^(-1) z^(-1), x*y*z).
+
+Its product is z^(-1), in H_g. Conversely, for a requested triple with
+uvw in H_g, set
+
+    z = (u*v*w)^(-1),   x = v*w,   y = u*w.
+
+The automorphism and unit determinant constructions attain these three
+values and hence the requested triple. This proves the full image formula.
+There are L^2 choices for the first two entries and L/g possible products,
+so its cardinality is L^3/g.
+
+## 5. Constructive determinant witnesses
+
+Fix a generator zeta of K*. For a desired z in H_g, write z = zeta^k
+with 0 <= k < L; membership is equivalent to g dividing k. Bezout
+coefficients give
+
+    g = b_0 L + sum_(j,i) b_(j,i) E_(j,i) + b_T T,
+
+omitting the final term when no swap generator exists. Scale variable (j,i)
+by zeta^(b_(j,i)*k/g), and compose one fixed permitted transposition to
+power b_T*k/g if needed. The resulting determinant is z. Negative
+coefficients are allowed because the maps are invertible. If all character
+generators are trivial, only z = 1 is requested and the identity suffices.
+
+For desired unit determinant x, choose a component j and an inverse r of
+N_j modulo L. The unit with scalar x^r in that component and one elsewhere
+has determinant x. In the trivial multiplicative group use the identity.
+Together with Section 4 this constructs every allowed determinant triple.
+
+Primitive-element and discrete-log enumeration in an explicit finite field
+suffice for a fixed q. This is not a polynomial bit-complexity claim in log q.
+A different exact subgroup witness search can be used, provided it verifies
+the same determinants and transported basis products.
+
+## 6. Supplied certificates and special-linear labels
+
+A tensor t: K^n x K^n -> K^n is supplied with model factor types and three
+invertible matrices U,V,W, in the convention
+
+    t(U*a,V*b) = W*mu_A(a,b).
+
+Columns are basis images from the declared model to the tensor. Check the
+dimensions, invertibility and all n^2 model basis products. By bilinearity
+these finite identities verify the supplied decomposition for all inputs.
+They do not provide a procedure for discovering the certificate.
+
+The reference model must be fixed before comparing labels. Heights inside
+each factor are sorted, and factor types are sorted lexicographically.
+For another supplied component order, construct the monomial permutation
+R from the canonical model to the supplied model, matching full types and
+monomial coordinates. Normalize the factor maps to
+
+    U_c = U*R,   V_c = V*R,   W_c = W*R.
+
+Thus, with d_raw = det(W)/(det(U)*det(V)),
+
+    d = det(W_c)/(det(U_c)*det(V_c)) = d_raw/det(R),
+    label(t) = d^(L/g).
+
+Sorting type metadata alone can lose this permutation sign. If variable
+order is also changed inside a supplied factor, its monomial permutation
+must also be included, or the interface must require sorted heights from
+the start. R changes the reference model coordinates, not the ambient
+coordinates of t.
+
+Two choices of matching among identical factors differ by a model
+automorphism, whose determinant lies in H_g, so the label is unchanged.
+More generally, two valid certificates from the same canonical model differ
+by a tensor stabilizer. Their determinant products differ by an element of
+H_g. The label is therefore independent of the certificate.
+
+For completeness, let G = GL_n(K)^3 and S = SL_n(K)^3. The determinant map
+G -> (K*)^3 has kernel S. Since S is normal, its orbits within a fixed
+G-orbit correspond to cosets of the stabilizer determinant image. The product
+map identifies these cosets with K*/H_g. The map d -> d^(L/g) has kernel
+H_g, so its value is a complete label, with exactly g possible values.
+
+Different type multisets cannot be general-linearly equivalent. An isotopy
+between multiplication in two unital commutative algebras normalizes exactly
+as in Section 4, using units in the target algebra, to an algebra isomorphism.
+It must match primitive idempotents and then local types. Conversely a type
+matching gives a literal product algebra isomorphism. For verified
+certificates over the same explicit field, therefore,
+
+    SL-equivalent iff canonical type multisets agree and labels agree.
+
+Different presentations of the finite field need an explicit, checked field
+isomorphism before their element-valued labels can be compared.
+
+## 7. Determinant-one transporters
+
+Let two normalized certificates (U_1,V_1,W_1) and (U_2,V_2,W_2) have the
+same canonical model and label. Put
+
+    a = det(U_1)/det(U_2),
+    b = det(V_1)/det(V_2),
+    c = det(W_1)/det(W_2).
+
+We need a model autotopism (P,Q,R_0) with determinants (a,b,c). In
+Section 4's notation choose
+
+    z = a*b/c,   x = a/z,   y = b/z.
+
+Equal labels imply (c/(a*b))^(L/g) = 1, hence z belongs to H_g.
+Section 5 constructs the required automorphism and units. Then
+
+    F = U_2 * P   * U_1^(-1),
+    G = V_2 * Q   * V_1^(-1),
+    H = W_2 * R_0 * W_1^(-1)
+
+all have determinant one and satisfy
+
+    t_2(F*x,G*y) = H*t_1(x,y).
+
+Substitution in the certificate identities proves this. An executable can
+also verify the three determinants and every transported basis product.
+Unequal labels preclude such maps.
+
+## 8. Discriminating examples and boundary cases
+
+Over F_3, let B = F_3[x]/(x^9). Its height list is (2), dimension nine,
+and local exponent 9*(9-1)/2 = 36. Since L = 2, the local automorphism
+determinant image is {1}; its multiplication orbit splits into two
+special-linear orbits. For B x B, a block transposition has determinant
+(-1)^9 = -1. The product gcd is gcd(2,36,36,1) = 1, giving only one
+special-linear orbit. A product rule using only local characters misses
+this change.
+
+The factors F_3[x]/(x^9) and F_3[y,z]/(y^3,z^3) both have dimension nine,
+but their height lists (2) and (1,1) have different tangent dimensions.
+A proposed swap is not an algebra automorphism. Equal component size
+does not authorize a permutation generator or component match.
+
+If all heights are empty, A = K^s. For s = 1 the automorphism image is
+trivial and g = L. For s >= 2 and odd q, permutations add -1 and g = L/2;
+in characteristic two they add nothing and g = L. This agrees with the
+split finite-etale case of PR5252. For q = 2 every nonzero determinant and
+label is one, and g = 1 for every model.
+
+Unequal component dimensions add no automorphism generators, but their block
+ordering still affects normalization of a supplied certificate. The empty
+product and zero-dimensional zero algebra are excluded. An empty height
+list inside a nonempty product is a valid field factor.
+
+## 9. Cost, credit and remaining obligations
+
+The gcd formula only needs exponents modulo L. Compute
+p^(sum_i h_(j,i)) * (p^h_(j,i)-1) modulo 2L and halve its even residue
+to obtain E_(j,i) modulo L without materializing a large component dimension.
+Modular powers, type comparison and gcd are polynomial in the parameter bit
+lengths, given p,q and the finite-field contract. Building and checking
+explicit matrices is instead polynomial in the explicit algebra dimension
+at fixed q. These are different size statements: a short symbolic height
+list can specify an algebra too large to materialize. The executable builds
+literal model dimensions and local exponents; the modular method just
+described is an arithmetic consequence of the formula, not an implemented
+compressed-model runtime guarantee.
+
+Ali Romman's [PR5459 at bef3575ddb19c44434a7e2460a353eac7c4d9387](https://github.com/aliromman/integer-mult-bounds/blob/bef3575ddb19c44434a7e2460a353eac7c4d9387/research/frobenius-tensor-characters/README.md)
+supplies the local height flag and determinant character; those local
+results are predecessor work. His
+[PR5637 at 86389e525d3efafe236e929f6ae401c68be1d115](https://github.com/aliromman/integer-mult-bounds/blob/86389e525d3efafe236e929f6ae401c68be1d115/research/extension-field-tensor-recognition/README.md)
+supplies extension-field recognition, local special-linear labels and the
+explicit product handoff. [apoursh's PR5502](https://github.com/CrocSwap/integer-mult-bounds/pull/5502)
+supplies the prime-field table height criterion.
+[Nick Petalas's PR5252](https://github.com/CrocSwap/integer-mult-bounds/pull/5252)
+supplies finite-etale tensor determinants and the normalization lineage.
+David Ganz and the retained atlas framework retain their credit. Primitive
+idempotents, cyclic subgroup arithmetic and unital isotopy normalization are
+classical; no general literature-priority claim is made.
+
+Open next questions are recovery of this decomposition from an arbitrary
+tensor and local factors with residue fields larger than the base. The
+latter requires coefficient-field identifications, norms and additional
+automorphisms; it does not follow by dropping the residue-field hypothesis.
+Neither task is supplied here. Physical coefficient preparation, native
+implementation, precision, movement, restoration, supplier admission and
+a new multiplication exponent remain outside this result.
+
+The written theorem covers general finite fields. Executable coverage is
+limited to the field contract and domains stated in the package's README;
+finite checks are corroboration, not a proof-kernel verification.
+
+Prepared by apoursh with substantial OpenAI Codex assistance. Apache-2.0.
+No independent human or formal proof-kernel acceptance is claimed.
diff --git a/research/nonsplit-frobenius-characters/verify.py b/research/nonsplit-frobenius-characters/verify.py
new file mode 100644
index 0000000000..3ad05e1513
--- /dev/null
+++ b/research/nonsplit-frobenius-characters/verify.py
@@ -0,0 +1,528 @@
+#!/usr/bin/env python3
+"""Bounded independent ground-field checks of nonsplit determinant characters.
+
+Apache-2.0. Prepared by apoursh with substantial OpenAI Codex assistance.
+Only the retained Field primitive is shared; extension arithmetic, elimination,
+model products and tensor coefficient checks below are independent oracles.
+"""
+import argparse
+import copy
+import hashlib
+import importlib.util
+import itertools
+import json
+from pathlib import Path
+
+
+def require(condition, message):
+    if not condition:
+        raise ValueError(message)
+
+
+def authenticate_sources():
+    here = Path(__file__).resolve()
+    root, package = here.parents[2], here.parent
+    manifest = json.loads((package / 'SOURCES.json').read_text())
+    rows = [row for row in manifest['files'] if row.get('usage') == 'input']
+    expected = {'research/etale-tensor-determinant-image/README.md',
+                'research/frobenius-tensor-characters/README.md',
+                'research/nonsplit-frobenius-characters/vendor/local.py',
+                'research/nonsplit-frobenius-characters/vendor/split-proof.md',
+                'research/nonsplit-frobenius-characters/vendor/ORIGINS.json'}
+    require(len(rows) == 5 and {row['path'] for row in rows} == expected,
+            'declared live source set differs from five pinned inputs')
+    for row in rows:
+        actual = hashlib.sha256((root / row['path']).read_bytes()).hexdigest()
+        require(actual == row['sha256'], 'source hash mismatch: '+row['path'])
+    return len(rows)
+
+
+def load_api():
+    path = Path(__file__).with_name('model.py')
+    spec = importlib.util.spec_from_file_location('nonsplit_model_target', path)
+    module = importlib.util.module_from_spec(spec)
+    spec.loader.exec_module(module)
+    return module
+
+
+def identity(n):
+    return [[int(i == j) for j in range(n)] for i in range(n)]
+
+
+def transpose(matrix):
+    return [list(column) for column in zip(*matrix)]
+
+
+def determinant(matrix, f):
+    rows = [list(row) for row in matrix]
+    out = 1
+    for j in range(len(rows)):
+        pivot = next((i for i in range(j, len(rows)) if rows[i][j]), None)
+        if pivot is None:
+            return 0
+        if pivot != j:
+            rows[j], rows[pivot] = rows[pivot], rows[j]
+            out = f.neg[out]
+        value = rows[j][j]
+        out = f.mul[out][value]
+        for i in range(j+1, len(rows)):
+            scale = f.neg[f.mul[rows[i][j]][f.inv[value]]]
+            for k in range(j, len(rows)):
+                rows[i][k] = f.add[rows[i][k]][f.mul[scale][rows[j][k]]]
+    return out
+
+
+def inverse(matrix, f):
+    n = len(matrix)
+    rows = [list(row)+unit for row, unit in zip(matrix, identity(n))]
+    for j in range(n):
+        pivot = next((i for i in range(j, n) if rows[i][j]), None)
+        require(pivot is not None, 'oracle matrix singular')
+        rows[j], rows[pivot] = rows[pivot], rows[j]
+        scale = f.inv[rows[j][j]]
+        rows[j] = [f.mul[scale][x] for x in rows[j]]
+        for i in range(n):
+            if i != j:
+                scale = f.neg[rows[i][j]]
+                rows[i] = [f.add[x][f.mul[scale][y]] for x, y in zip(rows[i], rows[j])]
+    return [row[n:] for row in rows]
+
+
+def mv(matrix, vector, f):
+    return [f.total(f.mul[x][y] for x, y in zip(row, vector)) for row in matrix]
+
+
+def mm(left, right, f):
+    return transpose([mv(left, column, f) for column in transpose(right)])
+
+
+def multiply(table, left, right, f):
+    out = [0]*len(table)
+    for i, x in enumerate(left):
+        if x:
+            for j, y in enumerate(right):
+                if y:
+                    scale = f.mul[x][y]
+                    for k, z in enumerate(table[i][j]):
+                        if z:
+                            out[k] = f.add[out[k]][f.mul[scale][z]]
+    return out
+
+
+class OracleExtension:
+    """Polynomial remainder arithmetic without the implementation's tables."""
+    def __init__(self, base, modulus):
+        self.base, self.modulus = base, list(modulus)
+        self.degree, self.q = len(modulus)-1, base.q**(len(modulus)-1)
+
+    def digits(self, value):
+        return [(value//self.base.q**r) % self.base.q for r in range(self.degree)]
+
+    def encode(self, values):
+        return sum(value*self.base.q**r for r, value in enumerate(values))
+
+    def add(self, a, b):
+        return self.encode([self.base.add[x][y] for x, y in zip(self.digits(a), self.digits(b))])
+
+    def multiply(self, a, b):
+        f, d = self.base, self.degree
+        product = [0]*(2*d-1)
+        for i, x in enumerate(self.digits(a)):
+            for j, y in enumerate(self.digits(b)):
+                product[i+j] = f.add[product[i+j]][f.mul[x][y]]
+        for k in range(2*d-2, d-1, -1):
+            coefficient = product[k]
+            for j in range(d):
+                correction = f.neg[f.mul[coefficient][self.modulus[j]]]
+                product[k-d+j] = f.add[product[k-d+j]][correction]
+        return self.encode(product[:d])
+
+    def power(self, a, exponent):
+        out = 1
+        for _ in range(exponent):
+            out = self.multiply(out, a)
+        return out
+
+
+def oracle_model(base, components, moduli):
+    factors = []
+    for d, heights in components:
+        extension = OracleExtension(base, moduli[d])
+        exponents = list(itertools.product(*(range(base.p**h) for h in heights)))
+        factors.append((extension, exponents, heights))
+    n = sum(extension.degree*len(exponents) for extension, exponents, _ in factors)
+    table, unit, offset = [[[0]*n for _ in range(n)] for _ in range(n)], [0]*n, 0
+    for extension, exponents, heights in factors:
+        d = extension.degree
+        unit[offset] = 1
+        positions = {powers: i for i, powers in enumerate(exponents)}
+        for i, a in enumerate(exponents):
+            for j, b in enumerate(exponents):
+                powers = tuple(x+y for x, y in zip(a, b))
+                if all(x < base.p**h for x, h in zip(powers, heights)):
+                    output = offset + d*positions[powers]
+                    for r in range(d):
+                        for s in range(d):
+                            value = extension.multiply(base.q**r, base.q**s)
+                            for t, coefficient in enumerate(extension.digits(value)):
+                                table[offset+i*d+r][offset+j*d+s][output+t] = coefficient
+        offset += d*len(exponents)
+    return table, unit
+
+
+def multiplier(table, value, f):
+    return transpose([multiply(table, value, unit, f) for unit in identity(len(table))])
+
+
+def endpoint(target, U, V, W, source, f):
+    uc, vc = transpose(U), transpose(V)
+    return all(multiply(target, uc[i], vc[j], f) == mv(W, source[i][j], f)
+               for i in range(len(source)) for j in range(len(source)))
+
+
+def is_automorphism(table, unit, matrix, f):
+    return mv(matrix, unit, f) == unit and endpoint(table, matrix, matrix, matrix, table, f)
+
+
+def transform(table, U, V, W, f):
+    uc, vc = transpose(inverse(U, f)), transpose(inverse(V, f))
+    return [[mv(W, multiply(table, x, y, f), f) for y in vc] for x in uc]
+
+
+def refused(action, message):
+    try:
+        action()
+    except (ValueError, TypeError):
+        return 1
+    raise ValueError('invalid input accepted: '+message)
+
+
+def instantiate(api, base, components, moduli):
+    residues = {d: api.Extension(base, modulus) for d, modulus in moduli.items()}
+    model = api.make_model(base, components, residues)
+    table, unit = oracle_model(base, components, moduli)
+    require(model['table'] == table and model['unit'] == unit, 'ground-field multiplication table mismatch')
+    return model, table, unit
+
+
+def compare_character(api, model, table, unit, image):
+    f = model['base']
+    for value in range(1, f.q):
+        if value in image:
+            got = api.automorphism(model, value)
+            matrix = got['matrix']
+            require(determinant(matrix, f) == value and is_automorphism(table, unit, matrix, f),
+                    'constructed automorphism failed independent matrix check')
+        else:
+            refused(lambda value=value: api.automorphism(model, value), 'outside automorphism determinant image')
+
+
+def tiny_exhaustions(api):
+    domains = [(2, [(2, [])], {2: [1, 1, 1]}, 2),
+               (3, [(2, [])], {2: [1, 0, 1]}, 2),
+               (2, [(3, [])], {3: [1, 1, 0, 1]}, 3),
+               (3, [(3, [])], {3: [2, 2, 0, 1]}, 3),
+               (2, [(1, []), (2, [])], {1: [0, 1], 2: [1, 1, 1]}, 2),
+               (3, [(1, []), (2, [])], {1: [0, 1], 2: [1, 0, 1]}, 2)]
+    reports = []
+    for p, components, moduli, expected in domains:
+        f = api.Field(p, [0, 1])
+        model, table, unit = instantiate(api, f, components, moduli)
+        n, gl_count, autos = len(table), 0, []
+        for entries in itertools.product(range(f.q), repeat=n*n):
+            matrix = [list(entries[i*n:(i+1)*n]) for i in range(n)]
+            if determinant(matrix, f):
+                gl_count += 1
+                if is_automorphism(table, unit, matrix, f):
+                    autos.append(matrix)
+        require(len(autos) == expected, 'tiny nonsplit automorphism count changed')
+        image = {determinant(matrix, f) for matrix in autos}
+        compare_character(api, model, table, unit, image)
+        units = [(list(value), multiplier(table, value, f))
+                 for value in itertools.product(range(f.q), repeat=n)]
+        units = [(value, matrix) for value, matrix in units if determinant(matrix, f)]
+        triples, count = set(), 0
+        for phi in autos:
+            for u, mu in units:
+                for v, nu in units:
+                    U, V = mm(mu, phi, f), mm(nu, phi, f)
+                    W = mm(multiplier(table, multiply(table, u, v, f), f), phi, f)
+                    require(endpoint(table, U, V, W, table, f), 'tiny normalized autotopism failed')
+                    triples.add(tuple(determinant(matrix, f) for matrix in (U, V, W)))
+                    count += 1
+        for wanted in itertools.product(range(1, f.q), repeat=3):
+            if wanted in triples:
+                got = api.autotopism(model, *wanted)
+                matrices = [got[key] for key in ('U', 'V', 'W')]
+                require(tuple(determinant(matrix, f) for matrix in matrices) == wanted,
+                        'tiny constructed autotopism determinant mismatch')
+                require(endpoint(table, *matrices, table, f), 'tiny constructed autotopism endpoint mismatch')
+            else:
+                refused(lambda wanted=wanted: api.autotopism(model, *wanted), 'tiny outside determinant triple')
+        reports.append({'p': p, 'components': components, 'dimension': n,
+                        'all_matrices': f.q**(n*n), 'invertible_matrices': gl_count,
+                        'automorphisms': len(autos), 'determinant_image': sorted(image),
+                        'units': len(units), 'normalized_autotopisms': count,
+                        'determinant_triples': [list(t) for t in sorted(triples)]})
+    return reports
+
+
+def polynomial_product(a, b, extension):
+    out = [0]*len(a)
+    for i, x in enumerate(a):
+        for j in range(len(a)-i):
+            if x and b[j]:
+                out[i+j] = extension.add(out[i+j], extension.multiply(x, b[j]))
+    return out
+
+
+def substitution(extension, length, coefficients, frobenius_power=0):
+    f, d = extension.base, extension.degree
+    powers, current = [], [1]+[0]*(length-1)
+    for _ in range(length):
+        powers.append(current)
+        current = polynomial_product(current, coefficients, extension)
+    require(not any(current), 'substitution violates nilpotent relation')
+    images = []
+    for power in powers:
+        for r in range(d):
+            coefficient = extension.power(f.q**r, f.q**frobenius_power)
+            images.append([c for value in power
+                           for c in extension.digits(extension.multiply(coefficient, value))])
+    return transpose(images)
+
+
+def nilpotent_exhaustions(api):
+    reports = []
+    for p, modulus, expected in [(2, [1, 1, 1], 6), (3, [1, 0, 1], 144)]:
+        f = api.Field(p, [0, 1])
+        model, table, unit = instantiate(api, f, [(2, [1])], {2: modulus})
+        extension = OracleExtension(f, modulus)
+        count, image = 0, set()
+        for frobenius in range(2):
+            for linear in range(1, extension.q):
+                for tail in itertools.product(range(extension.q), repeat=p-2):
+                    matrix = substitution(extension, p, [0, linear, *tail], frobenius)
+                    require(is_automorphism(table, unit, matrix, f), 'nilpotent substitution endpoint failed')
+                    value = determinant(matrix, f)
+                    require(value != 0, 'nilpotent substitution singular')
+                    image.add(value)
+                    count += 1
+        require(count == expected, 'nilpotent complete substitution count changed')
+        compare_character(api, model, table, unit, image)
+        reports.append({'p': p, 'residue_degree': 2, 'height': 1, 'dimension': len(table),
+                        'complete_automorphism_substitutions': count, 'determinant_image': sorted(image)})
+    return reports
+
+
+def strong_controls(api):
+    f = api.Field(3, [1, 0, 1])
+    beta = 4  # 1+t, encoded in base 3; t^2=-1.
+    require(f.power(beta, 4) == f.neg[1] and f.power(beta, 8) == 1,
+            'specified F9 primitive element changed')
+    modulus = [f.neg[beta], 0, 1]
+    extension = OracleExtension(f, modulus)
+    actual_extension = api.Extension(f, modulus)
+    multiplication_checks = 0
+    for a, b in itertools.product(range(extension.q), repeat=2):
+        require(extension.multiply(a, b) == actual_extension.mul[a][b], 'extension multiplication differs')
+        multiplication_checks += 1
+    for a in range(1, extension.q):
+        matrix = transpose([extension.digits(extension.multiply(a, f.q**r)) for r in range(2)])
+        require(determinant(matrix, f) == actual_extension.norm(a), 'norm differs from ground-field determinant')
+    model, table, unit = instantiate(api, f, [(2, [1])], {2: modulus})
+    u = f.q
+    scaling = substitution(extension, 3, [0, u, 0])
+    expected = f.power(beta, 7)
+    require(determinant(scaling, f) == expected and is_automorphism(table, unit, scaling, f),
+            'F81 nilpotent scaling determinant is not beta^7')
+    require(len({f.power(expected, k) for k in range(8)}) == 8, 'strong determinant does not have order eight')
+    image, direct_cases = set(), 0
+    for a in range(1, extension.q):
+        matrix = substitution(extension, 3, [0, a, 0])
+        require(is_automorphism(table, unit, matrix, f), 'F81 linear substitution endpoint failed')
+        image.add(determinant(matrix, f)); direct_cases += 1
+    for tail in (1, beta, u, extension.add(1, u)):
+        for frobenius in range(2):
+            matrix = substitution(extension, 3, [0, u, tail], frobenius)
+            require(is_automorphism(table, unit, matrix, f), 'F81 nonlinear substitution endpoint failed')
+            direct_cases += 1
+    require(image == set(range(1, f.q)), 'linear substitution determinants fail to fill F9 multiplicative group')
+    compare_character(api, model, table, unit, image)
+    wrong_extra_degree = {f.mul[value][value] for value in image}
+    require(len(wrong_extra_degree) == 4 and expected not in wrong_extra_degree,
+            'extra residue-degree exponent control failed')
+    # Ground F3, coefficient field F9, local nilpotent length nine.
+    ground = api.Field(3, [0, 1])
+    residue = OracleExtension(ground, [1, 0, 1])
+    model18, table18, unit18 = instantiate(api, ground, [(2, [2])], {2: [1, 0, 1]})
+    local_scaling_dets = set()
+    for a in range(1, residue.q):
+        matrix = substitution(residue, 9, [0, a]+[0]*7)
+        require(is_automorphism(table18, unit18, matrix, ground), 'length-nine coefficient scaling failed')
+        local_scaling_dets.add(determinant(matrix, ground))
+    frobenius = substitution(residue, 9, [0, 1]+[0]*7, 1)
+    require(local_scaling_dets == {1} and determinant(frobenius, ground) == 2,
+            'coefficient Frobenius sign correction missing')
+    require(is_automorphism(table18, unit18, frobenius, ground), 'coefficient Frobenius endpoint failed')
+    compare_character(api, model18, table18, unit18, {1, 2})
+    odd_pair, odd_table, odd_unit = instantiate(api, ground, [(3, []), (3, [])],
+                                               {3: [2, 2, 0, 1]})
+    swap = [[int(j == (i+3) % 6) for j in range(6)] for i in range(6)]
+    require(determinant(swap, ground) == 2 and is_automorphism(odd_table, odd_unit, swap, ground),
+            'repeated odd residue-degree block swap failed')
+    require(api.component_swap(odd_pair, 0, 1) == swap, 'constructed component swap differs')
+    compare_character(api, odd_pair, odd_table, odd_unit, {1, 2})
+    return {'base_field_size': 9, 'residue_field_size': 81, 'beta': beta,
+            'scaling_x_to_u_x_determinant': expected, 'determinant_order': 8,
+            'independent_extension_products': multiplication_checks, 'independent_norm_checks': 80,
+            'checked_F81_substitutions': direct_cases, 'F81_linear_scaling_image': sorted(image),
+            'wrong_extra_degree_image': sorted(wrong_extra_degree),
+            'F9_x9_over_F3_scaling_determinants': sorted(local_scaling_dets),
+            'F9_x9_over_F3_coefficient_frobenius_determinant': 2,
+            'F27_pair_over_F3_component_swap_determinant': 2,
+            'scope': '80 linear and 8 nonlinear F81 substitutions checked, not all12960 automorphisms.'}
+
+
+def coefficient_action(table, A, B, C, f):
+    n = len(table)
+    support = [(r, s, t, table[r][s][t]) for r, s, t in itertools.product(range(n), repeat=3)
+               if table[r][s][t]]
+    for i, j, k in itertools.product(range(n), repeat=3):
+        value = 0
+        for r, s, t, coefficient in support:
+            scale = f.mul[f.mul[A[i][r]][B[j][s]]][f.mul[C[k][t]][coefficient]]
+            value = f.add[value][scale]
+        if value != table[i][j][k]:
+            return False
+    return True
+
+
+def covariant_controls(api):
+    f = api.Field(3, [1, 0, 1])
+    model, table, _ = instantiate(api, f, [(1, [2])], {1: [0, 1]})
+    residue = OracleExtension(f, [0, 1])
+    image = {determinant(substitution(residue, 9, [0, a]+[0]*7), f) for a in range(1, f.q)}
+    require(image == {1, f.neg[1]}, 'proper-subgroup scaling fixture changed')
+    accepted, rejected = 0, 0
+    # Exhaust determinant triples, not all maps in their stabilizer fibres.
+    for wanted in itertools.product(range(1, f.q), repeat=3):
+        if f.mul[f.mul[wanted[0]][wanted[1]]][wanted[2]] in image:
+            got = api.covariant_stabilizer(model, *wanted)
+            matrices = [got[key] for key in ('A', 'B', 'C')]
+            require(tuple(determinant(matrix, f) for matrix in matrices) == wanted,
+                    'covariant determinant mismatch')
+            require(coefficient_action(table, *matrices, f), 'literal covariant coefficient action failed')
+            accepted += 1
+        else:
+            rejected += refused(lambda wanted=wanted: api.covariant_stabilizer(model, *wanted),
+                                'outside proper covariant subgroup')
+    phi = substitution(residue, 9, [0, 1, 1]+[0]*6)
+    inv_phi = inverse(phi, f)
+    require(coefficient_action(table, transpose(inv_phi), transpose(inv_phi), phi, f),
+            'nonlinear inverse-transpose check failed')
+    require(not coefficient_action(table, inv_phi, inv_phi, phi, f),
+            'missing transpose mutation escaped')
+    return {'base_field_size': 9, 'dimension': 9, 'accepted_covariant_triples': accepted,
+            'rejected_covariant_triples': rejected, 'nonlinear_missing_transpose_rejected': True}
+
+
+def shear(n, f, shift):
+    matrix = identity(n)
+    for i in range(n):
+        j = (i+1+shift) % n
+        if i != j:
+            matrix[i] = [f.add[x][y] for x, y in zip(matrix[i], matrix[j])]
+    return matrix
+
+
+def certificate_controls(api):
+    f = api.Field(3, [1, 0, 1])
+    model, table, _ = instantiate(api, f, [(1, [2])], {1: [0, 1]})
+    n = len(table)
+    U, V, W = shear(n, f, 0), shear(n, f, 2), shear(n, f, 4)
+    U[0] = [f.mul[4][x] for x in U[0]]
+    V[0] = [f.mul[f.inv[4]][x] for x in V[0]]
+    target = transform(table, U, V, W, f)
+    got = api.validate_certificate(model, target, U, V, W)
+    require(got['label'] == 1 and endpoint(target, U, V, W, table, f),
+            'independent factor-basis certificate failed')
+    count = 0
+    for key in ('U', 'V', 'W'):
+        maps = {'U': copy.deepcopy(U), 'V': copy.deepcopy(V), 'W': copy.deepcopy(W)}
+        maps[key][0][0] = f.add[maps[key][0][0]][1]
+        count += refused(lambda maps=maps: api.validate_certificate(model, target, **maps), 'changed factor map')
+    changed = copy.deepcopy(target); changed[0][0][0] = f.add[changed[0][0][0]][1]
+    count += refused(lambda: api.validate_certificate(model, changed, U, V, W), 'changed tensor')
+    count += refused(lambda: api.validate_certificate(model, target, U[:-1], V, W), 'wrong matrix shape')
+    count += refused(lambda: api.validate_certificate(model, target, [[0]*n for _ in range(n)], V, W), 'singular matrix')
+    for invalid in (-1, f.q, True, 0.5):
+        changed = copy.deepcopy(U); changed[0][0] = invalid
+        count += refused(lambda changed=changed: api.validate_certificate(model, target, changed, V, W),
+                         'noncanonical matrix entry')
+        changed = copy.deepcopy(target); changed[0][0][0] = invalid
+        count += refused(lambda changed=changed: api.validate_certificate(model, changed, U, V, W),
+                         'noncanonical tensor entry')
+    other_U = identity(n); other_U[0][0] = 4
+    other_table = transform(table, other_U, identity(n), identity(n), f)
+    other = api.validate_certificate(model, other_table, other_U, identity(n), identity(n))
+    require(other['label'] != got['label'], 'distinct determinant cosets have equal labels')
+    return {'dimension': n, 'changed_or_malformed_certificates_rejected': count,
+            'independent_three_factor_bases_checked': True, 'different_coset_labels_distinguished': True}
+
+
+def presentation_controls(api):
+    f2, f3 = api.Field(2, [0, 1]), api.Field(3, [0, 1])
+    f9, alt9 = api.Field(3, [1, 0, 1]), api.Field(3, [2, 1, 1])
+    count = 0
+    count += refused(lambda: api.Extension(f3, [0, 0, 1]), 'reducible residue polynomial')
+    alt_primitive = next(a for a in range(1, alt9.q)
+                         if len({alt9.power(a, k) for k in range(8)}) == 8)
+    valid_over_alternate_base = api.Extension(alt9, [alt9.neg[alt_primitive], 0, 1])
+    count += refused(lambda: api.make_model(f9, [(2, [])], {2: valid_over_alternate_base}),
+                     'different ground field presentation')
+    count += refused(lambda: api.make_model(f3, [(3, [])], {3: api.Extension(f3, [1, 0, 1])}),
+                     'declared residue degree mismatch')
+    count += refused(lambda: api.make_model(f3, [(2, []), (1, [])],
+                                            {1: api.Extension(f3, [0, 1]), 2: api.Extension(f3, [1, 0, 1])}),
+                     'noncanonical component order')
+    first = api.make_model(f3, [(2, [])], {2: api.Extension(f3, [1, 0, 1])})
+    second = api.make_model(f3, [(2, [])], {2: api.Extension(f3, [2, 1, 1])})
+    count += refused(lambda: api.model_isomorphism(first, second), 'alternate residue presentation')
+    cyclic = api.make_model(f2, [(1, [2])])
+    nonsplit = api.make_model(f2, [(2, [1])], {2: api.Extension(f2, [1, 1, 1])})
+    require(cyclic['n'] == nonsplit['n'] == 4, 'same-dimension type control changed')
+    count += refused(lambda: api.model_isomorphism(cyclic, nonsplit), 'same dimension different residue type')
+    count += refused(lambda: api.validate_certificate(cyclic, nonsplit['table'],
+                                                       identity(4), identity(4), identity(4)),
+                     'same-dimensional different-type multiplication table')
+    square = api.make_model(f2, [(1, [1, 1])])
+    count += refused(lambda: api.model_isomorphism(cyclic, square), 'same dimension different height type')
+    require(api.model_isomorphism(first, first) == identity(2), 'identity model isomorphism failed')
+    return {'presentation_or_type_rejections': count, 'same_dimension_different_types_checked': True}
+
+
+def run():
+    sources = authenticate_sources()
+    api = load_api()
+    return {'status': 'PASS_NONSPLIT_FROBENIUS_CHARACTERS',
+            'authenticated_source_files': sources,
+            'tiny_full_GL_exhaustions': tiny_exhaustions(api),
+            'nilpotent_substitution_exhaustions': nilpotent_exhaustions(api),
+            'strong_norm_and_frobenius_controls': strong_controls(api),
+            'covariant_controls': covariant_controls(api),
+            'certificate_controls': certificate_controls(api),
+            'presentation_controls': presentation_controls(api),
+            'scope': 'Finite exact matrices support the separate theorem; large automorphism groups and tensor recognition are not exhausted.'}
+
+
+if __name__ == '__main__':
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('--json', action='store_true')
+    args = parser.parse_args()
+    report = run()
+    if args.json:
+        print(json.dumps(report, indent=2, sort_keys=True))
+    else:
+        print(report['status'])
+        print(json.dumps({key: value for key, value in report.items() if key != 'status'}, sort_keys=True))