Route199 Frattini closers for the Route198 kernel frontier

Route198 exposes ten Route72 least-kernel/Frattini atoms. This sidecar keeps the same downstream consumer surface, but replaces those Route72 atoms by smaller Route199 packets:

• the least-kernel candidate is split into carrier, normality, containment, and product-image fields;
• universal leastness is checked pointwise against an arbitrary candidate;
• the internal Frattini witness is split into carrier, membership, and nontriviality;
• centralizer and fourth-power packets are split into carrier/property/image fields;
• the square/commutator layer is split into carrier, containment, and pointwise exponent-after-collapse data.

Least kernel selection

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.LeastKernelCarrierData {p : FramedPair} (chief : NonScalarChiefFactor p) : Type

Route199 carrier for the selected least-kernel candidate.

• Ksub : Subgroup p.fst.Y

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.LeastKernelNormalData {p : FramedPair} {chief : NonScalarChiefFactor p} (C : LeastKernelCarrierData chief) : Prop

Route199 normality field for the selected least-kernel carrier.

• Ksub_normal : C.Ksub.Normal

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.LeastKernelUpperContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} (C : LeastKernelCarrierData chief) : Prop

Route199 upper-containment field for the selected least-kernel carrier.

• Ksub_le_upper : C.Ksub ≤ chief.upper

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.LeastKernelChiefImageData {p : FramedPair} {chief : NonScalarChiefFactor p} (C : LeastKernelCarrierData chief) : Prop

Route199 chief-factor image field for the selected least-kernel carrier.

• KS_eq_upper : C.Ksub ⊔ chief.lower = chief.upper

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.leastKernelCarrierData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (LeastKernelCarrierData chief)

Route199 carrier atom for the selected least-kernel candidate.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.leastKernelNormalData {p : FramedPair} {chief : NonScalarChiefFactor p} (C : LeastKernelCarrierData chief) : Nonempty (LeastKernelNormalData C)

Route199 normality atom for the selected least-kernel carrier.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.leastKernelUpperContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} (C : LeastKernelCarrierData chief) : Nonempty (LeastKernelUpperContainmentData C)

Route199 upper-containment atom for the selected least-kernel carrier.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.leastKernelChiefImageData {p : FramedPair} {chief : NonScalarChiefFactor p} (C : LeastKernelCarrierData chief) : Nonempty (LeastKernelChiefImageData C)

Route199 chief-factor image atom for the selected least-kernel carrier.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.leastKernelCandidateData_from_route199Frattini {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelCandidateData chief)

Reassemble the Route72 candidate atom from Route199 fields.

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.LeastKernelUniversalCandidatePointData {p : FramedPair} {chief : NonScalarChiefFactor p} (K C : MinimalBlockKernelCandidateData chief) : Prop

Route199 pointwise universal leastness comparison against one candidate.

• le_selected_of_candidate : K.Ksub ≤ C.Ksub

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.leastKernelUniversalCandidatePointData {p : FramedPair} {chief : NonScalarChiefFactor p} (K C : MinimalBlockKernelCandidateData chief) : Nonempty (LeastKernelUniversalCandidatePointData K C)

Route199 pointwise universal leastness atom.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.leastKernelUniversalData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelCandidateData chief) : Nonempty (MinimalBlockKernelLeastUniversalData K)

Reassemble the Route72 universal leastness atom from Route199 pointwise candidate comparisons.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.leastKernelSelectionData_from_route199Frattini {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelRoute67FrattiniClosers.LeastKernelSelectionData chief)

Route67 least-kernel packet assembled from Route199 lower fields.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.leastOverChiefData_from_route199Frattini {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelLeastOverChiefData chief)

Route199 least-over-chief packet.

Frattini nonidentity

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.FrattiniInternalElementCarrierData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Type

Route199 carrier for the internal Frattini witness.

• r : ↥K.Ksub

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.FrattiniInternalElementMembershipData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (E : FrattiniInternalElementCarrierData K) : Prop

Route199 membership field for the internal Frattini witness.

• r_mem_frattini : E.r ∈ frattini ↥K.Ksub

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniInternalElementCarrierData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniInternalElementCarrierData K)

Route199 internal Frattini carrier atom.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniInternalElementMembershipData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (E : FrattiniInternalElementCarrierData K) : Nonempty (FrattiniInternalElementMembershipData E)

Route199 internal Frattini membership atom.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniInternalElementData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FrattiniInternalElementData K)

