From 808d31b2016ee666ef637e2cc5d1118f5fdd29c0 Mon Sep 17 00:00:00 2001
From: apoursh <8867770+apoursh@users.noreply.github.com>
Date: Sun, 25 Oct 2026 23:46:34 -0400
Subject: [PATCH 1/3] research: retain exact nonsplit-character predecessor
 inputs

---
 .../vendor/ORIGINS.json                       |  21 +
 .../vendor/local.py                           | 370 ++++++++++++++++++
 .../vendor/split-proof.md                     | 350 +++++++++++++++++
 3 files changed, 741 insertions(+)
 create mode 100644 research/nonsplit-frobenius-characters/vendor/ORIGINS.json
 create mode 100644 research/nonsplit-frobenius-characters/vendor/local.py
 create mode 100644 research/nonsplit-frobenius-characters/vendor/split-proof.md

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.

From 868167f18d1c90aac7fa33b052e623352b129043 Mon Sep 17 00:00:00 2001
From: apoursh <8867770+apoursh@users.noreply.github.com>
Date: Sun, 25 Oct 2026 23:52:42 -0400
Subject: [PATCH 2/3] research: derive nonsplit Frobenius tensor characters

---
 .../nonsplit-frobenius-characters/PROOF.md    | 466 ++++++++++++++++
 .../nonsplit-frobenius-characters/README.md   | 166 ++++++
 .../nonsplit-frobenius-characters/RESULT.json | 324 +++++++++++
 .../SOURCES.json                              |  51 ++
 .../nonsplit-frobenius-characters/TASK.json   | 111 ++++
 .../VALIDATION.md                             |  77 +++
 .../nonsplit-frobenius-characters/VERIFY.json |  40 ++
 .../nonsplit-frobenius-characters/model.py    | 416 ++++++++++++++
 .../nonsplit-frobenius-characters/verify.py   | 528 ++++++++++++++++++
 9 files changed, 2179 insertions(+)
 create mode 100644 research/nonsplit-frobenius-characters/PROOF.md
 create mode 100644 research/nonsplit-frobenius-characters/README.md
 create mode 100644 research/nonsplit-frobenius-characters/RESULT.json
 create mode 100644 research/nonsplit-frobenius-characters/SOURCES.json
 create mode 100644 research/nonsplit-frobenius-characters/TASK.json
 create mode 100644 research/nonsplit-frobenius-characters/VALIDATION.md
 create mode 100644 research/nonsplit-frobenius-characters/VERIFY.json
 create mode 100644 research/nonsplit-frobenius-characters/model.py
 create mode 100644 research/nonsplit-frobenius-characters/verify.py

diff --git a/research/nonsplit-frobenius-characters/PROOF.md b/research/nonsplit-frobenius-characters/PROOF.md
new file mode 100644
index 0000000000..6ec914a20a
--- /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/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))

From d72b2e42a4cf53ae85f5276da65c5cc84e17b253 Mon Sep 17 00:00:00 2001
From: apoursh <8867770+apoursh@users.noreply.github.com>
Date: Sun, 25 Oct 2026 23:54:15 -0400
Subject: [PATCH 3/3] docs: render nonsplit character formulas in GitHub
 Markdown

---
 .../nonsplit-frobenius-characters/PROOF.md    | 140 +++++++++---------
 1 file changed, 70 insertions(+), 70 deletions(-)

diff --git a/research/nonsplit-frobenius-characters/PROOF.md b/research/nonsplit-frobenius-characters/PROOF.md
index 6ec914a20a..66178c0eb7 100644
--- a/research/nonsplit-frobenius-characters/PROOF.md
+++ b/research/nonsplit-frobenius-characters/PROOF.md
@@ -14,24 +14,24 @@ 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,
@@ -52,27 +52,27 @@ one of these conditions holds:
 
 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
@@ -84,7 +84,7 @@ 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}.
+$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
@@ -92,9 +92,9 @@ 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
@@ -103,15 +103,15 @@ 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
+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;
@@ -122,17 +122,17 @@ when K is nonprime, p-Frobenius need not be K-linear.
 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.
@@ -156,17 +156,17 @@ 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
@@ -178,32 +178,32 @@ 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*.
+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,
+$\{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
+$\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
@@ -232,7 +232,7 @@ 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.
+$\langle\zeta^g\rangle=H_g$, proving the first assertion of the theorem.
 
 ## 5. Unit determinants remain surjective
 
@@ -241,11 +241,11 @@ 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
+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
@@ -255,38 +255,38 @@ possible determinant.
 
 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
+$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
+$(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.
@@ -303,13 +303,13 @@ independent input and output bases.
 
 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
+$\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
@@ -331,9 +331,9 @@ algorithm, a normal-basis construction, or arbitrary tensor recognition.
 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.
@@ -351,26 +351,26 @@ 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
+$(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
+$(-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
@@ -399,21 +399,21 @@ the allowed K-linear factor maps.
 
 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\).
+$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