Section 7 fourth-power kernel lowering

This route-neutral sidecar lowers Section7FrattiniCentralConcrete.KernelMinimalFourthPowerCandidateData to the manuscript's actual fourth-power-kernel mechanism.

After R = Phi(K) is known to centralize K, the remaining fourth-power part of lem:collapse is to show that the kernel of the map k ↦ k^4 contains the Hall-commutator subgroup [K, Ñ]. The earlier fixed-vector branch already proves that normalClosure([K, Ñ]) cannot lie under the lower chief term for the same tame 2-power-index witness. Consequently any normal fourth-power kernel containing [K, Ñ] still maps onto the selected chief factor, and the corrected KernelMinimal.minimal_inside forces it to equal K.

The file deliberately introduces no axioms and does not edit routed files. It provides standard-axiom bridge theorems that turn the lower, manuscript-shaped kernel data into:

• KernelMinimalFourthPowerCandidateData;
• K^4 = 1 for the corrected KernelMinimal;
• the older MinimalBlockKernelModuleConcreteFourthPowerData packet;
• the existing Frattini exponent/full Frattini packets when supplied with the already isolated square/commutator-layer input.

structure Q2Presentation.Induction.Section7FrattiniCentralConcrete.KernelMinimalFourthPowerClosureData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Type

A lower fourth-power-kernel interface over the corrected manuscript kernel.

Compared with KernelMinimalFourthPowerCandidateData, this structure does not ask the user to prove directly that fourthKernel ⊔ S = P. Instead it records the same tame 2-power-index witness used in the fixed-vector contradiction and asks that the normal closure of [K, Ñ] be contained in the fourth-power kernel. The theorem kernelMinimalFourthPowerCandidateData_of_closureData proves the chief-image condition.

• P0 : Subgroup p.fst.Y
• Ñ : Subgroup p.fst.Y
• P0_normal : self.P0.Normal
• P0_index_pow_two : ∃ (k : ℕ), self.P0.index = 2 ^ k
• lower_branch_action : kernelOddHallCommutatorClosure K self.Ñ ≤ chief.lower → ⁅chief.upper, self.P0⁆ ≤ chief.lower
• fourthKernel : Subgroup p.fst.Y
• fourthKernel_normal : self.fourthKernel.Normal
• fourthKernel_le_K : self.fourthKernel ≤ K.Ksub
• hallClosure_le_fourthKernel : kernelOddHallCommutatorClosure K self.Ñ ≤ self.fourthKernel
• fourthKernel_fourth_eq_one (k : p.fst.Y) : k ∈ self.fourthKernel → k ^ 4 = 1

structure Q2Presentation.Induction.Section7FrattiniCentralConcrete.KernelMinimalFourthPowerMapKernelData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) : Type

An even lower interface for the actual fourth-power map kernel.

This is the form closest to the manuscript sentence f([k,n]) = 1: it suffices to prove that the fourth-power kernel contains the raw commutator subgroup [K, Ñ]. Normality of fourthKernel then promotes this to containment of the normal closure automatically.

• P0 : Subgroup p.fst.Y
• Ñ : Subgroup p.fst.Y
• P0_normal : self.P0.Normal
• P0_index_pow_two : ∃ (k : ℕ), self.P0.index = 2 ^ k
• lower_branch_action : kernelOddHallCommutatorClosure K self.Ñ ≤ chief.lower → ⁅chief.upper, self.P0⁆ ≤ chief.lower
• fourthKernel : Subgroup p.fst.Y
• fourthKernel_normal : self.fourthKernel.Normal
• fourthKernel_le_K : self.fourthKernel ≤ K.Ksub
• commutatorSub_le_fourthKernel : ⁅K.Ksub, self.Ñ⁆ ≤ self.fourthKernel
• fourthKernel_fourth_eq_one (k : p.fst.Y) : k ∈ self.fourthKernel → k ^ 4 = 1

def Q2Presentation.Induction.Section7FrattiniCentralConcrete.KernelMinimalFourthPowerClosureData.ofMapKernelData {p : FramedPair} {chief : FirstNonScalarChiefFactor p} {K : KernelMinimal chief.toNonScalarChiefFactor} (D : KernelMinimalFourthPowerMapKernelData chief K) : KernelMinimalFourthPowerClosureData chief K

Raw commutator containment plus normality gives containment of the normal closure.

Equations

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

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.kernelOddHallCommutatorClosure_sup_lower_eq_upper_of_fourthPowerClosureData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (D : KernelMinimalFourthPowerClosureData chief K) : kernelOddHallCommutatorClosure K D.Ñ ⊔ chief.lower = chief.upper

For the same tame 2-power-index witness, the lower branch of the Hall-commutator chief dichotomy is impossible; hence normalClosure([K, Ñ]) maps onto the chief factor.

