Route72 Frattini closers for the minimal-block kernel

This sidecar is route-neutral and only targets the Route71 kernel/Frattini frontier. It provides a drop-in group-tower provider with the same surface as minimalBlock_groupTowerData_from_kernelRoute67CombinedClosers, but replaces the five Route67 Frattini leaves by smaller manuscript-shaped packets:

• least K is split into a candidate and universal leastness for that candidate;
• the nonidentity Frattini witness is split into an internal element and its nontriviality;
• the centralizer and fourth-power steps are split into the subgroup/kernel core and the Hall-commutator image onto the selected chief factor;
• the elementary Frattini layer is split into the Phi(K) <= K^2 [K,K] layer containment and the exponent-two conclusion on that layer after collapse.

Least kernel selection

axiom Q2Presentation.Induction.MinimalBlockKernelRoute72FrattiniClosers.leastKernelCandidateData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelCandidateData chief)

Route72 candidate part of the least-kernel choice.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute72FrattiniClosers.leastKernelUniversalData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelCandidateData chief) : Nonempty (MinimalBlockKernelLeastUniversalData K)

Route72 universal leastness for the selected candidate kernel.

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

Assemble the Route67 least-kernel selection packet from Route72's split candidate/universal data.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute72FrattiniClosers.leastOverChiefData_from_route72 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelLeastOverChiefData chief)

Route72 least-over-chief packet.

Frattini nonidentity

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

Route72 internal Frattini element, before asserting it is nontrivial.

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

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

Route72 nontriviality of the selected internal Frattini element.

• r_ne_one : ↑E.r ≠ 1

axiom Q2Presentation.Induction.MinimalBlockKernelRoute72FrattiniClosers.frattiniInternalElementData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniInternalElementData K)

Residual Route72 internal Frattini element.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute72FrattiniClosers.frattiniInternalElementNontrivialData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (E : FrattiniInternalElementData K) : Nonempty (FrattiniInternalElementNontrivialData E)

Residual Route72 nontriviality for the selected internal Frattini element.

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

Assemble the Route67 internal nonidentity packet from the Route72 split.

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

Route72 Frattini nontriviality from the split internal witness.

Centralizer-collapse step

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

Route72 core centralizer packet: a normal subgroup of K centralizing Phi(K).

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

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

Route72 Hall-commutator image packet proving the centralizer core still maps onto the selected chief factor.

• commutatorSub : Subgroup p.fst.Y
• commutatorSub_le_centralizer : self.commutatorSub ≤ C.centralizerSub
• commutatorSub_sup_lower : self.commutatorSub ⊔ chief.lower = chief.upper

axiom Q2Presentation.Induction.MinimalBlockKernelRoute72FrattiniClosers.frattiniCentralizerCoreData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniCentralizerCoreData K)

Residual Route72 centralizer core.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute72FrattiniClosers.frattiniCentralizerHallImageData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (C : FrattiniCentralizerCoreData K) : Nonempty (FrattiniCentralizerHallImageData C)

Residual Route72 Hall-image packet for the selected centralizer core.

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

Assemble the Route67 Hall-commutator centralizer packet from Route72 core and image data.

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

Route72 centralizer step.

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

Concrete centrality packet from the Route72 centralizer step.

Fourth-power step

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

Route72 core fourth-power kernel packet.

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

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

Route72 Hall-commutator image packet proving the fourth-power kernel still maps onto the selected chief factor.

• commutatorSub : Subgroup p.fst.Y
• commutatorSub_le_fourthKernel : self.commutatorSub ≤ P4.fourthKernel
• commutatorSub_sup_lower : self.commutatorSub ⊔ chief.lower = chief.upper

axiom Q2Presentation.Induction.MinimalBlockKernelRoute72FrattiniClosers.fourthPowerKernelCoreData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FourthPowerKernelCoreData K)

Residual Route72 fourth-power kernel core.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute72FrattiniClosers.fourthPowerKernelHallImageData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (P4 : FourthPowerKernelCoreData K) : Nonempty (FourthPowerKernelHallImageData P4)

Residual Route72 Hall-image packet for the selected fourth-power kernel.

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

Assemble the Route67 fourth-power kernel/commutator packet from Route72 core and image data.

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

Route72 fourth-power vanishing from the split kernel/image data.

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

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

Elementary Frattini layer

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

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

• squareCommutatorLayer : Subgroup p.fst.Y
• frattini_le_squareCommutatorLayer : Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub) ≤ self.squareCommutatorLayer

structure Q2Presentation.Induction.MinimalBlockKernelRoute72FrattiniClosers.FrattiniSquareCommutatorExponentData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (L : FrattiniSquareCommutatorContainmentData K) : Prop

Route72 exponent-two conclusion on the selected square/commutator layer after the centralizer and fourth-power collapses.

• squareCommutatorLayer_square_eq_one_of_collapse : MinimalBlockKernelRoute60FrattiniClosers.FrattiniCentralizerStepData K → MinimalBlockKernelRoute60FrattiniClosers.FourthPowerMapVanishesData K → ∀ r ∈ L.squareCommutatorLayer, r ^ 2 = 1

axiom Q2Presentation.Induction.MinimalBlockKernelRoute72FrattiniClosers.frattiniSquareCommutatorContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniSquareCommutatorContainmentData K)

Residual Route72 square/commutator layer containment packet.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute72FrattiniClosers.frattiniSquareCommutatorExponentData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (L : FrattiniSquareCommutatorContainmentData K) : Nonempty (FrattiniSquareCommutatorExponentData L)

Residual Route72 exponent-two packet for the selected square/commutator layer.

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

Assemble the Route67 square/commutator layer packet from Route72 containment and exponent data.

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

Route72 elementary Frattini layer from the split square/commutator data.

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

Concrete exponent-two packet from the Route72 elementary-layer implication.

Frattini packet

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

Concrete Frattini packet assembled through the Route72 lowerings.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute72CombinedClosers.kernelRoute55Data_from_route72 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelRoute55.KernelRoute55Data chief)

Route55-shaped kernel packet using Route72 least/Frattini lowerings and Route63 raw/head lowerings.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute72CombinedClosers.kernelRoute54Data_from_route72 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelRoute54.KernelRoute54Data chief)

Route54 coherent data supplied through the Route72 kernel packet.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute72CombinedClosers.consumedData_from_route72 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelRoute53.ConsumedData chief)

Route53 consumed data supplied through Route72.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute72CombinedClosers.groupInvariantRouteData_from_route72 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route53 group/invariant route data supplied through Route72.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute72CombinedClosers.groupTowerData_from_route72 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupTowerData p chief)

Group-tower provider using Route72 least/Frattini and Route63 raw/head lowerings.

Public provider

theorem Q2Presentation.Induction.minimalBlock_groupTowerData_from_kernelRoute72FrattiniClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupTowerData p chief)

Drop-in replacement for minimalBlock_groupTowerData_from_kernelRoute67CombinedClosers, with the five Route67 least/Frattini atoms replaced by Route72 lower packets.