theorem Q2Presentation.Induction.wild_commutator_mem_lower {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (y : p.fst.Y) (hy : y ∈ p.fst.LY) (n : p.fst.Y) (hn : n ∈ chief.upper) : ⁅y, n⁆ ∈ chief.lower

The wild part centralizes the chief factor: for y ∈ L_Y and n ∈ upper, the commutator ⁅y, n⁆ lies in lower.

Head-operator triviality for wild elements

theorem Q2Presentation.Induction.headOp_wild_eq_one {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (hR : Nat.card ↥(kernelFrattini K) = 1) (y : p.fst.Y) (hy : y ∈ p.fst.LY) : headOp chief K hR y = 1

Wild elements act trivially on the head: for y ∈ L_Y the descended head operator is the identity.