The Frattini layer centralizes the minimal kernel

This completes the lower-branch contradiction in lem:collapse.

The Hall--Witt/centralizer dichotomy says that, for the same odd Hall witness, either normalClosure([K,Ñ]) ≤ S or [K, Φ(K)] = 1. In the lower branch, the tame 2-power preimage P0 acts trivially on the chief factor P/S; the finite 2-group fixed-vector argument then produces a nontrivial globally fixed class in P/S. Section7FixedLift turns that into ChiefFactorTrivial, contradicting the first non-scalar choice. Thus only the central branch remains.

theorem Q2Presentation.Induction.kernel_commutator_frattini_eq_bot {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : ⁅K.Ksub, kernelFrattini K⁆ = ⊥

lem:collapse, central branch. For the manuscript's minimal kernel K, its Frattini layer R = Φ(K) is centralized by K.