Route78 Frattini closers for the minimal-block kernel

Route77 exposes the minimal-block least/Frattini frontier through the ten Route72 split atoms. This sidecar keeps Route76's raw-head refinements, but replaces the Route72 least/Frattini surface by selected manuscript-shaped packets:

• the least kernel is selected once, with its universal property attached to that selected candidate;
• the Frattini nonidentity witness is selected once, with nontriviality attached to that same element;
• the centralizer and fourth-power collapse steps use selected core plus Hall-image packets, avoiding the Route72 requirement to prove Hall-image data for every possible core;
• the square/commutator containment is closed by choosing the literal embedded Phi(K) layer, leaving only the exponent-two implication from the collapse steps.

The public provider at the bottom is a drop-in group-tower provider with the same target shape as minimalBlock_groupTowerData_from_kernelRoute76RawClosers.

Least kernel selection

structure Q2Presentation.Induction.MinimalBlockKernelRoute78FrattiniClosers.LeastKernelSelectedData {p : FramedPair} (chief : NonScalarChiefFactor p) : Type

Route78 selected least-kernel packet.

This is the dependent version of the Route72 candidate/universal split: the universal leastness proof is attached only to the candidate actually selected.

• candidate : MinimalBlockKernelCandidateData chief
• universal : MinimalBlockKernelLeastUniversalData self.candidate

def Q2Presentation.Induction.MinimalBlockKernelRoute78FrattiniClosers.LeastKernelSelectedData.least {p : FramedPair} {chief : NonScalarChiefFactor p} (D : LeastKernelSelectedData chief) : MinimalBlockKernelLeastOverChiefData chief

Forget a selected least-kernel packet to the least-over-chief interface.

Equations

• D.least = { toMinimalBlockKernelCandidateData := D.candidate, minimal_K := ⋯ }

theorem Q2Presentation.Induction.MinimalBlockKernelRoute78FrattiniClosers.leastKernelCandidateData_from_upper {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelCandidateData chief)

The standalone candidate-existence half is theorem-level: P itself is a normal candidate with P S = P. The provider below uses the sharper selected least packet, not this upper candidate.

axiom Q2Presentation.Induction.MinimalBlockKernelRoute78FrattiniClosers.leastKernelSelectedData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (LeastKernelSelectedData chief)

Residual Route78 selected least-kernel data.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute78FrattiniClosers.leastKernelSelectedCandidateData_from_route78 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelCandidateData chief)

Candidate projection for the selected Route78 least kernel.

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

Selected universal leastness projection for Route78.

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

Route67 least-kernel selection packet recovered from Route78 selected data.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute78FrattiniClosers.leastOverChiefData_from_route78 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelLeastOverChiefData chief)

Route78 least-over-chief packet.

Frattini nonidentity

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

Route78 selected internal Frattini element and its nontriviality.

This replaces the Route72 pair consisting of an arbitrary internal element axiom and a nontriviality axiom for every such element.

• element : MinimalBlockKernelRoute72FrattiniClosers.FrattiniInternalElementData K
• nontrivial : MinimalBlockKernelRoute72FrattiniClosers.FrattiniInternalElementNontrivialData self.element

axiom Q2Presentation.Induction.MinimalBlockKernelRoute78FrattiniClosers.frattiniInternalSelectedData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniInternalSelectedData K)

Residual Route78 selected internal Frattini witness.

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

Element projection for the selected Route78 Frattini witness.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute78FrattiniClosers.frattiniInternalElementSelectedNontrivialData_from_route78 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : ∃ (E : MinimalBlockKernelRoute72FrattiniClosers.FrattiniInternalElementData K), Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FrattiniInternalElementNontrivialData E)

Selected nontriviality projection for Route78.

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

Route67 internal nonidentity packet recovered from Route78 selected data.

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

Route78 Frattini nontriviality from the selected internal witness.

Centralizer-collapse step

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

Route78 selected centralizer core plus Hall-image data.

• core : MinimalBlockKernelRoute72FrattiniClosers.FrattiniCentralizerCoreData K
• image : MinimalBlockKernelRoute72FrattiniClosers.FrattiniCentralizerHallImageData self.core

axiom Q2Presentation.Induction.MinimalBlockKernelRoute78FrattiniClosers.frattiniCentralizerSelectedData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniCentralizerSelectedData K)

Residual Route78 selected centralizer core/image packet.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute78FrattiniClosers.frattiniCentralizerSelectedCoreImageData_from_route78 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : ∃ (C : MinimalBlockKernelRoute72FrattiniClosers.FrattiniCentralizerCoreData K), Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FrattiniCentralizerHallImageData C)

Selected core/image projection for Route78 centralizer data.