def Q2Presentation.Induction.Section7FrattiniCentralConcrete.kernelMinimalFourthPowerCandidateData_of_closureData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (D : KernelMinimalFourthPowerClosureData chief K) : KernelMinimalFourthPowerCandidateData chief K

The lowered closure data supplies the existing corrected fourth-power candidate.

Equations

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

def Q2Presentation.Induction.Section7FrattiniCentralConcrete.kernelMinimalFourthPowerCandidateData_of_mapKernelData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (D : KernelMinimalFourthPowerMapKernelData chief K) : KernelMinimalFourthPowerCandidateData chief K

The actual map-kernel data supplies the existing corrected fourth-power candidate.

Equations

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

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.kernelMinimal_K_fourth_eq_one_of_fourthPowerClosureData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (D : KernelMinimalFourthPowerClosureData chief K) (k : p.fst.Y) : k ∈ K.Ksub → k ^ 4 = 1

Fourth-power vanishing on the corrected manuscript kernel from the closure data.

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.kernelMinimal_K_fourth_eq_one_of_fourthPowerMapKernelData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : KernelMinimal chief.toNonScalarChiefFactor) (D : KernelMinimalFourthPowerMapKernelData chief K) (k : p.fst.Y) : k ∈ K.Ksub → k ^ 4 = 1

Fourth-power vanishing on the corrected manuscript kernel from the map-kernel data.

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.fourthPowerData_from_kernelMinimalFourthPowerClosureData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : MinimalBlockKernelLeastOverChiefData chief.toNonScalarChiefFactor) (D : KernelMinimalFourthPowerClosureData chief (kernelMinimalOfLeastOverChief chief K)) : Nonempty (MinimalBlockKernelModuleConcreteFourthPowerData K)

Old concrete fourth-power packet from the lowered closure data, for route files still using MinimalBlockKernelLeastOverChiefData.

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.fourthPowerData_from_kernelMinimalFourthPowerMapKernelData {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : MinimalBlockKernelLeastOverChiefData chief.toNonScalarChiefFactor) (D : KernelMinimalFourthPowerMapKernelData chief (kernelMinimalOfLeastOverChief chief K)) : Nonempty (MinimalBlockKernelModuleConcreteFourthPowerData K)

Old concrete fourth-power packet from the lowered map-kernel data.

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.frattiniExponentData_from_fourthPowerClosure_squareCommutator {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : MinimalBlockKernelLeastOverChiefData chief.toNonScalarChiefFactor) (D : KernelMinimalFourthPowerClosureData chief (kernelMinimalOfLeastOverChief chief K)) (E : MinimalBlockKernelRoute67FrattiniClosers.FrattiniSquareCommutatorLayerData K) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniExponentData K)

Exponent two on the literal Frattini layer from the lowered fourth-power closure data and the already isolated square/commutator-layer input.

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.frattiniExponentData_from_fourthPowerMapKernel_squareCommutator {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : MinimalBlockKernelLeastOverChiefData chief.toNonScalarChiefFactor) (D : KernelMinimalFourthPowerMapKernelData chief (kernelMinimalOfLeastOverChief chief K)) (E : MinimalBlockKernelRoute67FrattiniClosers.FrattiniSquareCommutatorLayerData K) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniExponentData K)

Exponent two on the literal Frattini layer from the lowered map-kernel data.

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.frattiniData_from_fourthPowerClosure_squareCommutator {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : MinimalBlockKernelLeastOverChiefData chief.toNonScalarChiefFactor) (N : MinimalBlockKernelModuleConcreteFrattiniNormalData K) (C : MinimalBlockKernelModuleConcreteFrattiniNontrivialData K) (D : KernelMinimalFourthPowerClosureData chief (kernelMinimalOfLeastOverChief chief K)) (E : MinimalBlockKernelRoute67FrattiniClosers.FrattiniSquareCommutatorLayerData K) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniData K)

Full concrete Frattini packet from the lowered fourth-power closure data. The only remaining non-centrality inputs are normality/nontriviality of Phi(K) and the square/commutator-layer packet.

theorem Q2Presentation.Induction.Section7FrattiniCentralConcrete.frattiniData_from_fourthPowerMapKernel_squareCommutator {p : FramedPair} (chief : FirstNonScalarChiefFactor p) (K : MinimalBlockKernelLeastOverChiefData chief.toNonScalarChiefFactor) (N : MinimalBlockKernelModuleConcreteFrattiniNormalData K) (C : MinimalBlockKernelModuleConcreteFrattiniNontrivialData K) (D : KernelMinimalFourthPowerMapKernelData chief (kernelMinimalOfLeastOverChief chief K)) (E : MinimalBlockKernelRoute67FrattiniClosers.FrattiniSquareCommutatorLayerData K) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniData K)

Full concrete Frattini packet from the lowered map-kernel data.