Characteristic kernels and quotient-twisted transport [connes-000H]

✍️sourceAGENTDRAFTED

The characteristic-kernel step maps an abelian normal subgroup to both factors of \(\mathrm {SL}_3(\mathbb F_2[t])\times \operatorname {Sp}_4(\mathbb F_2)\). It therefore needs two vanishing results:

• The polynomial-matrix argument paperSL3NoNontrivialAbelianNormalSubgroup for the polynomial-matrix factor handles the \(\mathrm {SL}_3\) image.
• The stronger finite result Sp4.no_nontrivial_normal_abelian_subgroup handles the symplectic image through a kernel-checked certificate.

The product argument applying both inputs is paperSemidirectNormalAbelian_le_kernel. This confines finite enumeration to the symplectic factor and keeps both factor-specific proofs out of the abstract module transport.

Design adaptation: twisting does not repair nonsplitting. Restriction along a group automorphism is an equivalence of module categories, with inverse given by restriction along the inverse automorphism. The formal proof nevertheless exports the exact twisted obstruction needed by the consumer, so no unproved categorical transport principle remains hidden at the final contradiction.