Reassemble the Route72 internal Frattini element atom from Route199 fields.

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.FrattiniInternalElementAmbientNontrivialData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (E : MinimalBlockKernelRoute72FrattiniClosers.FrattiniInternalElementData K) : Prop

Route199 ambient nontriviality field for the selected internal element.

• r_ne_one : ↑E.r ≠ 1

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniInternalElementAmbientNontrivialData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (E : MinimalBlockKernelRoute72FrattiniClosers.FrattiniInternalElementData K) : Nonempty (FrattiniInternalElementAmbientNontrivialData E)

Route199 ambient nontriviality atom for the selected internal element.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniInternalElementNontrivialData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (E : MinimalBlockKernelRoute72FrattiniClosers.FrattiniInternalElementData K) : Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FrattiniInternalElementNontrivialData E)

Reassemble the Route72 internal-element nontriviality atom from Route199.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniInternalNonidentityData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FrattiniInternalNonidentityData K)

Route67 internal nonidentity packet assembled from Route199 fields.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniNontrivialData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniNontrivialData K)

Route199 Frattini nontriviality from the split internal witness.

Centralizer-collapse step

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.FrattiniCentralizerCarrierData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Type

Route199 carrier for the centralizer subgroup.

• centralizerSub : Subgroup p.fst.Y

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.FrattiniCentralizerNormalData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (C : FrattiniCentralizerCarrierData K) : Prop

Route199 normality field for the centralizer subgroup.

• centralizerSub_normal : C.centralizerSub.Normal

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.FrattiniCentralizerKernelContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (C : FrattiniCentralizerCarrierData K) : Prop

Route199 containment field for the centralizer subgroup.

• centralizerSub_le_K : C.centralizerSub ≤ K.Ksub

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.FrattiniCentralizerCommutesData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (C : FrattiniCentralizerCarrierData K) : Prop

Route199 commutation field for the centralizer subgroup.

• centralizerSub_centralizes_frattini (c : p.fst.Y) : c ∈ C.centralizerSub → ∀ r ∈ Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub), c * r = r * c

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniCentralizerCarrierData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniCentralizerCarrierData K)

Route199 centralizer carrier atom.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniCentralizerNormalData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (C : FrattiniCentralizerCarrierData K) : Nonempty (FrattiniCentralizerNormalData C)

Route199 centralizer normality atom.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniCentralizerKernelContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (C : FrattiniCentralizerCarrierData K) : Nonempty (FrattiniCentralizerKernelContainmentData C)

Route199 centralizer containment atom.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniCentralizerCommutesData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (C : FrattiniCentralizerCarrierData K) : Nonempty (FrattiniCentralizerCommutesData C)

Route199 centralizer commutation atom.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniCentralizerCoreData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FrattiniCentralizerCoreData K)

Reassemble the Route72 centralizer core atom from Route199 fields.

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.FrattiniCentralizerHallCarrierData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (C : MinimalBlockKernelRoute72FrattiniClosers.FrattiniCentralizerCoreData K) : Type

Route199 carrier for the Hall commutator subgroup used in the centralizer step.

• commutatorSub : Subgroup p.fst.Y

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.FrattiniCentralizerHallContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {C : MinimalBlockKernelRoute72FrattiniClosers.FrattiniCentralizerCoreData K} (H : FrattiniCentralizerHallCarrierData C) : Prop

Route199 containment of the Hall commutator subgroup in the centralizer.

• commutatorSub_le_centralizer : H.commutatorSub ≤ C.centralizerSub

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.FrattiniCentralizerHallImageOntoData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {C : MinimalBlockKernelRoute72FrattiniClosers.FrattiniCentralizerCoreData K} (H : FrattiniCentralizerHallCarrierData C) : Prop

Route199 image-on-chief field for the centralizer Hall subgroup.

• commutatorSub_sup_lower : H.commutatorSub ⊔ chief.lower = chief.upper

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniCentralizerHallCarrierData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (C : MinimalBlockKernelRoute72FrattiniClosers.FrattiniCentralizerCoreData K) : Nonempty (FrattiniCentralizerHallCarrierData C)

Route199 centralizer Hall carrier atom.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniCentralizerHallContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {C : MinimalBlockKernelRoute72FrattiniClosers.FrattiniCentralizerCoreData K} (H : FrattiniCentralizerHallCarrierData C) : Nonempty (FrattiniCentralizerHallContainmentData H)