def Q2Presentation.Induction.MinimalBlockKernelRoute78FrattiniClosers.frattiniCentralizerHallCommutatorDataOfSelected {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (D : FrattiniCentralizerSelectedData K) : MinimalBlockKernelRoute67FrattiniClosers.FrattiniCentralizerHallCommutatorData K

Convert selected Route78 centralizer data to the Route67 Hall-commutator packet.

Equations

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

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

Route67 Hall-commutator centralizer packet recovered from Route78 selected core/image data.

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

Route78 centralizer step.

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

Concrete centrality packet from the Route78 centralizer step.

Fourth-power step

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

Route78 selected fourth-power core plus Hall-image data.

• core : MinimalBlockKernelRoute72FrattiniClosers.FourthPowerKernelCoreData K
• image : MinimalBlockKernelRoute72FrattiniClosers.FourthPowerKernelHallImageData self.core

axiom Q2Presentation.Induction.MinimalBlockKernelRoute78FrattiniClosers.fourthPowerKernelSelectedData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FourthPowerKernelSelectedData K)

Residual Route78 selected fourth-power core/image packet.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute78FrattiniClosers.fourthPowerKernelSelectedCoreImageData_from_route78 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : ∃ (P4 : MinimalBlockKernelRoute72FrattiniClosers.FourthPowerKernelCoreData K), Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FourthPowerKernelHallImageData P4)

Selected core/image projection for Route78 fourth-power data.

def Q2Presentation.Induction.MinimalBlockKernelRoute78FrattiniClosers.fourthPowerKernelCommutatorDataOfSelected {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (D : FourthPowerKernelSelectedData K) : MinimalBlockKernelRoute67FrattiniClosers.FourthPowerKernelCommutatorData K

Convert selected Route78 fourth-power data to the Route67 kernel/commutator packet.

Equations

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

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

Route67 fourth-power kernel/commutator packet recovered from Route78 selected core/image data.

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

Route78 fourth-power vanishing.

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

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

Elementary Frattini layer

def Q2Presentation.Induction.MinimalBlockKernelRoute78FrattiniClosers.literalFrattiniSquareCommutatorContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : MinimalBlockKernelRoute72FrattiniClosers.FrattiniSquareCommutatorContainmentData K

Literal embedded Frattini subgroup used as the Route78 square/commutator layer.

Equations

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

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

The Route72 containment proposition is closed theorem-level by choosing the literal embedded Phi(K) layer.

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

Route78 literal exponent-two implication for the embedded Phi(K) layer after the centralizer and fourth-power collapses.

• 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.MinimalBlockKernelRoute78FrattiniClosers.frattiniSquareCommutatorLiteralExponentData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniSquareCommutatorLiteralExponentData K)

Residual Route78 literal exponent-two packet.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute78FrattiniClosers.frattiniSquareCommutatorSelectedExponentData_from_route78 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : ∃ (L : MinimalBlockKernelRoute72FrattiniClosers.FrattiniSquareCommutatorContainmentData K), Nonempty (MinimalBlockKernelRoute72FrattiniClosers.FrattiniSquareCommutatorExponentData L)

Selected Route72 exponent projection for the literal Route78 containment choice.

def Q2Presentation.Induction.MinimalBlockKernelRoute78FrattiniClosers.frattiniElementaryLayerFromLiteralExponent {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (E : FrattiniSquareCommutatorLiteralExponentData K) : MinimalBlockKernelFrattiniRoute63Closers.FrattiniElementaryLayerFromCollapseData K

Convert the literal exponent packet to the Route63 elementary-collapse shape.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelRoute78FrattiniClosers.frattiniSquareCommutatorLayerDataOfLiteralExponent {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (E : FrattiniSquareCommutatorLiteralExponentData K) : MinimalBlockKernelRoute67FrattiniClosers.FrattiniSquareCommutatorLayerData K

Convert the literal exponent packet to the Route67 square/commutator layer shape.

Equations

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

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

Route67 square/commutator layer packet recovered from Route78 literal exponent data.

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

Route78 elementary Frattini layer from the literal square/commutator data.

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

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

Frattini packet

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

Concrete Frattini packet assembled through Route78 lowerings.

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

Route55-shaped packet using Route78 least/Frattini lowerings and Route76 raw head/lower-character refinements.

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

Route54 coherent data supplied through Route78.

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

Route53 consumed data supplied through Route78.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute78CombinedClosers.groupInvariantRouteData_from_route78 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route53 group/invariant route data supplied through Route78.

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

Group-tower provider using Route78 Frattini split data and Route76 raw head/lower-character refinements.

Public provider

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

Drop-in replacement for minimalBlock_groupTowerData_from_kernelRoute76RawClosers, with the Route77 least/Frattini frontier lowered from the ten Route72 atoms to selected Route78 packets.