The tame odd Hall lift centralizes the lower chief layers

This is the next reusable ingredient in lem:collapse after Section7OddCentralizer.lean.

The terminal split proof in CoprimeStability.lean already contains the finite group bookkeeping:

• the tame quotient H has a normal odd subgroup of 2-power index;
• its preimage P ≤ Y contains L_Y;
• Schur--Zassenhaus splits P as L_Y times an odd complement Ñ.

For the corrected first-chief setup we do not need scalar terminality. Once the odd complement Ñ is built, Section7OddCentralizer.chief_lower_odd_commute shows that Ñ centralizes S = chief.lower.

theorem Q2Presentation.Induction.tame_oddHall_lift_centralizes_lower {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (s t : p.fst.H) (hgen : Subgroup.closure {s, t} = ⊤) (htame : rconj t s = t ^ 2) : ∃ (Ñ : Subgroup p.fst.Y), Odd (Nat.card ↥Ñ) ∧ ∀ l ∈ chief.lower, ∀ n ∈ Ñ, l * n = n * l

The tame quotient supplies an odd lift Ñ ≤ Y, and the first-chief below-scalar induction makes that lift centralize the lower term S = chief.lower.