Route63 least/Frattini closers for the Section 7 minimal-block kernel

This sidecar leaves the routed files untouched. It gives a drop-in group-tower provider with the same target shape as minimalBlock_groupTowerData_from_kernelRoute61CombinedClosers, but replaces the five Route62 least/Frattini atoms by narrower manuscript-shaped packets:

• least-over-chief is assembled from a candidate K plus its universal leastness proof;
• cardinal nontriviality of Phi(K) is assembled from an explicit nonidentity Frattini witness;
• the Frattini-centralizer step is assembled from a centralizer candidate to which leastness applies;
• fourth-power vanishing is assembled from a kernel candidate for the fourth-power map to which leastness applies;
• the elementary Frattini layer is assembled from the preceding two collapse steps through the Phi(K) = K^2 [K,K] exponent-two implication.

Least kernel and Frattini nontriviality

theorem Q2Presentation.Induction.MinimalBlockKernelFrattiniRoute63Closers.leastOverChiefData_from_route63 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelLeastOverChiefData chief)

Route63 least-over-chief packet from the earlier candidate/leastness split.

This avoids the Route62 atom minimalBlock_kernelLeastOverChiefData; the remaining proof obligations are the selected candidate and its universal leastness proof.

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

Route63 Frattini nontriviality from an explicit nonidentity element of Phi(K).

This avoids the Route62 atom minimalBlock_kernelModuleConcreteFrattiniNontrivialData.

Centralizer-collapse step

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

Lower centralizer packet for manuscript Lemma 7.2.

The manuscript proves that C_K(Phi(K)) is a Y-normal candidate still mapping onto the selected chief factor. Leastness of K then forces K into this centralizer. This packet records exactly the candidate needed for that leastness argument, rather than the final pointwise centralizer conclusion.

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

axiom Q2Presentation.Induction.MinimalBlockKernelFrattiniRoute63Closers.frattiniCentralizerCandidateData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniCentralizerCandidateData K)

Residual Route63 centralizer-candidate packet.

def Q2Presentation.Induction.MinimalBlockKernelFrattiniRoute63Closers.frattiniCentralizerStepDataOfCandidate {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (C : FrattiniCentralizerCandidateData K) : MinimalBlockKernelRoute60FrattiniClosers.FrattiniCentralizerStepData K

Turn the centralizer candidate into the Route60 proof-step shape by applying leastness of K.

Equations

• ⋯ = ⋯

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

Route63 replacement for MinimalBlockKernelRoute60FrattiniClosers.frattiniCentralizerStepData.

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

Concrete centrality packet from the Route63 centralizer candidate.

Fourth-power step

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

Lower fourth-power packet for manuscript Lemma 7.2.

The manuscript proves that the kernel of the equivariant fourth-power map is a Y-normal candidate still mapping onto the chief factor; leastness then forces all of K into that kernel.

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

axiom Q2Presentation.Induction.MinimalBlockKernelFrattiniRoute63Closers.fourthPowerKernelCandidateData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FourthPowerKernelCandidateData K)

Residual Route63 fourth-power-kernel packet.

def Q2Presentation.Induction.MinimalBlockKernelFrattiniRoute63Closers.fourthPowerMapVanishesDataOfKernelCandidate {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (P4 : FourthPowerKernelCandidateData K) : MinimalBlockKernelRoute60FrattiniClosers.FourthPowerMapVanishesData K

Turn the fourth-power kernel candidate into the Route60 proof-step shape by applying leastness of K.

Equations

• ⋯ = ⋯

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

Route63 replacement for MinimalBlockKernelRoute60FrattiniClosers.fourthPowerMapVanishesData.

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

Concrete fourth-power packet from the Route63 fourth-power kernel.

Elementary Frattini layer

structure Q2Presentation.Induction.MinimalBlockKernelFrattiniRoute63Closers.FrattiniElementaryLayerFromCollapseData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Prop

Lower elementary-layer packet for the last step of manuscript Lemma 7.2.

After the centralizer and fourth-power steps, the remaining finite-group input is the exponent-two consequence of Phi(K) = K^2 [K,K].

• frattini_square_eq_one_of_collapse : MinimalBlockKernelRoute60FrattiniClosers.FrattiniCentralizerStepData K → MinimalBlockKernelRoute60FrattiniClosers.FourthPowerMapVanishesData K → ∀ r ∈ Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub), r ^ 2 = 1

axiom Q2Presentation.Induction.MinimalBlockKernelFrattiniRoute63Closers.frattiniElementaryLayerFromCollapseData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniElementaryLayerFromCollapseData K)

Residual Route63 elementary-layer implication.

def Q2Presentation.Induction.MinimalBlockKernelFrattiniRoute63Closers.frattiniElementaryLayerDataOfCollapse {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (E : FrattiniElementaryLayerFromCollapseData K) (C : MinimalBlockKernelRoute60FrattiniClosers.FrattiniCentralizerStepData K) (P4 : MinimalBlockKernelRoute60FrattiniClosers.FourthPowerMapVanishesData K) : MinimalBlockKernelRoute60FrattiniClosers.FrattiniElementaryLayerData K

Turn the exponent-two implication into the Route60 proof-step shape.

Equations

• ⋯ = ⋯

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

Route63 replacement for MinimalBlockKernelRoute60FrattiniClosers.frattiniElementaryLayerData.

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

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

Frattini packet and group-tower provider

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

Concrete Frattini packet assembled through the Route63 lowerings.

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

Route55-shaped kernel packet assembled from the Route63 Frattini side and the existing Route60 raw/head side.

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

Route54 coherent data supplied through the Route63 kernel packet.

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

Route53 consumed data supplied through the Route63 kernel packet.

theorem Q2Presentation.Induction.MinimalBlockKernelFrattiniRoute63Closers.groupInvariantRouteData_from_route63 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route53 group/invariant route data supplied through Route63.

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

Group-tower provider using Route63 least/Frattini lowerings.

Public provider

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

Drop-in replacement for minimalBlock_groupTowerData_from_kernelRoute61CombinedClosers, with the five Route62 least/Frattini atoms lowered by Route63 packets.