Assembly bridge for the Section 7 fourth-power map kernel

The preceding files prove all of the tame-witness and lower-branch bookkeeping needed by the fourth-power part of lem:collapse. This file isolates the remaining mathematical construction: for the selected odd Hall witness Ñ, find a normal subgroup of K containing [K, Ñ] on which fourth powers vanish.

Once that witness-specific kernel is supplied, the theorem below assembles the route-neutral KernelMinimalFourthPowerMapKernelData used by the rest of the corrected Section 7 trunk.

structure Q2Presentation.Induction.Section7FrattiniCentralConcrete.KernelMinimalFourthPowerForWitnessData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (Ñ : Subgroup p.fst.Y) : Type

The genuinely remaining fourth-power kernel datum for a fixed odd Hall witness Ñ.

This omits the already-proved tame 2-power preimage and lower-branch action fields from KernelMinimalFourthPowerMapKernelData; those are supplied by exists_tame_twoPower_oddHall_package.

• fourthKernel : Subgroup p.fst.Y
• fourthKernel_normal : self.fourthKernel.Normal
• fourthKernel_le_K : self.fourthKernel ≤ K.Ksub
• commutatorSub_le_fourthKernel : ⁅K.Ksub, Ñ⁆ ≤ self.fourthKernel
• fourthKernel_fourth_eq_one (k : p.fst.Y) : k ∈ self.fourthKernel → k ^ 4 = 1

def Q2Presentation.Induction.Section7FrattiniCentralConcrete.kernelMinimalFourthPowerMapKernelData_of_witnessData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (P0 Ñ : Subgroup p.fst.Y) (hP0norm : P0.Normal) (hidx : ∃ (k : ℕ), P0.index = 2 ^ k) (hlower : kernelOddHallCommutatorClosure K Ñ ≤ chief.lower → ⁅chief.upper, P0⁆ ≤ chief.lower) (D : KernelMinimalFourthPowerForWitnessData chief K Ñ) : KernelMinimalFourthPowerMapKernelData chief K

Assemble the full map-kernel datum from the same tame/odd-Hall witness and the witness-specific fourth-power kernel.

Equations

• One or more equations did not get rendered due to their size.

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.kernelMinimalFourthPowerMapKernelData_of_sameWitnessProvider {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) (provider : ∀ (P0 Ñ : 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) → Nonempty (KernelMinimalFourthPowerForWitnessData chief K Ñ)) : Nonempty (KernelMinimalFourthPowerMapKernelData chief K)

Use the canonical tame/odd-Hall package and a witness-specific fourth-power kernel provider to produce the full map-kernel datum.

This is the precise landing theorem for the remaining fourth-power construction: the provider only has to solve the fourth-power kernel problem for the same Ñ returned by the already-proved tame package.