Route199 centralizer Hall containment atom.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniCentralizerHallImageOntoData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {C : MinimalBlockKernelRoute72FrattiniClosers.FrattiniCentralizerCoreData K} (H : FrattiniCentralizerHallCarrierData C) : Nonempty (FrattiniCentralizerHallImageOntoData H)

Route199 centralizer Hall image-on-chief atom.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniCentralizerHallImageData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (C : MinimalBlockKernelRoute72FrattiniClosers.FrattiniCentralizerCoreData K) : Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FrattiniCentralizerHallImageData C)

Reassemble the Route72 centralizer Hall-image atom from Route199 fields.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniCentralizerHallCommutatorData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FrattiniCentralizerHallCommutatorData K)

Route67 centralizer packet assembled from Route199 fields.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniCentralizerStepData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute60FrattiniClosers.FrattiniCentralizerStepData K)

Route199 centralizer step.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniCentralData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniCentralData K)

Concrete centrality packet from the Route199 centralizer step.

Fourth-power step

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.FourthPowerKernelCarrierData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Type

Route199 carrier for the fourth-power kernel.

• fourthKernel : Subgroup p.fst.Y

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.FourthPowerKernelNormalData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (P4 : FourthPowerKernelCarrierData K) : Prop

Route199 normality field for the fourth-power kernel.

• fourthKernel_normal : P4.fourthKernel.Normal

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.FourthPowerKernelContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (P4 : FourthPowerKernelCarrierData K) : Prop

Route199 containment field for the fourth-power kernel.

• fourthKernel_le_K : P4.fourthKernel ≤ K.Ksub

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.FourthPowerKernelVanishesData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (P4 : FourthPowerKernelCarrierData K) : Prop

Route199 fourth-power vanishing field on the selected kernel.

• fourthKernel_fourth_eq_one (k : p.fst.Y) : k ∈ P4.fourthKernel → k ^ 4 = 1

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.fourthPowerKernelCarrierData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FourthPowerKernelCarrierData K)

Route199 fourth-power kernel carrier atom.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.fourthPowerKernelNormalData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (P4 : FourthPowerKernelCarrierData K) : Nonempty (FourthPowerKernelNormalData P4)

Route199 fourth-power kernel normality atom.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.fourthPowerKernelContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (P4 : FourthPowerKernelCarrierData K) : Nonempty (FourthPowerKernelContainmentData P4)

Route199 fourth-power kernel containment atom.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.fourthPowerKernelVanishesData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (P4 : FourthPowerKernelCarrierData K) : Nonempty (FourthPowerKernelVanishesData P4)

Route199 fourth-power vanishing-on-kernel atom.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.fourthPowerKernelCoreData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FourthPowerKernelCoreData K)

Reassemble the Route72 fourth-power kernel core atom from Route199 fields.

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.FourthPowerKernelHallCarrierData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (P4 : MinimalBlockKernelRoute72FrattiniClosers.FourthPowerKernelCoreData K) : Type

Route199 carrier for the Hall commutator subgroup used in the fourth-power step.

• commutatorSub : Subgroup p.fst.Y

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.FourthPowerKernelHallContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {P4 : MinimalBlockKernelRoute72FrattiniClosers.FourthPowerKernelCoreData K} (H : FourthPowerKernelHallCarrierData P4) : Prop

Route199 containment of the Hall commutator subgroup in the fourth-power kernel.

• commutatorSub_le_fourthKernel : H.commutatorSub ≤ P4.fourthKernel

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.FourthPowerKernelHallImageOntoData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {P4 : MinimalBlockKernelRoute72FrattiniClosers.FourthPowerKernelCoreData K} (H : FourthPowerKernelHallCarrierData P4) : Prop

Route199 image-on-chief field for the fourth-power Hall subgroup.

• commutatorSub_sup_lower : H.commutatorSub ⊔ chief.lower = chief.upper

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.fourthPowerKernelHallCarrierData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (P4 : MinimalBlockKernelRoute72FrattiniClosers.FourthPowerKernelCoreData K) : Nonempty (FourthPowerKernelHallCarrierData P4)

Route199 fourth-power Hall carrier atom.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.fourthPowerKernelHallContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {P4 : MinimalBlockKernelRoute72FrattiniClosers.FourthPowerKernelCoreData K} (H : FourthPowerKernelHallCarrierData P4) : Nonempty (FourthPowerKernelHallContainmentData H)

