The below-scalar odd part centralizes the lower chief layers

This is the next coprime-action input in lem:collapse. The terminal case already proved in CoprimeStability.lean shows that, if every chief factor in L_Y is scalar/trivial, then any odd-order subgroup centralizes every Y-normal subgroup of L_Y.

For the corrected Section 7 setup we only need the same induction below the first non-scalar chief factor. The hypothesis FirstNonScalarChiefFactor.below_scalar gives exactly the scalar/triviality input for all chief factors whose upper term lies in S = chief.lower.

theorem Q2Presentation.Induction.firstChief_lower_le_LY {p : FramedPair} (chief : FirstNonScalarChiefFactor p) : chief.lower ≤ p.fst.LY

The lower term S of a first non-scalar chief factor lies in L_Y.

theorem Q2Presentation.Induction.commutator_subgroup_eq_bot_of_below_scalar {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (A : Subgroup p.fst.Y) (hAodd : Odd (Nat.card ↥A)) (L : Subgroup p.fst.Y) : L.Normal → L ≤ chief.lower → ⁅L, A⁆ = ⊥

Below-scalar coprime stability. If A has odd order, then A centralizes every Y-normal subgroup lying below the first non-scalar lower term S = chief.lower.

This is the terminal coprime-stability induction from commutator_subgroup_eq_bot_of_scalarTerminal, with the scalar-terminal hypothesis replaced by chief.below_scalar on all chief factors below S.

theorem Q2Presentation.Induction.chief_lower_odd_commutator_eq_bot {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (A : Subgroup p.fst.Y) (hAodd : Odd (Nat.card ↥A)) : ⁅chief.lower, A⁆ = ⊥

The lower term S of the first non-scalar chief factor is centralized by any odd-order subgroup.

theorem Q2Presentation.Induction.below_scalar_odd_le_centralizer {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (A L : Subgroup p.fst.Y) (hAodd : Odd (Nat.card ↥A)) (hLnorm : L.Normal) (hLle : L ≤ chief.lower) : L ≤ Subgroup.centralizer ↑A

Centralizer form of commutator_subgroup_eq_bot_of_below_scalar.

theorem Q2Presentation.Induction.chief_lower_odd_le_centralizer {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (A : Subgroup p.fst.Y) (hAodd : Odd (Nat.card ↥A)) : chief.lower ≤ Subgroup.centralizer ↑A

Centralizer form for the whole lower term S = chief.lower.

theorem Q2Presentation.Induction.chief_lower_odd_commute {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (A : Subgroup p.fst.Y) (hAodd : Odd (Nat.card ↥A)) (l : p.fst.Y) : l ∈ chief.lower → ∀ a ∈ A, l * a = a * l

Elementwise form: every odd-order subgroup commutes with S = chief.lower.