The lower branch makes the 2-power tame quotient act on the chief factor

This is the next lem:collapse bridge after Section7LowerBranch.

The finite tame quotient has a normal odd subgroup N of 2-power index. Pulling N back to Y gives a normal subgroup P0 containing L_Y, again of 2-power index. Schur--Zassenhaus splits P0 as L_Y · Ñ with Ñ odd. In the remaining lower branch, Ñ acts trivially on P/S, and L_Y already acts trivially on P/S; hence all of P0 acts trivially on the chief factor.

theorem Q2Presentation.Induction.exists_tame_twoPower_preimage_with_odd_complement {p : FramedPair} (s t : p.fst.H) (hgen : Subgroup.closure {s, t} = ⊤) (htame : rconj t s = t ^ 2) : ∃ (P0 : Subgroup p.fst.Y) (Ñ : Subgroup p.fst.Y), P0.Normal ∧ p.fst.LY ≤ P0 ∧ (∃ (k : ℕ), P0.index = 2 ^ k) ∧ Ñ ≤ P0 ∧ Odd (Nat.card ↥Ñ) ∧ p.fst.LY ⊔ Ñ = P0

A tame 2-power preimage together with an odd complement. This is the Schur--Zassenhaus bookkeeping from Section7OddHall, but with the normal preimage P0 and the product decomposition retained for the lower-branch argument.

theorem Q2Presentation.Induction.chief_upper_tameTwoPower_preimage_commutator_le_lower_of_closure_le_lower {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) : ∃ (P0 : Subgroup p.fst.Y) (Ñ : Subgroup p.fst.Y), P0.Normal ∧ p.fst.LY ≤ P0 ∧ (∃ (k : ℕ), P0.index = 2 ^ k) ∧ Ñ ≤ P0 ∧ Odd (Nat.card ↥Ñ) ∧ p.fst.LY ⊔ Ñ = P0 ∧ (kernelOddHallCommutatorClosure K Ñ ≤ chief.lower → ⁅chief.upper, P0⁆ ≤ chief.lower)

In the lower branch, the normal tame preimage of 2-power index acts trivially on the chief factor: [P, P0] ≤ S.