diff --git a/research/mixed-singular-kronecker-characters/.gitattributes b/research/mixed-singular-kronecker-characters/.gitattributes
new file mode 100644
index 0000000000..7467454cb8
--- /dev/null
+++ b/research/mixed-singular-kronecker-characters/.gitattributes
@@ -0,0 +1 @@
+source/** -text
diff --git a/research/mixed-singular-kronecker-characters/INPUTS.json b/research/mixed-singular-kronecker-characters/INPUTS.json
new file mode 100644
index 0000000000..8422e5b210
--- /dev/null
+++ b/research/mixed-singular-kronecker-characters/INPUTS.json
@@ -0,0 +1,23 @@
+[
+  {
+    "local": "source/pencil.py",
+    "path": "research/kronecker-determinant-image/pencil.py",
+    "commit": "81c0577b83cdafa73346da8ade1261b0b202e45f",
+    "sha256": "a714862853cc884e84eac34ba1d7ccb14a6326bcfadb630910034bb44bd305db",
+    "git_blob": "6bc7fc076e6ce2418ec9ed05d85115deb3d4bdd2"
+  },
+  {
+    "local": "source/PROOF.md",
+    "path": "research/kronecker-determinant-image/PROOF.md",
+    "commit": "81c0577b83cdafa73346da8ade1261b0b202e45f",
+    "sha256": "7cc6f1845e15ccc3c8867680cadb8366008143815001be7d790ddc811f63a89b",
+    "git_blob": "77ff305e1c31bfec96e50585872a0a5fa420de20"
+  },
+  {
+    "local": "source/README.md",
+    "path": "research/kronecker-determinant-image/README.md",
+    "commit": "81c0577b83cdafa73346da8ade1261b0b202e45f",
+    "sha256": "7e15e74abb9fa45537b5b6986f016ab54981f085ad52d1e69e0e973bc63b9447",
+    "git_blob": "eed3f5378d4a58e603e492ad2ef22b40f2703260"
+  }
+]
diff --git a/research/mixed-singular-kronecker-characters/NOTICE.md b/research/mixed-singular-kronecker-characters/NOTICE.md
new file mode 100644
index 0000000000..1a9962a849
--- /dev/null
+++ b/research/mixed-singular-kronecker-characters/NOTICE.md
@@ -0,0 +1,7 @@
+# Attribution
+
+apoursh PR5672 supplies the single-index/multiplicity determinant theorem, the exact covariant action, characteristic-safe symmetric-power lifts and the retained F2/F3/F4/F5 arithmetic. Its PROOF.md, README.md and pencil.py are preserved unchanged under source/ and authenticated before use.
+
+Nick Petalas PR5250 supplies the singular-pencil handoff. David Ganz's A030/A026/A029 tensor atlas and the classical Kronecker and symmetric-power theory retain their source credit. No literature-priority claim is made.
+
+New complete mixed-index and mixed-orientation proof, zero-index treatment, Hom basis, power-subgroup character, independent coefficient-equation oracle and supplied-map SL correction: Ali Romman with substantial OpenAI Codex assistance. No subagents or independent human review are claimed. New material is Apache-2.0.
diff --git a/research/mixed-singular-kronecker-characters/PROOF.md b/research/mixed-singular-kronecker-characters/PROOF.md
new file mode 100644
index 0000000000..9de07b6280
--- /dev/null
+++ b/research/mixed-singular-kronecker-characters/PROOF.md
@@ -0,0 +1,146 @@
+# Determinant characters for all purely singular Kronecker sums
+
+## 1. Scope and action
+
+Let K be any field. Let R_e be the e by e+1 pencil with s on the diagonal and t above it, and let L_e=R_e^T be its left orientation. The predecessor calls the right block L_e; this note uses R and L to mark the two orientations. Minimal indices e can be zero. Thus R_0 has shape 0 by 1 and L_0 has shape 1 by 0.
+
+Let T be a finite direct sum of these blocks with positive multiplicities. Combine repeated equal types. Both total row and column dimensions m,n must be positive. The result does not include a regular block. The model is supplied; extraction from an arbitrary tensor is a separate task.
+
+Use exactly the predecessor's covariant action
+
+`(A0,A1) -> (P(a A0+b A1)Q^T, P(c A0+d A1)Q^T)`,
+
+where `R=[[a,b],[c,d]]` is the slice factor. Let Delta(T) be the image of its stabilizer under `(det P,det Q,det R)`. The right factor is Q^T, not Q^-1. All pencil equations are coefficient identities in two independent indeterminates, including over finite fields.
+
+The source is apoursh PR5672 at `81c0577b83cdafa73346da8ade1261b0b202e45f`, following Nick Petalas PR5250. Its single-type theorem, characteristic-safe slice lift and exact action convention remain predecessor work. This note supplies the complete mixed singular extension.
+
+## 2. Explicit intertwiner spaces
+
+A morphism from a source block to a destination block is a pair U,C with
+
+`U T_source(s,t)=T_destination(s,t) C`.
+
+For a source with shape ms by ns and destination with shape md by nd, U has shape md by ms and C has shape nd by ns. Comparing the s and t coefficients gives the following complete table:
+
+| Source | Destination | Dimension | Form |
+| --- | --- | ---: | --- |
+| R_e | R_f | max(e-f+1,0) | Rectangular upper Toeplitz |
+| L_e | L_f | max(f-e+1,0) | Transpose dual of the preceding row |
+| R_e | L_f | 0 | Zero |
+| L_e | R_f | e+f | Rectangular Hankel |
+
+Here are explicit bases and completeness arguments. For R_e to R_f with e>=f, choose coefficients a_0,...,a_(e-f). Put `C_(i,j)=a_(j-i)` for `0<=i<=f`, `0<=j<=e`, with coefficients outside that range zero. Use the same rule for U on `0<=i<f`, `0<=j<e`. The coefficient equations force each diagonal to be constant, with both boundary edges zero outside the displayed range. If e<f, those boundary conditions force every entry to zero. This proves both spanning and independence. It also covers e=0 or f=0.
+
+Transposing the equation identifies L_e to L_f with R_f to R_e, exchanging and transposing the two matrices. This gives the second row in every characteristic.
+
+For R_e to L_f, the top t-coefficient gives U_(0,j)=0 for every j. The s-coefficients then make the first row of C zero, including its last entry. The interior relation C_(i+1,j)=C_(i,j+1), together with the zero last column, makes every later row zero. The remaining coefficient equations make U zero. If an index is zero, the remaining pencil has no nonzero constant polynomial kernel of the required orientation, or the two matrices have no entries. Thus the third row is zero without an exception.
+
+For L_e to R_f, choose a_0,...,a_(e+f-1). Set
+
+`U_(i,j)=a_(i+j)`, for `0<=i<f`, `0<=j<=e`,
+
+`C_(i,j)=a_(i+j)`, for `0<=i<=f`, `0<=j<e`.
+
+The two coefficient equations say precisely that successive antidiagonals agree. They impose no further boundary condition. These e+f coefficients are independent. When e=f=0 there are none.
+
+Multiplicities replace each scalar coefficient by an arbitrary matrix from the source multiplicity space to the destination multiplicity space. This includes all off-diagonal mixing; it is not a block-diagonal assumption.
+
+## 3. Complete fixed-slice determinant image
+
+Order distinct types as right blocks in increasing index, followed by left blocks in decreasing index. Section 2 makes every morphism between different types upper triangular in this order. On one repeated right type of index e and multiplicity r, a diagonal morphism is
+
+`P=I_e tensor D`, `C=I_(e+1) tensor D`.
+
+For a left type the two dimensions are exchanged. This includes zero indices: the nonempty diagonal matrix still determines D. A simultaneous automorphism requires and is implied by invertibility of every diagonal D. Its off-diagonal blocks do not change either determinant.
+
+For a fixed slice action, put `C=Q^-T`. The two stabilizer equations are `P A_i=A_i C`. Hence the preceding morphism analysis gives every fixed-slice stabilizer, including its nonzero off-diagonal entries.
+
+Parameterize the right-type determinant by u=det D. Parameterize a left type by u=(det D)^-1, to retain the predecessor's transposed lift convention. Each distinct type contributes a vector
+
+`v_R(e)=(e,-e-1)`, `v_L(e)=(-e-1,e)`
+
+to the exponents of `(det P,det Q)`. Every u in K* occurs, by a diagonal multiplicity matrix. Multiplicity does not multiply these two exponents: it is the determinant of the full GL_r matrix that is free.
+
+Thus the fixed-slice image is exactly
+
+`{(product_i u_i^(v_i,1), product_i u_i^(v_i,2), 1): u_i in K*}`.
+
+## 4. All slice actions and multiplicities
+
+For every `R in GL2(K)`, let z=det R. The predecessor's polynomial-substitution matrices S_k(R) use ordinary monomials, not divided powers or factorial inverses. Their determinant is `z^(k(k+1)/2)` in every characteristic. A right block of positive index e and multiplicity r has the explicit lift
+
+`P_R=S_(e-1)(R)^T tensor I_r`,
+
+`Q_R=S_e(R)^-1 tensor I_r`.
+
+Its determinant shift is `(z^(r e(e-1)/2),z^(-r e(e+1)/2))`. A left block exchanges these two matrices and shifts. A zero-index block is identically zero and uses identity on its nonempty factor. Its shift exponents are zero, as the same integer formulas require.
+
+Take the direct sum of these lifts. Define the integers
+
+`A = sum_right r e(e-1)/2 - sum_left r e(e+1)/2`,
+
+`B = -sum_right r e(e+1)/2 + sum_left r e(e-1)/2`.
+
+The quotient of any other stabilizer with this same R and this lift fixes the unmixed pencil. Section 3 gives its complete determinant image. Conversely each of those fixed-slice factors can be composed with the lift. Therefore
+
+`Delta(T) = {(z^A product_i u_i^(v_i,1), z^B product_i u_i^(v_i,2), z): u_i,z in K*}`.  (1)
+
+The lift works for every prescribed matrix R of determinant z, not only a diagonal representative. All half-products above are integer exponents. There is no division by two in K.
+
+## 5. One exact character and its power subgroup
+
+Choose a base type. For a right base index e0 set `ell=(e0+1,e0)`; for a left base set `ell=(e0,e0+1)`. In both cases ell has coprime entries and `ell dot v0=0`. Put
+
+`c_i=ell dot v_i`, `d=gcd_i(c_i)>=0`.
+
+The gcd of an all-zero list is zero. Define
+
+`chi(x,y,z)=x^ell1 y^ell2 z^(-ell1 A-ell2 B)`.
+
+**Theorem.** For every field K,
+
+`Delta(T) = {(x,y,z) in (K*)^3 : chi(x,y,z) in (K*)^d}`.  (2)
+
+Here `(K*)^0={1}`. This convention recovers the exact equality for a single distinct block type.
+
+For necessity, apply chi to (1). Its value is `product_i u_i^c_i`, which is a d-th power when d>0 and is one when d=0.
+
+For sufficiency with d>0, let `w^d=chi(x,y,z)`. Choose integer Bezout coefficients b_i with `sum_i b_i c_i=d`, and set `u_i=w^b_i`. Remove the slice shifts and these u_i contributions from x,y, leaving X,Y with `X^ell1 Y^ell2=1`. For either base orientation, `a=(XY)^-1` supplies exactly the residual pair through `a^v0`. Multiply a into u_0. Equation (1) and the explicit block lifts now construct the requested stabilizer. When d=0, start with every u_i=1 and make the same kernel correction. No root is then needed.
+
+Over an arbitrary field, membership in the power subgroup includes the existence of w; a constructive witness can take w as input. The theorem does not assume an algorithm that extracts arbitrary roots in K. The bounded finite-field executable finds w by enumerating the at most q-1 nonzero elements.
+
+The kernel correction is elementary. For a right base, `X^(e0+1)Y^e0=1` gives `(XY)^(-e0)=X` and `(XY)^(e0+1)=Y`. For a left base, exchange X and Y. These formulas include e0=0.
+
+The primitive vector v0 can be completed to an integral basis. Hence d is also the gcd of all two-by-two minors of the type vectors. These minors are, up to sign,
+
+- Differences of two right indices.
+- Differences of two left indices.
+- Sums e+f+1 for a right index e and a left index f.
+
+This is a direct criterion using the full type list. It is independent of multiplicities. Multiplicities still affect A,B and therefore the actual character label; they cannot be dropped from the slice shift.
+
+## 6. Special-linear orbit labels and constructive correction
+
+Because m,n are positive, the determinant map from `GL_m(K) x GL_n(K) x GL_2(K)` onto `(K*)^3` is surjective, with kernel the product of the three special linear groups. Its orbits inside one GL orbit are therefore the cosets of Delta(T).
+
+The map chi is surjective onto K*: for a right base use `(x,y,z)=(u,u^-1,1)`, and for a left base exchange x,y. Equation (2) gives a complete label group
+
+`K*/(K*)^d`.
+
+Over F_q, the exact number of special-linear orbits is
+
+`gcd(q-1,d)`, with `gcd(q-1,0)=q-1`.
+
+For example, consecutive right indices give d=1 and one SL orbit. R_1 plus L_1 has d=3 and gives three SL orbits over F4. R_1 plus L_2 has d=4 and gives four over F5. Zero-index factors are included whenever both full factor dimensions are positive. In particular, a sum of R_0 and L_0 is a zero pencil with full determinant image, as d=1 requires.
+
+If a supplied GL map g has determinant triple in Delta(T), choose the stabilizer witness h with that same triple. Then `g h^-1` has determinant one in every factor and has the same action on T as g. This gives a literal SL correction when the model and map are supplied. It does not discover a canonical model or a GL map from an arbitrary tensor. Equal labels similarly give an SL transporter between two supplied presentations by composing their maps and the appropriate stabilizer witness.
+
+## 7. Verification boundary and use
+
+The exact verifier checks the Hom formulas against literal coefficient equations for every ordered pair of orientations and indices zero through three over F2, F3, F4 and F5. It then solves the full mixed stabilizer equations in twelve declared domains, enumerates every vector in each resulting linear solution space, and retains precisely invertible P,C. It uses neither the character formula nor the symmetric-power lift in that oracle. Cases marked with all_slice_actions cover every GL2 action. The other cases cover one representative for every nonzero slice determinant, with every GL2 action separately checked by literal constructed lifts.
+
+The finite evidence supports the all-field proof. It is not an exhaustive enumeration over all indices, dimensions or fields. The executable restricts indices to zero through five, combined multiplicities to one through three, fields to F2/F3/F4/F5, and both total factor dimensions to at most sixteen. The written proof has no such bounds.
+
+This closes the supplied purely singular determinant-character interface in the tensor atlas. Native realization, dirty-state ownership, movement, restoration, storage, precision and the complete recursive cost remain unknown. Regular blocks, arbitrary-tensor extraction and a paid multiplication consumer are outside the result. No new kappa, selected-frontier change, human acceptance or proof-kernel verification is claimed.
+
+New proof and checks: Ali Romman with substantial OpenAI Codex assistance. Credit apoursh PR5672; Nick Petalas PR5250; David Ganz's A030/A026/A029 atlas and the classical Kronecker and symmetric-power lineage. The source notice and action conventions remain unchanged.
diff --git a/research/mixed-singular-kronecker-characters/README.md b/research/mixed-singular-kronecker-characters/README.md
new file mode 100644
index 0000000000..7e1b969cc7
--- /dev/null
+++ b/research/mixed-singular-kronecker-characters/README.md
@@ -0,0 +1,48 @@
+# Mixed singular Kronecker determinant characters
+
+This completes the determinant-character question for every supplied direct sum of singular Kronecker blocks. It includes unequal indices, both orientations, arbitrary multiplicities and zero-index blocks, provided both full factor dimensions are positive. The theorem holds over every field. Regular blocks and discovery from an arbitrary tensor are separate problems. **No new kappa is claimed.**
+
+Write a right index-e block as R_e and its transpose as L_e. Each distinct right type contributes the integer vector `(e,-e-1)`; each left type contributes `(-e-1,e)`. The complete determinant image is generated by these multiplicity determinants and the explicit common GL2 slice lift. All off-diagonal intertwiners are included in the proof.
+
+Choose one type vector v0 and a primitive integer row ell that annihilates it. Let `d=gcd_i(ell dot v_i)`. With the exact slice exponents A,B in [PROOF.md](PROOF.md), a triple (x,y,z) occurs precisely when
+
+`x^ell1 * y^ell2 * z^(-ell1*A-ell2*B)` belongs to `(K*)^d`.
+
+For d=0 this means equality to one. Over F_q, the number of special-linear orbits inside the GL orbit is exactly **gcd(q-1,d)**. Equivalently, d is the gcd of same-orientation index differences and opposite-orientation sums e+f+1. Multiplicities affect the slice character but do not change this orbit count.
+
+Examples show why the mixed result is different from the single-type rule. R_1 plus R_2 has one SL orbit over every finite field. R_1 plus L_1 has three over F4. R_1 plus L_2 has four over F5. The zero pencil formed from positive numbers of R_0 and L_0 has full determinant image.
+
+The executable constructs a stabilizer witness for every accepted determinant triple, with any prescribed GL2 slice action of that determinant. It also corrects a supplied GL tensor map to a determinant-one map with exactly the same tensor image when the character permits it. It does not discover the supplied model or the initial map.
+
+## Evidence and replay
+
+```sh
+python3.12 -I -W error -B research/mixed-singular-kronecker-characters/verify.py
+python3.12 -I -O -W error -B research/mixed-singular-kronecker-characters/verify.py
+```
+
+Expected: `PASS_MIXED_SINGULAR_KRONECKER_CHARACTERS`. Python 3.12 and the standard library suffice. Three frozen source files are authenticated before import. Direct replay compares the complete [RESULT.json](RESULT.json) without changing publication files.
+
+The finite evidence includes:
+
+- All 256 ordered Hom cases with indices zero through three over F2/F3/F4/F5, solved independently from coefficient equations.
+- Twelve full mixed stabilizer domains, with 98,066 linear solutions and 41,744 invertible stabilizers. The oracle uses no character or symmetric-power formula. The report marks whether every GL2 action or one representative per determinant was enumerated.
+- 6,684 literal lifts over every GL2 action in nineteen supplied model/field pairs, plus 6,684 reconstructions with the same prescribed action.
+- All 468 determinant triples in those pairs: 330 constructed witnesses and 138 exclusions. All 330 accepted cases also give checked determinant-one corrections of non-diagonal supplied maps.
+- Eight mathematical controls, twelve malformed-domain rejections and 1,474 independent permutation determinant checks.
+
+The executable is bounded: indices 0..5, combined multiplicities 1..3, F2/F3/F4/F5, and both full factor dimensions at most sixteen. The arbitrary-field and arbitrary-dimension result is the written proof. Over an arbitrary field, constructive power-subgroup membership can require a supplied d-th root; no universal root-extraction algorithm is claimed.
+
+## Use and limits
+
+This closes the supplied purely singular character interface from Nick Petalas PR5250 and apoursh PR5672. It gives exact SL labels and admissible correction maps for tensor-atlas candidates. A multiplication-bound use still needs a named native producer and consumer, with paid maps, ownership, movement, restoration, storage, precision and a complete recursive invoice. Those costs remain unknown.
+
+Base is canonical main `df0137efd35e11b4445734bf612bdd4c7ebc330c`, priority7. Selected .00310045 is unchanged. Normal/optimized, committed-byte and export checks are separate from hosted CI, independent human acceptance and formal-kernel proof. Full-history ancestry preflight is unavailable in this shallow checkout.
+
+Ali Romman with substantial OpenAI Codex assistance. Credit apoursh PR5672 for the single-type theorem and retained field/symmetric-power implementation; Nick Petalas PR5250 for the explicit handoff; David Ganz's A030/A026/A029 atlas and the classical Kronecker/symmetric-power lineage. Original source notices remain under source/. New mixed proof, oracle, witnesses and checks are Apache-2.0.
+
+## Open next questions
+
+- Add regular factors to a supplied mixed pencil. Their shared slice stabilizer can restrict GL2, so the present lift cannot be applied without that new condition.
+- Extract the supplied singular block types and actual factor maps from an arbitrary tensor. This package does not perform Kronecker reduction.
+- Bind one resulting tensor interface to a physical native caller and its complete bill. Do not treat algebraic determinant maps as free operations.
diff --git a/research/mixed-singular-kronecker-characters/RESULT.json b/research/mixed-singular-kronecker-characters/RESULT.json
new file mode 100644
index 0000000000..82725dbf8f
--- /dev/null
+++ b/research/mixed-singular-kronecker-characters/RESULT.json
@@ -0,0 +1,1292 @@
+{
+  "constructive_witnesses": [
+    {
+      "accepted_triples": 1,
+      "character_exponents": [
+        2,
+        1,
+        2
+      ],
+      "excluded_triples": 0,
+      "field": 2,
+      "lifts": 12,
+      "model": [
+        [
+          "R",
+          1,
+          1
+        ],
+        [
+          "R",
+          2,
+          1
+        ]
+      ],
+      "power_index": 1,
+      "special_linear_corrections": 1
+    },
+    {
+      "accepted_triples": 8,
+      "character_exponents": [
+        2,
+        1,
+        2
+      ],
+      "excluded_triples": 0,
+      "field": 3,
+      "lifts": 96,
+      "model": [
+        [
+          "R",
+          1,
+          1
+        ],
+        [
+          "R",
+          2,
+          1
+        ]
+      ],
+      "power_index": 1,
+      "special_linear_corrections": 8
+    },
+    {
+      "accepted_triples": 9,
+      "character_exponents": [
+        2,
+        1,
+        3
+      ],
+      "excluded_triples": 18,
+      "field": 4,
+      "lifts": 360,
+      "model": [
+        [
+          "R",
+          1,
+          1
+        ],
+        [
+          "L",
+          1,
+          1
+        ]
+      ],
+      "power_index": 3,
+      "special_linear_corrections": 9
+    },
+    {
+      "accepted_triples": 4,
+      "character_exponents": [
+        1,
+        0,
+        -1
+      ],
+      "excluded_triples": 4,
+      "field": 3,
+      "lifts": 96,
+      "model": [
+        [
+          "R",
+          0,
+          1
+        ],
+        [
+          "R",
+          2,
+          1
+        ]
+      ],
+      "power_index": 2,
+      "special_linear_corrections": 4
+    },
+    {
+      "accepted_triples": 4,
+      "character_exponents": [
+        2,
+        3,
+        3
+      ],
+      "excluded_triples": 4,
+      "field": 3,
+      "lifts": 96,
+      "model": [
+        [
+          "L",
+          0,
+          1
+        ],
+        [
+          "L",
+          2,
+          1
+        ]
+      ],
+      "power_index": 2,
+      "special_linear_corrections": 4
+    },
+    {
+      "accepted_triples": 16,
+      "character_exponents": [
+        2,
+        1,
+        6
+      ],
+      "excluded_triples": 48,
+      "field": 5,
+      "lifts": 960,
+      "model": [
+        [
+          "R",
+          1,
+          1
+        ],
+        [
+          "L",
+          2,
+          1
+        ]
+      ],
+      "power_index": 4,
+      "special_linear_corrections": 16
+    },
+    {
+      "accepted_triples": 4,
+      "character_exponents": [
+        2,
+        1,
+        2
+      ],
+      "excluded_triples": 4,
+      "field": 3,
+      "lifts": 96,
+      "model": [
+        [
+          "R",
+          1,
+          2
+        ],
+        [
+          "L",
+          0,
+          1
+        ]
+      ],
+      "power_index": 2,
+      "special_linear_corrections": 4
+    },
+    {
+      "accepted_triples": 1,
+      "character_exponents": [
+        1,
+        0,
+        0
+      ],
+      "excluded_triples": 0,
+      "field": 2,
+      "lifts": 12,
+      "model": [
+        [
+          "R",
+          0,
+          2
+        ],
+        [
+          "L",
+          0,
+          2
+        ]
+      ],
+      "power_index": 1,
+      "special_linear_corrections": 1
+    },
+    {
+      "accepted_triples": 27,
+      "character_exponents": [
+        3,
+        2,
+        5
+      ],
+      "excluded_triples": 0,
+      "field": 4,
+      "lifts": 360,
+      "model": [
+        [
+          "R",
+          2,
+          1
+        ],
+        [
+          "R",
+          4,
+          1
+        ]
+      ],
+      "power_index": 2,
+      "special_linear_corrections": 27
+    },
+    {
+      "accepted_triples": 4,
+      "character_exponents": [
+        2,
+        1,
+        1
+      ],
+      "excluded_triples": 4,
+      "field": 3,
+      "lifts": 96,
+      "model": [
+        [
+          "R",
+          1,
+          1
+        ],
+        [
+          "R",
+          3,
+          1
+        ]
+      ],
+      "power_index": 2,
+      "special_linear_corrections": 4
+    },
+    {
+      "accepted_triples": 4,
+      "character_exponents": [
+        3,
+        4,
+        9
+      ],
+      "excluded_triples": 4,
+      "field": 3,
+      "lifts": 96,
+      "model": [
+        [
+          "L",
+          1,
+          1
+        ],
+        [
+          "L",
+          3,
+          1
+        ]
+      ],
+      "power_index": 2,
+      "special_linear_corrections": 4
+    },
+    {
+      "accepted_triples": 1,
+      "character_exponents": [
+        1,
+        0,
+        1
+      ],
+      "excluded_triples": 0,
+      "field": 2,
+      "lifts": 12,
+      "model": [
+        [
+          "R",
+          0,
+          1
+        ],
+        [
+          "R",
+          1,
+          1
+        ],
+        [
+          "L",
+          0,
+          1
+        ],
+        [
+          "L",
+          1,
+          1
+        ]
+      ],
+      "power_index": 1,
+      "special_linear_corrections": 1
+    },
+    {
+      "accepted_triples": 16,
+      "character_exponents": [
+        2,
+        1,
+        7
+      ],
+      "excluded_triples": 48,
+      "field": 5,
+      "lifts": 960,
+      "model": [
+        [
+          "R",
+          1,
+          2
+        ],
+        [
+          "L",
+          2,
+          1
+        ]
+      ],
+      "power_index": 4,
+      "special_linear_corrections": 16
+    },
+    {
+      "accepted_triples": 27,
+      "character_exponents": [
+        1,
+        0,
+        6
+      ],
+      "excluded_triples": 0,
+      "field": 4,
+      "lifts": 360,
+      "model": [
+        [
+          "R",
+          0,
+          1
+        ],
+        [
+          "L",
+          3,
+          1
+        ]
+      ],
+      "power_index": 4,
+      "special_linear_corrections": 27
+    },
+    {
+      "accepted_triples": 4,
+      "character_exponents": [
+        2,
+        3,
+        9
+      ],
+      "excluded_triples": 4,
+      "field": 3,
+      "lifts": 96,
+      "model": [
+        [
+          "L",
+          2,
+          3
+        ]
+      ],
+      "power_index": 0,
+      "special_linear_corrections": 4
+    },
+    {
+      "accepted_triples": 64,
+      "character_exponents": [
+        5,
+        4,
+        20
+      ],
+      "excluded_triples": 0,
+      "field": 5,
+      "lifts": 960,
+      "model": [
+        [
+          "R",
+          4,
+          1
+        ],
+        [
+          "R",
+          5,
+          1
+        ]
+      ],
+      "power_index": 1,
+      "special_linear_corrections": 64
+    },
+    {
+      "accepted_triples": 8,
+      "character_exponents": [
+        2,
+        1,
+        4
+      ],
+      "excluded_triples": 0,
+      "field": 3,
+      "lifts": 96,
+      "model": [
+        [
+          "R",
+          1,
+          2
+        ],
+        [
+          "R",
+          2,
+          2
+        ]
+      ],
+      "power_index": 1,
+      "special_linear_corrections": 8
+    },
+    {
+      "accepted_triples": 64,
+      "character_exponents": [
+        2,
+        1,
+        3
+      ],
+      "excluded_triples": 0,
+      "field": 5,
+      "lifts": 960,
+      "model": [
+        [
+          "R",
+          1,
+          1
+        ],
+        [
+          "L",
+          1,
+          1
+        ]
+      ],
+      "power_index": 3,
+      "special_linear_corrections": 64
+    },
+    {
+      "accepted_triples": 64,
+      "character_exponents": [
+        2,
+        1,
+        3
+      ],
+      "excluded_triples": 0,
+      "field": 5,
+      "lifts": 960,
+      "model": [
+        [
+          "R",
+          1,
+          1
+        ],
+        [
+          "R",
+          3,
+          1
+        ],
+        [
+          "L",
+          1,
+          1
+        ]
+      ],
+      "power_index": 1,
+      "special_linear_corrections": 64
+    }
+  ],
+  "controls": {
+    "malformed_rejections": [
+      "empty",
+      "unknown_side",
+      "negative_index",
+      "zero_multiplicity",
+      "zero_rows",
+      "zero_columns",
+      "too_large_index",
+      "noninteger_index",
+      "combined_multiplicity",
+      "zero_determinant",
+      "outside_field",
+      "wrong_arity"
+    ],
+    "mathematical_controls": [
+      "slice_shift",
+      "Q_transpose",
+      "slice_orientation",
+      "unequal_right_mixing",
+      "left_to_right_mixing",
+      "forbidden_reverse_mixing",
+      "multiplicity_index",
+      "cross_orientation_sum"
+    ],
+    "permutation_determinant_cases": 1474,
+    "wrong_slice_shift_triples": 16
+  },
+  "hom_domains": [
+    {
+      "field": 2,
+      "ordered_pairs": 64,
+      "total_Hom_dimension": 88
+    },
+    {
+      "field": 3,
+      "ordered_pairs": 64,
+      "total_Hom_dimension": 88
+    },
+    {
+      "field": 4,
+      "ordered_pairs": 64,
+      "total_Hom_dimension": 88
+    },
+    {
+      "field": 5,
+      "ordered_pairs": 64,
+      "total_Hom_dimension": 88
+    }
+  ],
+  "literal_oracles": [
+    {
+      "all_slice_actions": true,
+      "determinant_image": [
+        [
+          1,
+          1,
+          1
+        ]
+      ],
+      "dimensions": [
+        3,
+        5
+      ],
+      "endomorphism_dimension": 4,
+      "field": 2,
+      "linear_solutions_tested": 96,
+      "model": [
+        [
+          "R",
+          1,
+          1
+        ],
+        [
+          "R",
+          2,
+          1
+        ]
+      ],
+      "slice_actions": 6,
+      "special_linear_orbits": 1,
+      "stabilizers": 24
+    },
+    {
+      "all_slice_actions": true,
+      "determinant_image": [
+        [
+          1,
+          1,
+          1
+        ],
+        [
+          1,
+          1,
+          2
+        ],
+        [
+          1,
+          2,
+          1
+        ],
+        [
+          1,
+          2,
+          2
+        ],
+        [
+          2,
+          1,
+          1
+        ],
+        [
+          2,
+          1,
+          2
+        ],
+        [
+          2,
+          2,
+          1
+        ],
+        [
+          2,
+          2,
+          2
+        ]
+      ],
+      "dimensions": [
+        3,
+        5
+      ],
+      "endomorphism_dimension": 4,
+      "field": 3,
+      "linear_solutions_tested": 3888,
+      "model": [
+        [
+          "R",
+          1,
+          1
+        ],
+        [
+          "R",
+          2,
+          1
+        ]
+      ],
+      "slice_actions": 48,
+      "special_linear_orbits": 1,
+      "stabilizers": 1728
+    },
+    {
+      "all_slice_actions": true,
+      "determinant_image": [
+        [
+          1,
+          1,
+          1
+        ],
+        [
+          1,
+          1,
+          2
+        ],
+        [
+          1,
+          1,
+          3
+        ],
+        [
+          2,
+          2,
+          1
+        ],
+        [
+          2,
+          2,
+          2
+        ],
+        [
+          2,
+          2,
+          3
+        ],
+        [
+          3,
+          3,
+          1
+        ],
+        [
+          3,
+          3,
+          2
+        ],
+        [
+          3,
+          3,
+          3
+        ]
+      ],
+      "dimensions": [
+        3,
+        3
+      ],
+      "endomorphism_dimension": 4,
+      "field": 4,
+      "linear_solutions_tested": 46080,
+      "model": [
+        [
+          "R",
+          1,
+          1
+        ],
+        [
+          "L",
+          1,
+          1
+        ]
+      ],
+      "slice_actions": 180,
+      "special_linear_orbits": 3,
+      "stabilizers": 25920
+    },
+    {
+      "all_slice_actions": false,
+      "determinant_image": [
+        [
+          1,
+          1,
+          1
+        ],
+        [
+          1,
+          2,
+          1
+        ],
+        [
+          2,
+          1,
+          2
+        ],
+        [
+          2,
+          2,
+          2
+        ]
+      ],
+      "dimensions": [
+        2,
+        4
+      ],
+      "endomorphism_dimension": 5,
+      "field": 3,
+      "linear_solutions_tested": 486,
+      "model": [
+        [
+          "R",
+          0,
+          1
+        ],
+        [
+          "R",
+          2,
+          1
+        ]
+      ],
+      "slice_actions": 2,
+      "special_linear_orbits": 2,
+      "stabilizers": 216
+    },
+    {
+      "all_slice_actions": false,
+      "determinant_image": [
+        [
+          1,
+          1,
+          1
+        ],
+        [
+          1,
+          2,
+          2
+        ],
+        [
+          2,
+          1,
+          1
+        ],
+        [
+          2,
+          2,
+          2
+        ]
+      ],
+      "dimensions": [
+        4,
+        2
+      ],
+      "endomorphism_dimension": 5,
+      "field": 3,
+      "linear_solutions_tested": 486,
+      "model": [
+        [
+          "L",
+          0,
+          1
+        ],
+        [
+          "L",
+          2,
+          1
+        ]
+      ],
+      "slice_actions": 2,
+      "special_linear_orbits": 2,
+      "stabilizers": 216
+    },
+    {
+      "all_slice_actions": false,
+      "determinant_image": [
+        [
+          1,
+          1,
+          1
+        ],
+        [
+          1,
+          1,
+          4
+        ],
+        [
+          1,
+          4,
+          2
+        ],
+        [
+          1,
+          4,
+          3
+        ],
+        [
+          2,
+          1,
+          2
+        ],
+        [
+          2,
+          1,
+          3
+        ],
+        [
+          2,
+          4,
+          1
+        ],
+        [
+          2,
+          4,
+          4
+        ],
+        [
+          3,
+          1,
+          2
+        ],
+        [
+          3,
+          1,
+          3
+        ],
+        [
+          3,
+          4,
+          1
+        ],
+        [
+          3,
+          4,
+          4
+        ],
+        [
+          4,
+          1,
+          1
+        ],
+        [
+          4,
+          1,
+          4
+        ],
+        [
+          4,
+          4,
+          2
+        ],
+        [
+          4,
+          4,
+          3
+        ]
+      ],
+      "dimensions": [
+        4,
+        4
+      ],
+      "endomorphism_dimension": 5,
+      "field": 5,
+      "linear_solutions_tested": 12500,
+      "model": [
+        [
+          "R",
+          1,
+          1
+        ],
+        [
+          "L",
+          2,
+          1
+        ]
+      ],
+      "slice_actions": 4,
+      "special_linear_orbits": 4,
+      "stabilizers": 8000
+    },
+    {
+      "all_slice_actions": false,
+      "determinant_image": [
+        [
+          1,
+          1,
+          1
+        ],
+        [
+          1,
+          1,
+          2
+        ],
+        [
+          2,
+          1,
+          1
+        ],
+        [
+          2,
+          1,
+          2
+        ]
+      ],
+      "dimensions": [
+        3,
+        4
+      ],
+      "endomorphism_dimension": 7,
+      "field": 3,
+      "linear_solutions_tested": 4374,
+      "model": [
+        [
+          "R",
+          1,
+          2
+        ],
+        [
+          "L",
+          0,
+          1
+        ]
+      ],
+      "slice_actions": 2,
+      "special_linear_orbits": 2,
+      "stabilizers": 1728
+    },
+    {
+      "all_slice_actions": true,
+      "determinant_image": [
+        [
+          1,
+          1,
+          1
+        ]
+      ],
+      "dimensions": [
+        2,
+        2
+      ],
+      "endomorphism_dimension": 8,
+      "field": 2,
+      "linear_solutions_tested": 1536,
+      "model": [
+        [
+          "R",
+          0,
+          2
+        ],
+        [
+          "L",
+          0,
+          2
+        ]
+      ],
+      "slice_actions": 6,
+      "special_linear_orbits": 1,
+      "stabilizers": 216
+    },
+    {
+      "all_slice_actions": false,
+      "determinant_image": [
+        [
+          1,
+          1,
+          1
+        ],
+        [
+          1,
+          1,
+          2
+        ],
+        [
+          1,
+          1,
+          3
+        ],
+        [
+          1,
+          2,
+          1
+        ],
+        [
+          1,
+          2,
+          2
+        ],
+        [
+          1,
+          2,
+          3
+        ],
+        [
+          1,
+          3,
+          1
+        ],
+        [
+          1,
+          3,
+          2
+        ],
+        [
+          1,
+          3,
+          3
+        ],
+        [
+          2,
+          1,
+          1
+        ],
+        [
+          2,
+          1,
+          2
+        ],
+        [
+          2,
+          1,
+          3
+        ],
+        [
+          2,
+          2,
+          1
+        ],
+        [
+          2,
+          2,
+          2
+        ],
+        [
+          2,
+          2,
+          3
+        ],
+        [
+          2,
+          3,
+          1
+        ],
+        [
+          2,
+          3,
+          2
+        ],
+        [
+          2,
+          3,
+          3
+        ],
+        [
+          3,
+          1,
+          1
+        ],
+        [
+          3,
+          1,
+          2
+        ],
+        [
+          3,
+          1,
+          3
+        ],
+        [
+          3,
+          2,
+          1
+        ],
+        [
+          3,
+          2,
+          2
+        ],
+        [
+          3,
+          2,
+          3
+        ],
+        [
+          3,
+          3,
+          1
+        ],
+        [
+          3,
+          3,
+          2
+        ],
+        [
+          3,
+          3,
+          3
+        ]
+      ],
+      "dimensions": [
+        6,
+        8
+      ],
+      "endomorphism_dimension": 5,
+      "field": 4,
+      "linear_solutions_tested": 3072,
+      "model": [
+        [
+          "R",
+          2,
+          1
+        ],
+        [
+          "R",
+          4,
+          1
+        ]
+      ],
+      "slice_actions": 3,
+      "special_linear_orbits": 1,
+      "stabilizers": 1728
+    },
+    {
+      "all_slice_actions": false,
+      "determinant_image": [
+        [
+          1,
+          1,
+          1
+        ],
+        [
+          1,
+          2,
+          2
+        ],
+        [
+          2,
+          1,
+          1
+        ],
+        [
+          2,
+          2,
+          2
+        ]
+      ],
+      "dimensions": [
+        4,
+        6
+      ],
+      "endomorphism_dimension": 5,
+      "field": 3,
+      "linear_solutions_tested": 486,
+      "model": [
+        [
+          "R",
+          1,
+          1
+        ],
+        [
+          "R",
+          3,
+          1
+        ]
+      ],
+      "slice_actions": 2,
+      "special_linear_orbits": 2,
+      "stabilizers": 216
+    },
+    {
+      "all_slice_actions": false,
+      "determinant_image": [
+        [
+          1,
+          1,
+          1
+        ],
+        [
+          1,
+          2,
+          1
+        ],
+        [
+          2,
+          1,
+          2
+        ],
+        [
+          2,
+          2,
+          2
+        ]
+      ],
+      "dimensions": [
+        6,
+        4
+      ],
+      "endomorphism_dimension": 5,
+      "field": 3,
+      "linear_solutions_tested": 486,
+      "model": [
+        [
+          "L",
+          1,
+          1
+        ],
+        [
+          "L",
+          3,
+          1
+        ]
+      ],
+      "slice_actions": 2,
+      "special_linear_orbits": 2,
+      "stabilizers": 216
+    },
+    {
+      "all_slice_actions": true,
+      "determinant_image": [
+        [
+          1,
+          1,
+          1
+        ]
+      ],
+      "dimensions": [
+        4,
+        4
+      ],
+      "endomorphism_dimension": 12,
+      "field": 2,
+      "linear_solutions_tested": 24576,
+      "model": [
+        [
+          "R",
+          0,
+          1
+        ],
+        [
+          "R",
+          1,
+          1
+        ],
+        [
+          "L",
+          0,
+          1
+        ],
+        [
+          "L",
+          1,
+          1
+        ]
+      ],
+      "slice_actions": 6,
+      "special_linear_orbits": 1,
+      "stabilizers": 1536
+    }
+  ],
+  "scope": "All-field proof for supplied purely singular direct sums; bounded executable F2/F3/F4/F5 models. Regular factors, arbitrary extraction and physical pricing remain open.",
+  "status": "PASS_MIXED_SINGULAR_KRONECKER_CHARACTERS"
+}
diff --git a/research/mixed-singular-kronecker-characters/SOURCES.json b/research/mixed-singular-kronecker-characters/SOURCES.json
new file mode 100644
index 0000000000..8d30481694
--- /dev/null
+++ b/research/mixed-singular-kronecker-characters/SOURCES.json
@@ -0,0 +1,39 @@
+{
+  "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/kronecker-determinant-image/pencil.py",
+      "usage": "provenance",
+      "pin": "head:81c0577b83cdafa73346da8ade1261b0b202e45f:research/kronecker-determinant-image/pencil.py",
+      "git_blob": "6bc7fc076e6ce2418ec9ed05d85115deb3d4bdd2",
+      "sha256": "a714862853cc884e84eac34ba1d7ccb14a6326bcfadb630910034bb44bd305db"
+    },
+    {
+      "path": "research/kronecker-determinant-image/PROOF.md",
+      "usage": "provenance",
+      "pin": "head:81c0577b83cdafa73346da8ade1261b0b202e45f:research/kronecker-determinant-image/PROOF.md",
+      "git_blob": "77ff305e1c31bfec96e50585872a0a5fa420de20",
+      "sha256": "7cc6f1845e15ccc3c8867680cadb8366008143815001be7d790ddc811f63a89b"
+    },
+    {
+      "path": "research/kronecker-determinant-image/README.md",
+      "usage": "provenance",
+      "pin": "head:81c0577b83cdafa73346da8ade1261b0b202e45f:research/kronecker-determinant-image/README.md",
+      "git_blob": "eed3f5378d4a58e603e492ad2ef22b40f2703260",
+      "sha256": "7e15e74abb9fa45537b5b6986f016ab54981f085ad52d1e69e0e973bc63b9447"
+    }
+  ]
+}
diff --git a/research/mixed-singular-kronecker-characters/TASK.json b/research/mixed-singular-kronecker-characters/TASK.json
new file mode 100644
index 0000000000..df74ec7aec
--- /dev/null
+++ b/research/mixed-singular-kronecker-characters/TASK.json
@@ -0,0 +1,107 @@
+{
+  "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": "Classify all determinant images of supplied purely singular Kronecker sums, including unequal indices, left/right mixing, multiplicities and zero indices with positive total factor dimensions.",
+  "scope_change_reason": "PR5672 releases the mixed singular part of PR5250. This is a written all-field theorem and bounded exact evidence, not Lean formalization.",
+  "bottleneck_link": "This closes a named determinant-character gap for tensor-atlas alternatives and provides literal SL corrections. Physical supplier costs remain unknown, so no kappa gain is inferred.",
+  "budget_minutes": 120,
+  "stop_rule": "Stop after the complete supplied singular theorem, independent literal oracle and publication checks. Exclude regular blocks, arbitrary extraction and physical realization.",
+  "outcome": "completed",
+  "evidence": "PROOF.md and RESULT.json; 256 Hom cases, 98066 literal solutions, complete bounded GL2 witnesses and supplied-map corrections.",
+  "author": "Ali Romman with substantial OpenAI Codex assistance",
+  "ai_assistance": "Substantial OpenAI Codex assistance for proof, implementation, independent equation oracle and publication. No subagents.",
+  "open_questions": [
+    {
+      "question": "What is the character image after regular factors are added?",
+      "why_it_matters": "The shared slice stabilizer can be smaller than GL2.",
+      "first_step": "Pin a supplied regular type and prove which slice matrices preserve it before combining determinant images.",
+      "blocked_by": "Regular-factor slice stabilizer and its exact lifts."
+    },
+    {
+      "question": "Can arbitrary supplied tensors be reduced to this singular model with actual maps?",
+      "why_it_matters": "The present executable requires block types and a model.",
+      "first_step": "Use a source-bound Kronecker reduction and check every coefficient map.",
+      "blocked_by": "Constructive extraction and source conventions."
+    },
+    {
+      "question": "Which native producer and consumer can use these tensor maps?",
+      "why_it_matters": "Algebraic classification alone gives no multiplication saving.",
+      "first_step": "Name one physical interface and charge all maps, memory, restoration and precision.",
+      "blocked_by": "A complete physical caller and paid invoice."
+    }
+  ]
+}
diff --git a/research/mixed-singular-kronecker-characters/VERIFY.json b/research/mixed-singular-kronecker-characters/VERIFY.json
new file mode 100644
index 0000000000..a021dfb26b
--- /dev/null
+++ b/research/mixed-singular-kronecker-characters/VERIFY.json
@@ -0,0 +1,34 @@
+{
+  "schema_version": 1,
+  "status": "ready",
+  "python": "3.12",
+  "requirements": [],
+  "inputs": [],
+  "commands": [
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 570,
+      "checks": "Authenticated source lifts, complete mixed Hom equations and all declared literal stabilizer spaces, every bounded GL2 lift, determinant characters, SL corrections and rejection controls"
+    },
+    {
+      "argv": [
+        "{python}",
+        "-I",
+        "-O",
+        "-W",
+        "error",
+        "-B",
+        "{package}/verify.py"
+      ],
+      "timeout_seconds": 570,
+      "checks": "Authenticated source lifts, complete mixed Hom equations and all declared literal stabilizer spaces, every bounded GL2 lift, determinant characters, SL corrections and rejection controls"
+    }
+  ]
+}
diff --git a/research/mixed-singular-kronecker-characters/mixed.py b/research/mixed-singular-kronecker-characters/mixed.py
new file mode 100644
index 0000000000..9f14f93e1f
--- /dev/null
+++ b/research/mixed-singular-kronecker-characters/mixed.py
@@ -0,0 +1,187 @@
+"""Determinant witnesses for bounded supplied mixed singular pencil models.
+
+The proof covers all fields and indices. This executable uses the retained
+F2/F3/F4/F5 arithmetic and positive-index lifts in its stated bounded domain.
+Ali Romman with substantial OpenAI Codex assistance. Apache-2.0.
+"""
+from hashlib import sha256
+from pathlib import Path
+from math import gcd
+import importlib.util
+import json
+
+ROOT=Path(__file__).resolve().parent
+for item in json.loads((ROOT/'INPUTS.json').read_text()):
+    if sha256((ROOT/item['local']).read_bytes()).hexdigest()!=item['sha256']:
+        raise ValueError('Frozen input '+item['local'])
+spec=importlib.util.spec_from_file_location('credited_kronecker',ROOT/'source/pencil.py')
+old=importlib.util.module_from_spec(spec);spec.loader.exec_module(old)
+Field=old.Field
+need=old.require
+
+
+def types(model):
+    need(isinstance(model,(list,tuple)) and model,'nonempty supplied block model')
+    grouped={}
+    for item in model:
+        need(isinstance(item,(list,tuple)) and len(item)==3,'block has orientation, index and multiplicity')
+        side,e,r=item
+        need(side in ('R','L') and type(e)is int and 0<=e<=5 and type(r)is int and 1<=r<=3,'bounded block domain')
+        grouped[side,e]=grouped.get((side,e),0)+r
+    need(all(r<=3 for r in grouped.values()),'bounded combined multiplicity')
+    out=[(s,e,r) for (s,e),r in grouped.items()]
+    out.sort(key=lambda x:(x[0]=='L',x[1] if x[0]=='R'else-x[1]))
+    m=sum((e+(s=='L'))*r for s,e,r in out);n=sum((e+(s=='R'))*r for s,e,r in out)
+    need(0<m<=16 and 0<n<=16,'both total dimensions must be positive and at most16')
+    return out
+
+
+def layout(model):
+    out=[];m=n=0
+    for side,e,r in types(model):
+        a=(e+(side=='L'))*r;b=(e+(side=='R'))*r
+        out.append(dict(side=side,e=e,r=r,row=m,col=n,m=a,n=b));m+=a;n+=b
+    return out,m,n
+
+
+def slices(model):
+    parts,m,n=layout(model);a=[[0]*n for _ in range(m)];b=[[0]*n for _ in range(m)]
+    for c in parts:
+        r,e=c['r'],c['e']
+        for i in range(e):
+            for j in range(r):
+                x,y=c['row']+i*r+j,c['col']+i*r+j;a[x][y]=1
+                if c['side']=='R':b[x][y+r]=1
+                else:b[x+r][y]=1
+    return a,b
+
+
+def character_data(model):
+    parts=types(model);side,e,_=parts[0]
+    ell=(e+1,e) if side=='R' else(e,e+1)
+    vectors=[(j,-j-1) if s=='R' else(-j-1,j)for s,j,r in parts]
+    a=sum(r*j*(j-1)//2 if s=='R'else-r*j*(j+1)//2 for s,j,r in parts)
+    b=sum(-r*j*(j+1)//2 if s=='R'else r*j*(j-1)//2 for s,j,r in parts)
+    values=[ell[0]*u+ell[1]*v for u,v in vectors];d=0
+    for value in values:d=gcd(d,value)
+    return dict(types=parts,vectors=vectors,ell=ell,slice_shift=(a,b),character_slice_exponent=-ell[0]*a-ell[1]*b,relation_values=values,power_index=d)
+
+
+def character(model,triple,field):
+    need(isinstance(triple,(tuple,list)) and len(triple)==3 and all(type(x)is int and 0<x<field.q for x in triple),'three nonzero field determinants')
+    data=character_data(model);x,y,z=triple;l,h=data['ell']
+    return field.mul(field.mul(field.power(x,l),field.power(y,h)),field.power(z,data['character_slice_exponent']))
+
+
+def accepts(model,triple,field):
+    c=character(model,triple,field);d=character_data(model)['power_index']
+    return any(field.power(u,d)==c for u in range(1,field.q))
+
+
+def extended(a,b):
+    x0,x1,y0,y1=1,0,0,1
+    while b:
+        q,a,b=a//b,b,a%b;x0,x1=x1,x0-q*x1;y0,y1=y1,y0-q*y1
+    return (a,x0,y0) if a>=0 else(-a,-x0,-y0)
+
+
+def bezout(values):
+    d=0;coeff=[]
+    for value in values:
+        d,a,b=extended(d,value);coeff=[a*x for x in coeff]+[b]
+    need(sum(a*b for a,b in zip(coeff,values))==d,'Exact integral Bezout witness')
+    return d,coeff
+
+
+def block_diagonal(blocks):
+    size=sum(len(a)for a in blocks);out=[[0]*size for _ in range(size)];offset=0
+    for block in blocks:
+        for i,row in enumerate(block):out[offset+i][offset:offset+len(block)]=row
+        offset+=len(block)
+    return out
+
+
+def lift(model,action,scalars,field):
+    parts=types(model);need(len(scalars)==len(parts),'one determinant per distinct type')
+    need(len(action)==2 and all(len(row)==2 for row in action) and all(type(x)is int and 0<=x<field.q for row in action for x in row) and old.determinant(action,field)!=0,'invertible supplied slice action')
+    ps=[];qs=[]
+    for (side,e,r),u in zip(parts,scalars):
+        need(type(u)is int and 0<u<field.q,'nonzero multiplicity determinant')
+        d=old.identity(r);d[0][0]=u
+        if e:p,q,_=old.lift(e,r,action,d,field)
+        else:p,q=[],old.transpose(old.inverse(d,field))
+        if side=='L':p,q=q,p
+        ps.append(p);qs.append(q)
+    return block_diagonal(ps),block_diagonal(qs),action
+
+
+def witness(model,triple,field,action=None):
+    need(accepts(model,triple,field),'mixed character excludes triple')
+    data=character_data(model);chi=character(model,triple,field);d,coeff=bezout(data['relation_values'])
+    need(d==data['power_index'],'Same character lattice index')
+    root=next(u for u in range(1,field.q)if field.power(u,d)==chi)
+    scalars=[field.power(root,c)for c in coeff]
+    x,y,z=triple;a,b=data['slice_shift'];x=field.mul(x,field.power(z,-a));y=field.mul(y,field.power(z,-b))
+    for u,(c,h)in zip(scalars,data['vectors']):x=field.mul(x,field.power(u,-c));y=field.mul(y,field.power(u,-h))
+    correction=field.inv(field.mul(x,y));scalars[0]=field.mul(scalars[0],correction)
+    if action is None:action=[[z,0],[0,1]]
+    result=lift(model,action,scalars,field);a0,a1=slices(model)
+    need(old.determinant(action,field)==z,'Prescribed slice determinant')
+    need(old.fixes(a0,a1,result,field),'Literal mixed stabilizer witness')
+    need(tuple(old.determinant(a,field)for a in result)==tuple(triple),'All requested determinants')
+    return result
+
+
+def hom_single(src,dst):
+    """Return all coefficient-basis pairs U,C with U L_src=L_dst C."""
+    s,e=src;t,f=dst
+    ms,ns=e+(s=='L'),e+(s=='R');md,nd=f+(t=='L'),f+(t=='R')
+    if s==t=='L':
+        return [(old.transpose(c),old.transpose(u))for u,c in hom_single(('R',f),('R',e))]
+    if s=='R' and t=='L':return []
+    count=max(e-f+1,0) if s==t=='R' else e+f
+    result=[]
+    for k in range(count):
+        if s==t=='R':
+            u=[[int(j-i==k)for j in range(ms)]for i in range(md)]
+            c=[[int(j-i==k)for j in range(ns)]for i in range(nd)]
+        else:
+            u=[[int(i+j==k)for j in range(ms)]for i in range(md)]
+            c=[[int(i+j==k)for j in range(ns)]for i in range(nd)]
+        result.append((u,c))
+    return result
+
+
+def fixed_slice_basis(model):
+    parts,m,n=layout(model);out=[]
+    for src in parts:
+        for dst in parts:
+            for u,c in hom_single((src['side'],src['e']),(dst['side'],dst['e'])):
+                for i in range(dst['r']):
+                    for j in range(src['r']):
+                        p=[[0]*m for _ in range(m)];v=[[0]*n for _ in range(n)]
+                        for a,row in enumerate(u):
+                            for b,value in enumerate(row):p[dst['row']+a*dst['r']+i][src['row']+b*src['r']+j]=value
+                        for a,row in enumerate(c):
+                            for b,value in enumerate(row):v[dst['col']+a*dst['r']+i][src['col']+b*src['r']+j]=value
+                        out.append([x for row in p+v for x in row])
+    return out
+
+
+def tensor_image(model,maps,field):
+    first,second=slices(model);p,q,r=maps
+    return [old.multiply(old.multiply(p,old.mix(first,second,*row,field),field),old.transpose(q),field)for row in r]
+
+
+def correct_given_map(model,maps,field):
+    """Preserve a supplied GL map's tensor image while making every determinant one."""
+    _,m,n=layout(model);need(isinstance(maps,(tuple,list))and len(maps)==3,'three supplied factor maps')
+    for matrix,size in zip(maps,(m,n,2)):
+        need(isinstance(matrix,(tuple,list))and len(matrix)==size and all(isinstance(row,(tuple,list))and len(row)==size for row in matrix),'supplied map dimensions')
+        need(all(type(x)is int and 0<=x<field.q for row in matrix for x in row),'supplied map field entries')
+    triple=tuple(old.determinant(a,field)for a in maps);need(all(triple),'supplied maps are invertible')
+    stabilizer=witness(model,triple,field)
+    result=tuple(old.multiply(g,old.inverse(h,field),field)for g,h in zip(maps,stabilizer))
+    need(all(old.determinant(a,field)==1 for a in result),'All corrected map determinants')
+    need(tensor_image(model,result,field)==tensor_image(model,maps,field),'Same supplied tensor image')
+    return result
diff --git a/research/mixed-singular-kronecker-characters/oracle.py b/research/mixed-singular-kronecker-characters/oracle.py
new file mode 100644
index 0000000000..6535d1363e
--- /dev/null
+++ b/research/mixed-singular-kronecker-characters/oracle.py
@@ -0,0 +1,71 @@
+"""Literal linear-equation oracle for mixed pencil stabilizers.
+
+No character formula, Hom recurrence or symmetric-power lift is used here.
+The supplied field operations are shared exact arithmetic.
+Ali Romman with substantial OpenAI Codex assistance. Apache-2.0.
+"""
+from itertools import product
+
+
+def nullspace(rows,columns,field):
+    a=[row[:]for row in rows];pivots=[];at=0
+    for col in range(columns):
+        pivot=next((i for i in range(at,len(a))if a[i][col]),None)
+        if pivot is None:continue
+        a[at],a[pivot]=a[pivot],a[at];scale=field.inv(a[at][col]);a[at]=[field.mul(scale,x)for x in a[at]]
+        for i in range(len(a)):
+            if i!=at and a[i][col]:
+                scale=a[i][col];a[i]=[field.sub(x,field.mul(scale,y))for x,y in zip(a[i],a[at])]
+        pivots.append(col);at+=1
+    out=[]
+    for free in sorted(set(range(columns))-set(pivots)):
+        v=[0]*columns;v[free]=1
+        for i,p in enumerate(pivots):v[p]=field.neg(a[i][free])
+        out.append(v)
+    return out
+
+
+def equations(source,target,src_dims,dst_dims,field):
+    ms,ns=src_dims;md,nd=dst_dims;columns=md*ms+nd*ns;rows=[]
+    for a,b in zip(source,target):
+        for i in range(md):
+            for j in range(ns):
+                row=[0]*columns
+                for k in range(ms):row[i*ms+k]=a[k][j]
+                for k in range(nd):row[md*ms+k*ns+j]=field.neg(b[i][k])
+                rows.append(row)
+    return rows,columns
+
+
+def stabilizer_space(first,second,action,field):
+    m,n=len(first),len(first[0]);mixed=[]
+    for x,y in action:mixed.append([[field.add(field.mul(x,a),field.mul(y,b))for a,b in zip(row,other)]for row,other in zip(first,second)])
+    rows,columns=equations(mixed,(first,second),(m,n),(m,n),field)
+    return nullspace(rows,columns,field)
+
+
+def determinant(a,field):
+    """Row elimination for complete literal matrix domains."""
+    rows=[row[:]for row in a];out=1
+    for k in range(len(rows)):
+        pivot=next((i for i in range(k,len(rows))if rows[i][k]),None)
+        if pivot is None:return 0
+        if pivot!=k:rows[k],rows[pivot]=rows[pivot],rows[k];out=field.neg(out)
+        diagonal=rows[k][k];out=field.mul(out,diagonal);inv=field.inv(diagonal)
+        for i in range(k+1,len(rows)):
+            factor=field.mul(rows[i][k],inv)
+            for j in range(k,len(rows)):rows[i][j]=field.sub(rows[i][j],field.mul(factor,rows[k][j]))
+    return out
+
+
+def enumerate_space(basis,m,n,field,limit=60000):
+    if field.q**len(basis)>limit:raise ValueError('explicit oracle domain exceeds enumeration limit')
+    columns=m*m+n*n;image=set();invertible=0
+    for coefficients in product(range(field.q),repeat=len(basis)):
+        v=[0]*columns
+        for a,row in zip(coefficients,basis):
+            if a:v=[field.add(x,field.mul(a,y))for x,y in zip(v,row)]
+        p=[v[i*m:(i+1)*m]for i in range(m)];offset=m*m;c=[v[offset+i*n:offset+(i+1)*n]for i in range(n)]
+        x,z=determinant(p,field),determinant(c,field)
+        if x and z:image.add((x,field.inv(z)));invertible+=1
+    return image,invertible
diff --git a/research/mixed-singular-kronecker-characters/source/PROOF.md b/research/mixed-singular-kronecker-characters/source/PROOF.md
new file mode 100644
index 0000000000..77ff305e1c
--- /dev/null
+++ b/research/mixed-singular-kronecker-characters/source/PROOF.md
@@ -0,0 +1,335 @@
+# Determinant image of an isotypic singular Kronecker pencil
+
+This note gives a self-contained proof for one positive right minimal index
+with arbitrary positive multiplicity, and obtains the left-block case by
+transposition. It addresses the corresponding open question in Nick Petalas's
+[pencil-determinant-image package at its pinned head](https://github.com/CrocSwap/integer-mult-bounds/blob/43142bedc7cb5c0f1f73ff3fea6d9bfd237949ee/research/pencil-determinant-image/README.md).
+The block and symmetric-power constructions are classical; no literature
+novelty is claimed. The addition here is the explicit determinant-image formula,
+its action conventions, and its bounded verification package. This is a scoped
+proof, not a new multiplication bound or a classification of arbitrary pencils.
+
+## 1. Pencil and action conventions
+
+Let K be any field, and let e,r be positive integers. Define
+
+```
+A_0 = [I_e | 0],       A_1 = [0 | I_e],
+L_e(s,t) = s A_0 + t A_1.
+```
+
+Thus L_e is e by e+1, with s on its main diagonal and t immediately above
+that diagonal. Set
+
+```
+T_0 = A_0 tensor I_r,   T_1 = A_1 tensor I_r,
+T(s,t) = L_e(s,t) tensor I_r.
+```
+
+The row dimension is er and the column dimension is (e+1)r. The tensor-product
+ordering groups each monomial index into an r-dimensional block. A simultaneous
+permutation of rows and columns identifies this pencil with the direct sum of
+r identical L_e blocks.
+
+For P in GL_(er)(K), Q in GL_((e+1)r)(K), and
+
+```
+R = [[a,b], [c,d]] in GL_2(K),
+```
+
+use exactly the action
+
+```
+(T_0,T_1) -> (P(a T_0 + b T_1)Q^T, P(c T_0 + d T_1)Q^T).
+```
+
+In particular the right factor in the action is Q^T, not Q^(-1). If
+z=(s,t)^T, the mixed pencil is T(R^T z), because
+
+```
+s(a T_0+b T_1) + t(c T_0+d T_1)
+    = (as+ct)T_0 + (bs+dt)T_1.
+```
+
+Let Stab(T) be the stabilizer under this action, and let
+
+```
+Delta(T) = { (det P, det Q, det R) : (P,Q,R) in Stab(T) }.
+```
+
+All equalities of pencils below are polynomial equalities in independent
+indeterminates s,t. No interpolation over the points of K is used.
+
+## 2. The exact image
+
+**Theorem.** For every field K and all e,r >= 1,
+
+```
+Delta(L_e tensor I_r)
+ = { (u^e z^[r e(e-1)/2],
+      u^[-(e+1)] z^[-r e(e+1)/2],
+      z) : u,z in K^* }
+ = { (x,y,z) in (K^*)^3 :
+       x^(e+1) y^e z^[r e(e+1)/2] = 1 }.
+```
+
+The half-products in these exponents are integers. They do not denote division
+inside K, so the statement includes characteristic two.
+
+For the transposed block the result is
+
+```
+Delta(L_e^T tensor I_r)
+ = { (x,y,z) in (K^*)^3 :
+       x^e y^(e+1) z^[r e(e+1)/2] = 1 }.
+```
+
+The proof also constructs a stabilizer element for every triple in the stated
+image, with any prescribed R having determinant z.
+
+## 3. A characteristic-safe lift of every slice transformation
+
+For k >= 0 let V_k be the homogeneous degree-k polynomials in X,Y, with ordered
+basis
+
+```
+X^k, X^(k-1)Y, ..., Y^k.
+```
+
+Let S_k(R) be the matrix of polynomial substitution
+
+```
+f(X,Y) -> f(aX+bY,cX+dY)
+```
+
+on coefficient columns in this basis. Equivalently, column i, with
+0 <= i <= k, consists of the coefficients of
+
+```
+(aX+bY)^(k-i) (cX+dY)^i.
+```
+
+In particular S_0(R)=[1] and S_1(R)=R^T. This convention matters for the
+transposes in the lift. Substitution by R^(-1) is inverse to substitution by R,
+so S_k(R) is invertible in every characteristic.
+
+Use ordinary monomials and binomial coefficients reduced in K. There are no
+normalized monomials, divided factorials, or assumptions that k! is invertible.
+The substitution identities remain valid when some binomial coefficients
+vanish in K.
+
+The determinant is
+
+```
+det S_k(R) = (det R)^[k(k+1)/2].                    (1)
+```
+
+For completeness, this follows on generators of GL_2(K). For a diagonal
+R=diag(alpha,beta), S_k is diagonal with entries alpha^(k-i) beta^i,
+whose product is (alpha beta)^[k(k+1)/2]. Upper and lower unitriangular
+matrices act triangularly with all diagonal entries one. For the matrix
+interchanging X,Y, S_k reverses k+1 basis vectors, with determinant
+(-1)^[k(k+1)/2]. These matrices generate GL_2(K) by row elimination.
+With the stated coefficient-column convention, composition satisfies
+S_k(R)S_k(U)=S_k(UR). Determinants are multiplicative in either order,
+proving (1) for all R. This proof also works in characteristic two.
+
+Let B_e(s,t)=L_e(s,t)^T. It is the coefficient matrix of multiplication by
+sX+tY from V_(e-1) to V_e. Substituting the two linear forms into this product
+gives
+
+```
+S_e(R) B_e(s,t) = B_e(as+ct,bs+dt) S_(e-1)(R).
+```
+
+Transposing and rearranging proves
+
+```
+L_e(as+ct,bs+dt)
+    = S_(e-1)(R)^(-T) L_e(s,t) S_e(R)^T.           (2)
+```
+
+Consequently a stabilizer lift of every R is
+
+```
+P_R = S_(e-1)(R)^T tensor I_r,
+Q_R = S_e(R)^(-1) tensor I_r.                      (3)
+```
+
+Indeed (2) says P_R T(R^T z) Q_R^T = T(z). There is no residual sign and
+no restriction on R beyond invertibility.
+
+## 4. The complete fixed-slice stabilizer
+
+Suppose R=I_2 and (P,Q,I_2) fixes T. Put C=Q^(-T). The two equations are
+
+```
+P T_0 = T_0 C,       P T_1 = T_1 C.               (4)
+```
+
+Write P as an e by e block matrix and C as an e+1 by e+1 block matrix,
+with every block of size r by r. Use indices starting at zero. The first
+equation of (4) says that the first e block rows of C equal [P | 0]. The
+second says that the last e block rows of C equal [0 | P]. In their overlap,
+for 1 <= i <= e-1, one obtains
+
+```
+P_(i,0) = 0,
+P_(i,j) = P_(i-1,j-1)       for 1 <= j <= e-1,
+P_(i-1,e-1) = 0.                                  (5)
+```
+
+The recurrence makes each block diagonal constant. The first boundary
+condition kills every diagonal below the main diagonal; the last kills every
+diagonal above it. Thus
+
+```
+P = I_e tensor D,       C = I_(e+1) tensor D
+```
+
+for one r by r matrix D. When e=1 there is no overlapping block row,
+but the two equations directly give C=diag(P,P), which is the same conclusion.
+Invertibility of P forces D to be invertible. Conversely every invertible D
+satisfies (4). Therefore the fixed-slice stabilizer is exactly
+
+```
+(P,Q) = (I_e tensor D, I_(e+1) tensor D^(-T)),
+       D in GL_r(K).                              (6)
+```
+
+In particular arbitrary mixing between the r equal blocks is already included;
+it contributes one full GL_r(K), not just r independent scalar factors.
+
+## 5. All stabilizers and their determinants
+
+Fix R. Both a given stabilizer (P,Q,R) and the lift (P_R,Q_R,R) send
+T(R^T z) to T(z). Their quotient on the row and column factors therefore
+fixes the unmixed pencil T(z). Equation (6) applies. Since the factors acting
+on the monomial index commute with those acting on the multiplicity index,
+every stabilizer with slice factor R is uniquely of the form
+
+```
+P = S_(e-1)(R)^T tensor D,
+Q = S_e(R)^(-1) tensor D^(-T),       D in GL_r(K).  (7)
+```
+
+More explicitly, putting H=P P_R^(-1) and J=Q Q_R^(-1) gives
+H T(z) J^T=T(z), so (6) gives H=I_e tensor D and
+J=I_(e+1) tensor D^(-T). This proves necessity as well as sufficiency of (7).
+
+Let u=det D and z=det R. Applying (1) and
+det(A tensor B)=(det A)^(dim B)(det B)^(dim A) to (7) gives
+
+```
+det P = u^e z^[r e(e-1)/2],
+det Q = u^[-(e+1)] z^[-r e(e+1)/2].               (8)
+```
+
+The determinant maps GL_r(K)->K^* and GL_2(K)->K^* are surjective,
+as witnessed by diagonal matrices. Hence every u,z in K^* occurs, proving
+the parametrized form of the theorem. Eliminating u from (8) gives
+
+```
+(det P)^(e+1) (det Q)^e (det R)^[r e(e+1)/2] = 1.
+```
+
+## 6. Constructive converse without root extraction
+
+Suppose x,y,z are nonzero and satisfy
+
+```
+x^(e+1) y^e z^[r e(e+1)/2] = 1.                  (9)
+```
+
+Define
+
+```
+u = (xy)^(-1) z^(-re).                            (10)
+```
+
+There is no need to take an e-th root or an (e+1)-st root. To check (10),
+put A=r e(e-1)/2 and B=r e(e+1)/2. Then A+B=re^2 and
+2B=re(e+1). Equation (9) gives
+
+```
+u^e z^A
+  = x^(-e) y^(-e) z^(-re^2+A)
+  = x z^(B-re^2+A) = x,
+
+u^[-(e+1)] z^(-B)
+  = x^(e+1) y^(e+1) z^[re(e+1)-B]
+  = y z^[re(e+1)-2B] = y.
+```
+
+Take D=diag(u,1,...,1), and take any R with determinant z, for example
+diag(z,1). Equations (7) then give an explicit stabilizer with determinant
+triple (x,y,z). This proves that (9) is the only constraint, over any field.
+Conversely (8) implies xy=u^(-1)z^(-re), so (10) also proves uniqueness
+of u for a given image triple.
+
+## 7. Transposition and the finite-field orbit count
+
+Transposing the two slice equations exchanges P and Q and leaves R unchanged.
+Thus (P,Q,R) stabilizes (T_0,T_1) if and only if (Q,P,R) stabilizes
+(T_0^T,T_1^T). The determinant image for the left block is exactly the right
+block's image with its first two coordinates exchanged. This proves the
+transposed formula in Section 2.
+
+For K=F_q, the parametrization (8) is injective in (u,z), by (10), so
+
+```
+|Delta(T)| = (q-1)^2.
+```
+
+Let G=GL_(er)(F_q) x GL_((e+1)r)(F_q) x GL_2(F_q) and let N be the
+product of its three special linear subgroups. The determinant map identifies
+G/N with (F_q^*)^3. Because N is normal, the N-orbits within the single
+G-orbit of T are indexed by
+
+```
+(F_q^*)^3 / Delta(T).
+```
+
+The character
+
+```
+chi(x,y,z) = x^(e+1) y^e z^[r e(e+1)/2]
+```
+
+has kernel Delta(T) and is surjective: chi(w,w^(-1),1)=w.
+Consequently there are exactly q-1 such special-linear orbits. For the left
+block exchange x and y in this character. This is an orbit statement about
+the displayed isotypic pencil only.
+
+## 8. Boundaries of the result and checks that can falsify mistakes
+
+The theorem covers e>=1 and r>=1 only. The degree-zero right and left blocks
+have shapes 0 by 1 and 1 by 0, respectively. They represent unused columns
+or rows and require separate treatment of zero-dimensional factors; the lift
+above would also call for the undefined V_(-1). Adjoining such blocks to a
+positive-index pencil introduces extra fixed-slice maps that are outside the
+recurrence proved here. This exclusion is a scope boundary, not a claim that
+the displayed equation has been disproved under some extension of conventions.
+
+Different positive minimal indices, mixtures of right and left blocks, and
+regular/singular coupling are also outside this theorem. Their off-diagonal
+homomorphisms have not been classified here. No result is claimed for the
+separate regular-pencil question with no invertible rational slice.
+
+Useful discriminating finite checks include:
+
+- For e=1,r=1, the lift reads P=[u] and Q=u^(-1)R^(-T). The equation is
+  x^2 y z=1, which checks the sign and the inverse transpose on the right.
+- For e=2,r=1 over F_3, the image equation is x=z with y unrestricted.
+  Dropping the slice determinant exponent would instead require x=1.
+- For e=1,r=2 over F_3, the equation is y=1 with x,z unrestricted,
+  whereas e=1,r=1 gives y=z. This detects an omitted multiplicity factor.
+- In characteristic two, e at least two exercises vanishing binomial
+  coefficients in S_e. F_4 provides nontrivial determinant characters;
+  testing only F_2 cannot distinguish determinant exponents.
+- Directly solve the stabilizer slice equations in small dimensions instead
+  of checking only matrices generated by (7). Such a check can falsify the
+  completeness assertion in Sections 4 and 5.
+
+Finite checks support the implementation and expose convention errors. They
+do not replace the arbitrary-field proof above or settle any excluded case.
diff --git a/research/mixed-singular-kronecker-characters/source/README.md b/research/mixed-singular-kronecker-characters/source/README.md
new file mode 100644
index 0000000000..eed3f5378d
--- /dev/null
+++ b/research/mixed-singular-kronecker-characters/source/README.md
@@ -0,0 +1,140 @@
+# Determinant images for repeated singular Kronecker blocks
+
+**Scoped written proof with exact finite corroboration; no new kappa.**
+This answers the single-minimal-index/multiplicity next question in Nick
+Petalas's [PR #5250](https://github.com/CrocSwap/integer-mult-bounds/pull/5250).
+It complements that package's regular square pencils with an invertible slice.
+It does not classify mixed pencils or recover a decomposition from arbitrary
+input tensors.
+
+For any field K and positive integers e,r, let L_e(s,t) be the e by e+1 pencil
+with s on the diagonal and t on the superdiagonal, repeated as L_e tensor I_r.
+Use the action `(P,Q,R)` on slices `(A,B)` given by
+
+```
+(P(aA+bB)Q^T, P(cA+dB)Q^T),  R=[[a,b],[c,d]].
+```
+
+The exact stabilizer determinant image is
+
+```
+Delta = {(x,y,z) in (K*)^3 : x^(e+1) y^e z^[r e(e+1)/2] = 1}.
+```
+
+For the transposed pencil exchange x and y. [PROOF.md](PROOF.md) proves
+necessity and sufficiency, explicitly lifts every GL2 slice action in every
+characteristic, and constructs a witness for every allowed triple without root
+extraction. The half-product is an integer exponent, including characteristic
+two. Over F_q the image has size (q-1)^2 and the GL orbit splits into exactly
+q-1 orbits under the product of the three special linear groups.
+
+## Why this scope and what it adds
+
+PR #5250, exact head `43142bedc7cb5c0f1f73ff3fea6d9bfd237949ee`, explicitly
+leaves singular blocks and their multiplicity spaces open. Its README at this
+package's base has the identical Git blob. The new step is the complete
+one-type determinant image, its explicit slice-action lifts and constructive
+converse. Classical Kronecker blocks and symmetric powers are not claimed as
+new mathematics; global literature priority is unclaimed.
+
+This takes that concrete handoff before a random assignment. The original
+`formal-interface-lemma` card is retained verbatim in [TASK.json](TASK.json)
+with **changed scope**: a written mathematical side result, not a Lean
+formalization or a selected-supplier implication. Canonical main was pulled at
+`df0137efd35e11b4445734bf612bdd4c7ebc330c`, priority revision 7; selected kappa
+remains 0.00310045. The schema-aware source-binding baseline passed; its
+metadata check is not a cold scientific replay. Coordination and the five-point
+family comparison are in TASK.json and [Discussion #5670](https://github.com/CrocSwap/integer-mult-bounds/discussions/5670).
+
+## Reproducible evidence
+
+Use CPython 3.12 and its standard library from the repository root:
+
+```sh
+python3.12 -B scripts/research_package.py --package research/kronecker-determinant-image
+python3.12 -B scripts/check_research_commit.py --package research/kronecker-determinant-image --check-source-history
+```
+
+The registered commands run both ordinary and optimized Python with warnings
+as errors. Direct replay also works without Git or repository files:
+
+```sh
+python3.12 -I -W error -B research/kronecker-determinant-image/verify.py
+python3.12 -I -O -W error -B research/kronecker-determinant-image/verify.py
+```
+
+The success marker is `PASS_KRONECKER_DETERMINANT_IMAGE`. The preceding `RESULT`
+JSON gives all tested domains, determinant images and counts; `PACKAGE_SHA256`
+binds the local package files. The program writes no files. Each registered
+command has a 120-second limit. [SOURCES.json](SOURCES.json) pins historical
+provenance only: no predecessor executable or external scientific input is
+imported, and no live input is omitted from VERIFY.json.
+
+- **Completeness discriminator:** [oracle.py](oracle.py) independently enumerates
+  every P and R and solves both literal equations for the unique Q transpose.
+  Eight fixed (e,r,q) domains are (1,1,2/3/5), (2,1,2/3), (1,2,2/3) and
+  (3,1,2): 7,710 candidate pairs and 4,470 stabilizers. Its determinant images
+  agree exactly with the character kernel. It uses no symmetric powers or
+  predicted-image formula.
+- **Constructive checks:** [pencil.py](pencil.py) uses polynomial convolution,
+  without factorial division, over F2, F3, F4 and F5. Thirteen explicit domains
+  in `verify.py:LIFT_DOMAINS` cover indices through five and multiplicities
+  through three. Every GL2 action and every nonzero multiplicity determinant
+  is tested in those domains, including nonscalar repeated-block mixing:
+  4,932 right-block lifts and 4,932 transposed lifts.
+- **Converse:** all 454 nonzero determinant triples across both orientations
+  in those domains are checked: 154 produce literal stabilizers with exactly
+  the requested determinants and 300 are excluded by the character.
+- **Failure controls:** six mathematical mutants detect a missing slice
+  exponent, missing multiplicity, wrong orientation, two incorrect right-factor
+  conventions and binomial reduction modulo q instead of the characteristic.
+  Fourteen malformed/domain controls reject; 224 finite-field triples check
+  associativity and distributivity. These explicit checks survive `-O`.
+
+These are bounded checks, not exhaustive verification of every field or index.
+F4 lift checks exercise characteristic two with nontrivial determinants; the
+independent exhaustive stabilizer oracle is over prime fields only. Necessity
+in general dimensions rests on the written block recurrence. Code limits are
+e<=5, r<=3 and q in {2,3,4,5}; admitted bounds do not mean every combination was
+tested. The oracle caps raw matrix enumeration at 625, retained group size at
+480 and P,R pairs at 2,304 per fixture. No dependencies were added. Functions
+are short, loops are bounded, and Python's managed allocation is used for these
+small matrices; this is not an unbounded public tensor API.
+
+## Boundaries and credit
+
+Excluded: degree-zero unused rows/columns, unequal minimal indices, mixtures
+of left and right blocks, regular/singular coupling, and regular pencils with
+no invertible base-field rational slice. No arbitrary-tensor recognition or
+uniform bit-complexity result is supplied. Native realization, dirty-state
+ownership, routing, storage, precision, compiler cost and the full recursive
+invoice remain **unknown**, not free. No physical supplier, selected-frontier
+change, complete multiplication theorem, Lean build or selected cold replay is
+claimed. Human and formal proof-kernel review remain unclaimed; parallel agent
+checks are AI-assisted review.
+
+Nick Petalas retains credit for the restricted regular-pencil extraction and
+this explicit handoff. David Ganz retains atlas A030/A026/A029 and its cited
+tensor/stabilizer lineage. The classical Kronecker, symmetric-power and
+centralizer/canonical-form results remain predecessor work; this package does
+not reproduce or claim the regular-pencil algorithms of Arne Storjohann or
+the determinant work of Ferrer, Mingueza and Montoro. Source pins and the atlas
+attribution file are recorded in SOURCES.json. Prepared by **apoursh** with
+substantial **OpenAI Codex** assistance, including parallel proof, overlap and
+independent corroborator work. Apache-2.0.
+
+## Open next questions
+
+- **Mixed positive minimal indices and block types.** Classify the fixed-slice
+  homomorphisms of L_1 direct sum L_2, then determine how they affect determinant
+  characters before adding any regular block. This is needed to combine the
+  one-type result with PR5250; a mixed-block filtration and complete slice-action
+  analysis are missing here.
+- **Regular pencils without an invertible rational slice.** Start with
+  diag(s,t,s+t) over F2 and its homogeneous elementary divisors. Its determinant
+  polynomial is nonzero but all base-field projective slices are singular.
+  A coordinate-independent replacement for B_R inverse and compatible descent
+  remain the separate blocker in PR5250.
+
+Structured relevance, first steps and blockers are also in TASK.json. Neither
+question is reserved by this submission.
diff --git a/research/mixed-singular-kronecker-characters/source/pencil.py b/research/mixed-singular-kronecker-characters/source/pencil.py
new file mode 100644
index 0000000000..6bc7fc076e
--- /dev/null
+++ b/research/mixed-singular-kronecker-characters/source/pencil.py
@@ -0,0 +1,195 @@
+"""Bounded exact witnesses for the written Kronecker determinant theorem.
+
+The implementation is deliberately limited to small fixtures; PROOF.md supplies
+the arbitrary-field/dimension argument. apoursh with OpenAI Codex; Apache-2.0.
+"""
+from itertools import product
+
+
+def require(ok, message):
+    if not ok:
+        raise ValueError(message)
+
+
+class Field:
+    """F2, F3, F5, or F4=F2[w]/(w^2+w+1), encoded 0,1,w,w+1."""
+    def __init__(self, order):
+        require(type(order) is int and order in (2, 3, 4, 5), 'unsupported field')
+        self.q = order
+        self.p = 2 if order == 4 else order
+
+    def add(self, a, b):
+        return a ^ b if self.q == 4 else (a + b) % self.q
+
+    def neg(self, a):
+        return a if self.q == 4 else -a % self.q
+
+    def sub(self, a, b):
+        return self.add(a, self.neg(b))
+
+    def mul(self, a, b):
+        if self.q != 4:
+            return a * b % self.q
+        value = 0
+        for bit in range(2):
+            if (b >> bit) & 1:
+                value ^= a << bit
+        return value ^ 7 if value & 4 else value
+
+    def power(self, a, exponent):
+        if exponent < 0:
+            require(a != 0, 'inverse of zero')
+            exponent %= self.q - 1
+        value = 1
+        for _ in range(exponent):
+            value = self.mul(value, a)
+        return value
+
+    def inv(self, a):
+        require(a != 0, 'inverse of zero')
+        return self.power(a, self.q - 2)
+
+
+def identity(n):
+    return [[int(i == j) for j in range(n)] for i in range(n)]
+
+
+def transpose(a):
+    return [list(row) for row in zip(*a)]
+
+
+def multiply(a, b, field):
+    require(len(a[0]) == len(b), 'matrix dimension mismatch')
+    result = [[0] * len(b[0]) for _ in a]
+    for i, row in enumerate(a):
+        for k, value in enumerate(row):
+            if value:
+                for j, other in enumerate(b[k]):
+                    result[i][j] = field.add(result[i][j], field.mul(value, other))
+    return result
+
+
+def mix(a, b, x, y, field):
+    return [[field.add(field.mul(x, u), field.mul(y, v))
+             for u, v in zip(row, other)] for row, other in zip(a, b)]
+
+
+def determinant(a, field):
+    rows = [row[:] for row in a]
+    result = 1
+    for col in range(len(rows)):
+        pivot = next((i for i in range(col, len(rows)) if rows[i][col]), None)
+        if pivot is None:
+            return 0
+        if pivot != col:
+            rows[col], rows[pivot] = rows[pivot], rows[col]
+            result = field.neg(result)
+        result = field.mul(result, rows[col][col])
+        inv = field.inv(rows[col][col])
+        for i in range(col + 1, len(rows)):
+            scale = field.mul(rows[i][col], inv)
+            rows[i] = [field.sub(x, field.mul(scale, y))
+                       for x, y in zip(rows[i], rows[col])]
+    return result
+
+
+def inverse(a, field):
+    n = len(a)
+    rows = [row[:] + unit for row, unit in zip(a, identity(n))]
+    for col in range(n):
+        pivot = next((i for i in range(col, n) if rows[i][col]), None)
+        require(pivot is not None, 'singular matrix')
+        rows[col], rows[pivot] = rows[pivot], rows[col]
+        inv = field.inv(rows[col][col])
+        rows[col] = [field.mul(inv, value) for value in rows[col]]
+        for i in range(n):
+            if i != col:
+                scale = rows[i][col]
+                rows[i] = [field.sub(x, field.mul(scale, y))
+                           for x, y in zip(rows[i], rows[col])]
+    return [row[n:] for row in rows]
+
+
+def tensor(a, b, field):
+    return [[field.mul(x, y) for x in row for y in other]
+            for row in a for other in b]
+
+
+def slices(e, r):
+    require(type(e) is int and type(r) is int and 1 <= e <= 5 and 1 <= r <= 3,
+            'outside bounded positive-index fixture domain')
+    return ([[int(j == i) for j in range((e + 1) * r)] for i in range(e * r)],
+            [[int(j == i + r) for j in range((e + 1) * r)] for i in range(e * r)])
+
+
+def symmetric_power(k, action, field):
+    """Ordinary monomial substitution, using convolution without factorials."""
+    require(type(k) is int and 0 <= k <= 5, 'unsupported degree')
+    columns = []
+    for i in range(k + 1):
+        coefficients = [1]
+        for linear in [action[0]] * (k - i) + [action[1]] * i:
+            result = [0] * (len(coefficients) + 1)
+            for j, value in enumerate(coefficients):
+                result[j] = field.add(result[j], field.mul(value, linear[0]))
+                result[j + 1] = field.add(result[j + 1], field.mul(value, linear[1]))
+            coefficients = result
+        columns.append(coefficients)
+    return transpose(columns)
+
+
+def general_linear_two(field):
+    for entries in product(range(field.q), repeat=4):
+        action = [list(entries[:2]), list(entries[2:])]
+        if determinant(action, field):
+            yield action
+
+
+def lift(e, r, action, multiplicity, field):
+    slices(e, r)
+    require(len(action) == 2 and all(len(row) == 2 for row in action),
+            'slice action dimension mismatch')
+    require(len(multiplicity) == r and all(len(row) == r for row in multiplicity),
+            'multiplicity dimension mismatch')
+    require(all(type(x) is int and 0 <= x < field.q
+                for matrix in (action, multiplicity) for row in matrix for x in row),
+            'matrix entry outside field')
+    require(determinant(action, field) != 0, 'singular slice action')
+    require(determinant(multiplicity, field) != 0, 'singular multiplicity action')
+    p = tensor(transpose(symmetric_power(e - 1, action, field)), multiplicity, field)
+    q = tensor(inverse(symmetric_power(e, action, field), field),
+               transpose(inverse(multiplicity, field)), field)
+    return p, q, action
+
+
+def fixes(first, second, witness, field):
+    p, q, action = witness
+    for row, target in zip(action, (first, second)):
+        mixed = mix(first, second, *row, field)
+        if multiply(multiply(p, mixed, field), transpose(q), field) != target:
+            return False
+    return True
+
+
+def character(e, r, triple, field, left=False):
+    x, y, z = triple
+    if left:
+        x, y = y, x
+    return field.mul(field.mul(field.power(x, e + 1), field.power(y, e)),
+                     field.power(z, r * e * (e + 1) // 2))
+
+
+def witness_for_triple(e, r, triple, field, left=False):
+    slices(e, r)
+    require(len(triple) == 3, 'determinant triple dimension mismatch')
+    require(all(type(x) is int and 0 < x < field.q for x in triple),
+            'determinants must be nonzero field elements')
+    require(character(e, r, triple, field, left) == 1, 'character excludes triple')
+    x, y, z = triple
+    if left:
+        x, y = y, x
+    u = field.mul(field.inv(field.mul(x, y)), field.power(z, -r * e))
+    d = identity(r)
+    d[0][0] = u
+    p, q, action = lift(e, r, [[z, 0], [0, 1]], d, field)
+    return (q, p, action) if left else (p, q, action)
diff --git a/research/mixed-singular-kronecker-characters/verify.py b/research/mixed-singular-kronecker-characters/verify.py
new file mode 100644
index 0000000000..bfe546c13d
--- /dev/null
+++ b/research/mixed-singular-kronecker-characters/verify.py
@@ -0,0 +1,170 @@
+"""Verify mixed singular characters against literal equations and witnesses."""
+from itertools import product,permutations
+from math import gcd
+from pathlib import Path
+import json
+import sys
+sys.path.insert(0,str(Path(__file__).resolve().parent))
+import mixed as M
+import oracle as O
+R=Path(__file__).resolve().parent
+
+
+def dot(a,b,f):
+    v=0
+    for x,y in zip(a,b):v=f.add(v,f.mul(x,y))
+    return v
+
+
+def single(side,e):
+    m,n=e+(side=='L'),e+(side=='R');a=[[0]*n for _ in range(m)];b=[[0]*n for _ in range(m)]
+    for i in range(e):
+        a[i][i]=1
+        if side=='R':b[i][i+1]=1
+        else:b[i+1][i]=1
+    return (a,b),(m,n)
+
+
+def hom_checks():
+    counts=[]
+    for q in (2,3,4,5):
+        f=M.Field(q);cases=dimension=0
+        for src,dst in product(product(('R','L'),range(4)),repeat=2):
+            a,ad=single(*src);b,bd=single(*dst);equations,width=O.equations(a,b,ad,bd,f)
+            literal=O.nullspace(equations,width,f)
+            proposed=[[x for row in u+c for x in row]for u,c in M.hom_single(src,dst)]
+            M.need(all(len(v)==width for v in proposed),'Complete zero-index Hom shapes')
+            M.need(all(dot(row,v,f)==0 for row in equations for v in proposed),'Every explicit off-diagonal intertwiner')
+            M.need(len(literal)==len(proposed)==width-len(O.nullspace(proposed,width,f)),'Complete Hom basis and linear independence')
+            cases+=1;dimension+=len(literal)
+        counts.append(dict(field=q,ordered_pairs=cases,total_Hom_dimension=dimension))
+    return counts
+
+
+DOMAINS=[
+ (2,[('R',1,1),('R',2,1)],True),
+ (3,[('R',1,1),('R',2,1)],True),
+ (4,[('R',1,1),('L',1,1)],True),
+ (3,[('R',0,1),('R',2,1)],False),
+ (3,[('L',0,1),('L',2,1)],False),
+ (5,[('R',1,1),('L',2,1)],False),
+ (3,[('R',1,2),('L',0,1)],False),
+ (2,[('R',0,2),('L',0,2)],True),
+ (4,[('R',2,1),('R',4,1)],False),
+ (3,[('R',1,1),('R',3,1)],False),
+ (3,[('L',1,1),('L',3,1)],False),
+ (2,[('R',0,1),('R',1,1),('L',0,1),('L',1,1)],True),
+]
+
+
+def oracle_checks():
+    reports=[]
+    for q,model,all_actions in DOMAINS:
+        f=M.Field(q);a,b=M.slices(model);m,n=len(a),len(a[0]);data=M.character_data(model)
+        basis=M.fixed_slice_basis(model);equations,width=O.equations((a,b),(a,b),(m,n),(m,n),f)
+        literal=O.nullspace(equations,width,f)
+        M.need(len(literal)==len(basis)==width-len(O.nullspace(basis,width,f)),'Complete mixed fixed-slice dimension')
+        M.need(all(dot(row,v,f)==0 for row in equations for v in basis),'All mixed Hom coefficients satisfy literal equations')
+        actions=list(M.old.general_linear_two(f)) if all_actions else [[[z,0],[0,1]]for z in range(1,q)]
+        image=set();accepted=0;tested=0
+        for action in actions:
+            kernel=O.stabilizer_space(a,b,action,f);M.need(len(kernel)==len(literal),'Every slice action has full expected dimension')
+            pairs,count=O.enumerate_space(kernel,m,n,f);z=O.determinant(action,f)
+            image.update((x,y,z)for x,y in pairs);accepted+=count;tested+=q**len(kernel)
+        predicted={triple for triple in product(range(1,q),repeat=3)if M.accepts(model,triple,f)}
+        M.need(image==predicted,'Literal full mixed determinant image')
+        index=(q-1)**3//len(image);M.need(index==gcd(q-1,data['power_index']),'Exact finite-field orbit count')
+        reports.append(dict(field=q,model=model,dimensions=[m,n],endomorphism_dimension=len(literal),slice_actions=len(actions),
+                            all_slice_actions=all_actions,linear_solutions_tested=tested,stabilizers=accepted,
+                            determinant_image=sorted(image),special_linear_orbits=index))
+        print('PASS_LITERAL_DOMAIN',q,model,flush=True)
+    return reports
+
+
+def witness_checks():
+    reports=[];all_models=[(q,model)for q,model,_ in DOMAINS]
+    all_models += [(5,[('R',1,2),('L',2,1)]),(4,[('R',0,1),('L',3,1)]),(3,[('L',2,3)]),(5,[('R',4,1),('R',5,1)]),(3,[('R',1,2),('R',2,2)]),(5,[('R',1,1),('L',1,1)]),(5,[('R',1,1),('R',3,1),('L',1,1)])]
+    for q,model in all_models:
+        f=M.Field(q);a,b=M.slices(model);yes=no=0
+        for triple in product(range(1,q),repeat=3):
+            if M.accepts(model,triple,f):
+                M.witness(model,triple,f)
+                maps=[M.old.identity(len(a)),M.old.identity(len(a[0])),M.old.identity(2)]
+                for matrix,value in zip(maps,triple):
+                    matrix[0][0]=value
+                    if len(matrix)>1:matrix[0][1]=1
+                M.correct_given_map(model,maps,f);yes+=1
+            else:
+                try:M.witness(model,triple,f)
+                except ValueError:no+=1
+                else:raise ValueError('Excluded determinant triple accepted')
+        data=M.character_data(model);lifts=0
+        for action in M.old.general_linear_two(f):
+            # Both constant and nonconstant type determinants are tested.
+            for choice in (0,1):
+                scalars=[1+(choice+i)%(q-1) for i in range(len(data['types']))]
+                w=M.lift(model,action,scalars,f)
+                M.need(M.old.fixes(a,b,w,f),'Every GL2 literal mixed lift')
+                triple=tuple(M.old.determinant(x,f)for x in w)
+                M.need(M.accepts(model,triple,f),'Every lift has the stated character')
+                # The converse also permits the same prescribed non-diagonal action.
+                M.witness(model,triple,f,action);lifts+=1
+        reports.append(dict(field=q,model=model,accepted_triples=yes,excluded_triples=no,special_linear_corrections=yes,lifts=lifts,
+                            power_index=data['power_index'],character_exponents=list(data['ell'])+[data['character_slice_exponent']]))
+    return reports
+
+
+def controls():
+    f=M.Field(5);model=[('R',1,1),('L',2,1)];data=M.character_data(model);a,b=M.slices(model)
+    wrong_shift=[]
+    for triple in product(range(1,5),repeat=3):
+        x,y,z=triple;wrong=f.mul(f.power(x,data['ell'][0]),f.power(y,data['ell'][1]))
+        if (wrong==1)!=M.accepts(model,triple,f):wrong_shift.append(triple)
+    M.need(wrong_shift,'Slice determinant cannot be omitted')
+    noncommuting=[[1,1],[0,1]];w=M.lift(model,noncommuting,[2,3],f)
+    M.need(not M.old.fixes(a,b,(w[0],M.old.transpose(w[1]),w[2]),f),'Missing Q transpose control')
+    M.need(not M.old.fixes(a,b,(w[0],w[1],M.old.transpose(w[2])),f),'Slice action orientation control')
+    M.need(len(M.fixed_slice_basis([('R',1,1),('R',2,1)]))==4,'Unequal right indices have off-diagonal mixing')
+    M.need(len(M.fixed_slice_basis([('R',1,1),('L',1,1)]))==4,'Left-to-right mixing is present')
+    M.need(not M.hom_single(('R',1),('L',1)),'Forbidden reverse cross-orientation map')
+    M.need(M.character_data([('R',1,2),('R',2,2)])['power_index']==1,'Multiplicity does not multiply the index lattice')
+    M.need(M.character_data([('R',1,1),('L',1,1)])['power_index']==3,'Cross-orientation uses e+f+1')
+    rejected=[]
+    for name,model in [('empty',[]),('unknown_side',[('Z',1,1)]),('negative_index',[('R',-1,1)]),('zero_multiplicity',[('R',1,0)]),('zero_rows',[('R',0,1)]),('zero_columns',[('L',0,1)]),('too_large_index',[('R',6,1)]),('noninteger_index',[('R',True,1)]),('combined_multiplicity',[('R',1,2),('R',1,2)])]:
+        try:M.types(model)
+        except ValueError:rejected.append(name)
+        else:raise ValueError('Invalid model accepted '+name)
+    for name,triple in [('zero_determinant',(0,1,1)),('outside_field',(5,1,1)),('wrong_arity',(1,1))]:
+        try:M.accepts([('R',1,1)],triple,f)
+        except ValueError:rejected.append(name)
+        else:raise ValueError('Invalid triple accepted '+name)
+    # Compare elimination with Leibniz on every matrix in the stated tiny domains.
+    determinant_cases=0
+    for q,n in [(2,3),(3,2),(4,2),(5,2)]:
+        ff=M.Field(q)
+        for values in product(range(q),repeat=n*n):
+            matrix=[list(values[i*n:(i+1)*n])for i in range(n)];value=0
+            for perm in permutations(range(n)):
+                term=1
+                for i,j in enumerate(perm):term=ff.mul(term,matrix[i][j])
+                if sum(perm[i]>perm[j]for i in range(n)for j in range(i+1,n))%2:term=ff.neg(term)
+                value=ff.add(value,term)
+            M.need(value==O.determinant(matrix,ff)==M.old.determinant(matrix,ff),'Independent permutation determinant')
+            determinant_cases+=1
+    return dict(wrong_slice_shift_triples=len(wrong_shift),mathematical_controls=['slice_shift','Q_transpose','slice_orientation','unequal_right_mixing','left_to_right_mixing','forbidden_reverse_mixing','multiplicity_index','cross_orientation_sum'],malformed_rejections=rejected,permutation_determinant_cases=determinant_cases)
+
+
+def run():
+    return dict(status='PASS_MIXED_SINGULAR_KRONECKER_CHARACTERS',hom_domains=hom_checks(),
+                literal_oracles=oracle_checks(),constructive_witnesses=witness_checks(),controls=controls(),
+                scope='All-field proof for supplied purely singular direct sums; bounded executable F2/F3/F4/F5 models. Regular factors, arbitrary extraction and physical pricing remain open.')
+
+
+def main():
+    result=json.loads(json.dumps(run()))
+    if '--write'in sys.argv:(R/'RESULT.json').write_text(json.dumps(result,indent=2,sort_keys=True)+'\n')
+    else:M.need(result==json.loads((R/'RESULT.json').read_text()),'Exact published result')
+    print(result['status'],flush=True)
+
+
+if __name__=='__main__':main()