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

This sidecar is route-neutral: it does not edit the active Route59 files.

Route55 still exposes the least/Frattini part of the kernel/raw frontier through the Route26 upper-candidate leastness shortcut and the field-level Frattini leaves. This file keeps the same manuscript tower shape, but narrows that surface as follows:

• the least kernel is selected by the genuine least-over-chief packet, avoiding the Route26 minimalBlock_kernelLeastUniversalData leaf for the fixed upper candidate;
• nonidentity of Phi(K) is recovered theorem-level from cardinal nontriviality;
• the three remaining Lemma 7.2 conclusions are exposed as lower proof-step packets: centralizer collapse, fourth-power map vanishing, and elementary Frattini layer;
• the raw head nonzero witness is recovered from same-tower head nontriviality, avoiding minimalBlock_kernelModuleConcreteHeadNonzeroData.

The public provider at the bottom has the Route55 target shape, so it can feed a future Route60 replacement without changing downstream consumers.

Least kernel selection

def Q2Presentation.Induction.MinimalBlockKernelRoute60FrattiniClosers.leastCandidateOfLeastOverChief {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : MinimalBlockKernelCandidateData chief

Forget a least-over-chief packet to its candidate part.

Equations

• Q2Presentation.Induction.MinimalBlockKernelRoute60FrattiniClosers.leastCandidateOfLeastOverChief K = K.toMinimalBlockKernelCandidateData

def Q2Presentation.Induction.MinimalBlockKernelRoute60FrattiniClosers.leastUniversalDataOfLeastOverChief {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : MinimalBlockKernelLeastUniversalData (leastCandidateOfLeastOverChief K)

The universal leastness field, recovered theorem-level from a selected least-over-chief packet.

This does not prove leastness for Route26's fixed upper candidate; it records the universal property for the actual selected least kernel.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.MinimalBlockKernelRoute60FrattiniClosers.leastOverChiefData_from_route60 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelLeastOverChiefData chief)

Route60 selects the manuscript least-over-chief kernel directly.

The axiom closure uses the genuine minimalBlock_kernelLeastOverChiefData packet and avoids Route26's minimalBlock_kernelLeastUniversalData leaf.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute60FrattiniClosers.selectedLeastUniversalData_from_route60 {p : FramedPair} (chief : NonScalarChiefFactor p) : ∃ (K : MinimalBlockKernelCandidateData chief), Nonempty (MinimalBlockKernelLeastUniversalData K)

Existential least-universal provider for the selected Route60 least kernel.

Frattini-collapse proof-step packets

def Q2Presentation.Induction.MinimalBlockKernelRoute60FrattiniClosers.frattiniNormalData_from_route60 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : MinimalBlockKernelModuleConcreteFrattiniNormalData K

The normality of the literal Frattini subgroup is theorem-level from normality of the selected K.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelRoute60FrattiniClosers.frattiniNonidentityDataOfNontrivial {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (C : MinimalBlockKernelModuleConcreteFrattiniNontrivialData K) : MinimalBlockKernelModuleConcreteFrattiniNonidentityData K

Convert cardinal nontriviality of Phi(K) into a concrete nonidentity witness.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.MinimalBlockKernelRoute60FrattiniClosers.frattiniNonidentityData_from_route60Nontrivial {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniNonidentityData K)

Route60 nonidentity provider from the already split cardinal nontriviality packet.

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

Lemma 7.2 centralizer-collapse step: K centralizes its Frattini subgroup.

The field is stated in centralizer orientation; the adapter below flips the equality to the current concrete packet orientation.

• K_centralizes_frattini (k : p.fst.Y) : k ∈ K.Ksub → ∀ r ∈ Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub), k * r = r * k

axiom Q2Presentation.Induction.MinimalBlockKernelRoute60FrattiniClosers.frattiniCentralizerStepData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniCentralizerStepData K)

Residual proof-step packet for the centralizer part of Lemma 7.2.

def Q2Presentation.Induction.MinimalBlockKernelRoute60FrattiniClosers.frattiniCentralDataOfCentralizerStep {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (C : FrattiniCentralizerStepData K) : MinimalBlockKernelModuleConcreteFrattiniCentralData K

Current centrality packet recovered from the Route60 centralizer step.

Equations

• ⋯ = ⋯

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

Route60 provider for the current Frattini-centrality packet.

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

Lemma 7.2 fourth-power-map step: the equivariant map k ↦ k^4 vanishes.

• fourth_power_vanishes (k : p.fst.Y) : k ∈ K.Ksub → k ^ 4 = 1

axiom Q2Presentation.Induction.MinimalBlockKernelRoute60FrattiniClosers.fourthPowerMapVanishesData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FourthPowerMapVanishesData K)

Residual proof-step packet for fourth-power vanishing in Lemma 7.2.

def Q2Presentation.Induction.MinimalBlockKernelRoute60FrattiniClosers.fourthPowerDataOfMapVanishes {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (P4 : FourthPowerMapVanishesData K) : MinimalBlockKernelModuleConcreteFourthPowerData K

Current fourth-power packet recovered from the Route60 proof-step packet.

Equations

• ⋯ = ⋯

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

Route60 provider for the current fourth-power packet.

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

Final Lemma 7.2 elementary-layer step: Phi(K) has exponent two.

• frattini_square_eq_one (r : p.fst.Y) : r ∈ Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub) → r ^ 2 = 1

axiom Q2Presentation.Induction.MinimalBlockKernelRoute60FrattiniClosers.frattiniElementaryLayerData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniElementaryLayerData K)

