The three-subgroup step for the Frattini centralizer

This is the Hall--Witt/three-subgroups part of lem:collapse.

For the odd Hall lift Ñ from Section7OddHall.lean:

• Ñ centralizes R = Φ(K);
• [K,R] ≤ R, so [K,R] centralizes Ñ;
• therefore the Three Subgroups Lemma gives [[K,Ñ],R]=1.

Equivalently, [K,Ñ] ≤ C_Y(R).

theorem Q2Presentation.Induction.kernel_oddHall_commutator_centralizes_frattini {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (s t : p.fst.H) (hgen : Subgroup.closure {s, t} = ⊤) (htame : rconj t s = t ^ 2) : ∃ (Ñ : Subgroup p.fst.Y), Odd (Nat.card ↥Ñ) ∧ ⁅⁅K.Ksub, Ñ⁆, kernelFrattini K⁆ = ⊥

Three-subgroups/Hall--Witt step. The commutator of the minimal kernel with the tame odd Hall lift centralizes the Frattini layer R = Φ(K).

theorem Q2Presentation.Induction.kernel_oddHall_commutator_le_frattini_centralizer {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (s t : p.fst.H) (hgen : Subgroup.closure {s, t} = ⊤) (htame : rconj t s = t ^ 2) : ∃ (Ñ : Subgroup p.fst.Y), Odd (Nat.card ↥Ñ) ∧ ⁅K.Ksub, Ñ⁆ ≤ Subgroup.centralizer ↑(kernelFrattini K)

Centralizer-subgroup form of kernel_oddHall_commutator_centralizes_frattini.