Route199 fourth-power Hall containment atom.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.fourthPowerKernelHallImageOntoData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {P4 : MinimalBlockKernelRoute72FrattiniClosers.FourthPowerKernelCoreData K} (H : FourthPowerKernelHallCarrierData P4) : Nonempty (FourthPowerKernelHallImageOntoData H)

Route199 fourth-power Hall image-on-chief atom.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.fourthPowerKernelHallImageData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (P4 : MinimalBlockKernelRoute72FrattiniClosers.FourthPowerKernelCoreData K) : Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FourthPowerKernelHallImageData P4)

Reassemble the Route72 fourth-power Hall-image atom from Route199 fields.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.fourthPowerKernelCommutatorData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FourthPowerKernelCommutatorData K)

Route67 fourth-power packet assembled from Route199 fields.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.fourthPowerMapVanishesData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute60FrattiniClosers.FourthPowerMapVanishesData K)

Route199 fourth-power vanishing.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.fourthPowerData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFourthPowerData K)

Concrete fourth-power packet from the Route199 fourth-power step.

Elementary Frattini layer

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.FrattiniSquareCommutatorLayerCarrierData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Type

Route199 carrier for the square/commutator layer.

• squareCommutatorLayer : Subgroup p.fst.Y

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.FrattiniSquareCommutatorLayerContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (L : FrattiniSquareCommutatorLayerCarrierData K) : Prop

Route199 containment of the literal Frattini subgroup in the selected square/commutator layer.

• frattini_le_squareCommutatorLayer : Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub) ≤ L.squareCommutatorLayer

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniSquareCommutatorLayerCarrierData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniSquareCommutatorLayerCarrierData K)

Route199 square/commutator layer carrier atom.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniSquareCommutatorLayerContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (L : FrattiniSquareCommutatorLayerCarrierData K) : Nonempty (FrattiniSquareCommutatorLayerContainmentData L)

Route199 square/commutator layer containment atom.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniSquareCommutatorContainmentData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FrattiniSquareCommutatorContainmentData K)

Reassemble the Route72 square/commutator containment atom from Route199 fields.

structure Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.FrattiniSquareCommutatorLayerPointwiseExponentData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (L : MinimalBlockKernelRoute72FrattiniClosers.FrattiniSquareCommutatorContainmentData K) (C : MinimalBlockKernelRoute60FrattiniClosers.FrattiniCentralizerStepData K) (P4 : MinimalBlockKernelRoute60FrattiniClosers.FourthPowerMapVanishesData K) (r : p.fst.Y) (hr : r ∈ L.squareCommutatorLayer) : Prop

Route199 pointwise exponent conclusion for one element of the selected square/commutator layer after the two collapse inputs.

• square_eq_one : r ^ 2 = 1

axiom Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniSquareCommutatorLayerPointwiseExponentData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (L : MinimalBlockKernelRoute72FrattiniClosers.FrattiniSquareCommutatorContainmentData K) (C : MinimalBlockKernelRoute60FrattiniClosers.FrattiniCentralizerStepData K) (P4 : MinimalBlockKernelRoute60FrattiniClosers.FourthPowerMapVanishesData K) (r : p.fst.Y) (hr : r ∈ L.squareCommutatorLayer) : Nonempty (FrattiniSquareCommutatorLayerPointwiseExponentData L C P4 r hr)

Route199 pointwise square/commutator exponent atom.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniSquareCommutatorExponentData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (L : MinimalBlockKernelRoute72FrattiniClosers.FrattiniSquareCommutatorContainmentData K) : Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FrattiniSquareCommutatorExponentData L)

Reassemble the Route72 square/commutator exponent atom from Route199 pointwise data.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniSquareCommutatorLayerData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute67FrattiniClosers.FrattiniSquareCommutatorLayerData K)

Route67 square/commutator layer packet assembled from Route199 fields.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniElementaryLayerData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute60FrattiniClosers.FrattiniElementaryLayerData K)

Route199 elementary Frattini layer.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniExponentData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniExponentData K)

Concrete exponent-two packet from the Route199 elementary layer.

Frattini packet and provider

theorem Q2Presentation.Induction.MinimalBlockKernelRoute199FrattiniClosers.frattiniData_from_route199Frattini {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniData K)

Concrete Frattini packet assembled through the Route199 lower frontier.