Residual proof-step packet for the elementary Frattini layer.

def Q2Presentation.Induction.MinimalBlockKernelRoute60FrattiniClosers.frattiniExponentDataOfElementaryLayer {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (E : FrattiniElementaryLayerData K) : MinimalBlockKernelModuleConcreteFrattiniExponentData K

Current exponent-two packet recovered from the Route60 proof-step packet.

Equations

• ⋯ = ⋯

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

Route60 provider for the current exponent-two packet.

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

Concrete Frattini packet assembled from Route60's least/Frattini closers.

Head nonzero from same-tower head nontriviality

def Q2Presentation.Induction.MinimalBlockKernelRoute60FrattiniClosers.headNonzeroDataOfHeadData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} {D : MinimalBlockKernelModuleConcreteRawData K F} (H : MinimalBlockKernelModuleConcreteHeadData D) : MinimalBlockKernelModuleConcreteHeadNonzeroData D

Convert the same-tower nontrivial-head packet into the explicit nonzero coset witness used by the older concrete interface.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.MinimalBlockKernelRoute60FrattiniClosers.headNonzeroData_from_route60HeadData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : MinimalBlockKernelModuleConcreteRawData K F) : Nonempty (MinimalBlockKernelModuleConcreteHeadNonzeroData D)

Route60 provider for the explicit head-nonzero packet, avoiding the independent minimalBlock_kernelModuleConcreteHeadNonzeroData axiom.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute60FrattiniClosers.rawQuotientTowerData_from_route60Transport {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelRawQuotientTowerData K F)

Raw quotient tower assembled through Route60's same-tower head provider.

Route55-shaped packet and group-tower provider

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

Route55 packet assembled through Route60's least/Frattini/head closers.

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

Route54 coherent data supplied through Route60's Route55-shaped packet.

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

Route53 consumed data supplied through Route60.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute60FrattiniClosers.groupInvariantRouteData_from_route60 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route53 group/invariant route data supplied through Route60.

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

Route60 group tower through the least/Frattini/head closers in this file.

Public Route60 kernel provider

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

Route60 kernel provider for future integration.

Compared with Route55, this provider removes the target least/head leaves minimalBlock_kernelLeastUniversalData and minimalBlock_kernelModuleConcreteHeadNonzeroData, and replaces the target Frattini field leaves by the lower proof-step packets in this sidecar.