A single odd-Hall witness carrying both §7 packages

The earlier §7 files proved two useful facts with existentially chosen odd subgroups:

• the Hall--Witt/three-subgroup argument puts normalClosure([K,Ñ]) inside K ∩ C_Y(Φ(K));
• the tame quotient has a normal 2-power-index preimage P0 = L_Y · Ñ, and in the lower branch this P0 acts trivially on the chief factor.

For the collapse branch these facts must use the same Ñ. The point of this file is that the Hall--Witt argument only needs Ñ to have odd order. We first prove that uniform form, then package it with the tame preimage witness from Section7TwoPowerAction.

theorem Q2Presentation.Induction.kernel_oddSubgroup_commutator_centralizes_frattini {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (Ñ : Subgroup p.fst.Y) (hÑodd : Odd (Nat.card ↥Ñ)) : ⁅⁅K.Ksub, Ñ⁆, kernelFrattini K⁆ = ⊥

Any odd-order subgroup centralizes the Frattini layer R = Φ(K) modulo the three-subgroup argument.

theorem Q2Presentation.Induction.kernel_oddSubgroup_commutator_le_frattini_centralizer {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (Ñ : Subgroup p.fst.Y) (hÑodd : Odd (Nat.card ↥Ñ)) : ⁅K.Ksub, Ñ⁆ ≤ Subgroup.centralizer ↑(kernelFrattini K)

Centralizer-subgroup form of kernel_oddSubgroup_commutator_centralizes_frattini.

theorem Q2Presentation.Induction.kernel_oddSubgroup_commutatorClosure_le_centralizerInKernel {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (Ñ : Subgroup p.fst.Y) (hÑodd : Odd (Nat.card ↥Ñ)) : kernelOddHallCommutatorClosure K Ñ ≤ kernelFrattiniCentralizerInKernel K

The normal closure of [K,Ñ] lies in the Frattini centralizer carrier for any odd-order subgroup Ñ.

theorem Q2Presentation.Induction.exists_tame_twoPower_oddHall_package {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 Ñ ≤ kernelFrattiniCentralizerInKernel K ∧ (kernelOddHallCommutatorClosure K Ñ ≤ chief.lower → ⁅chief.upper, P0⁆ ≤ chief.lower)

A single tame odd-complement witness carrying both the Frattini-centralizer carrier and the lower-branch 2-power action bridge.