Route74 selected Frattini closers for the minimal-block kernel

Route72 split the Route67 least/Frattini packets into ten smaller fields. Some of those fields are intentionally dependent on the selected object, but their axiom statements quantify over arbitrary candidates/cores. This sidecar keeps the Route72 decomposition available while avoiding those ten Route72 atoms in the exported provider:

• least-kernel and Frattini-nonidentity data are carried as selected coherent packets, then projected to the Route72 field shapes;
• the centralizer and fourth-power packets are projected from the Route67 Hall-commutator packets as selected core + image data;
• the final square/commutator containment is closed theorem-level by choosing the literal Phi(K) layer, with the exponent-two implication supplied by the Route63 elementary-collapse packet.

The public theorem has the same target as minimalBlock_groupTowerData_from_kernelRoute72FrattiniClosers.

Least kernel selection

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

Route74 selected least-kernel packet.

This is the manuscript-shaped dependent version of the Route72 candidate plus universal data: the universal property is attached to the candidate actually chosen.

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

def Q2Presentation.Induction.MinimalBlockKernelRoute74FrattiniClosers.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 := ⋯ }

def Q2Presentation.Induction.MinimalBlockKernelRoute74FrattiniClosers.leastKernelSelectedDataOfRoute67 {p : FramedPair} {chief : NonScalarChiefFactor p} (L : MinimalBlockKernelRoute67FrattiniClosers.LeastKernelSelectionData chief) : LeastKernelSelectedData chief

Project Route67's coherent least selection to Route74's selected packet.

Equations

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

theorem Q2Presentation.Induction.MinimalBlockKernelRoute74FrattiniClosers.leastKernelSelectedData_from_route74 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (LeastKernelSelectedData chief)

Route74 selected least-kernel data, projected from the Route67 coherent selection packet.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute74FrattiniClosers.leastKernelSelectedCandidateData_from_route74 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelCandidateData chief)

Candidate projection for the selected Route74 least kernel.

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

Universal leastness projection for the selected Route74 candidate.

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

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

theorem Q2Presentation.Induction.MinimalBlockKernelRoute74FrattiniClosers.leastOverChiefData_from_route74 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelLeastOverChiefData chief)

Route74 least-over-chief packet.

Frattini nonidentity

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

Route74 selected internal Frattini element and its nontriviality.

This keeps the nontriviality proof attached to the element that was selected, instead of asking for nontriviality of every possible internal element.

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

def Q2Presentation.Induction.MinimalBlockKernelRoute74FrattiniClosers.frattiniInternalSelectedDataOfRoute67 {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (W : MinimalBlockKernelRoute67FrattiniClosers.FrattiniInternalNonidentityData K) : FrattiniInternalSelectedData K

Project Route67's internal nonidentity witness to Route74's selected split element/nontriviality data.

Equations

• Q2Presentation.Induction.MinimalBlockKernelRoute74FrattiniClosers.frattiniInternalSelectedDataOfRoute67 W = { element := { r := W.r, r_mem_frattini := ⋯ }, nontrivial := ⋯ }

theorem Q2Presentation.Induction.MinimalBlockKernelRoute74FrattiniClosers.frattiniInternalSelectedData_from_route74 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniInternalSelectedData K)

Route74 selected internal Frattini witness.

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

Route67 internal nonidentity packet recovered from Route74 selected data.

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

Route74 Frattini nontriviality from the selected internal witness.

Centralizer-collapse step

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

Route74 selected centralizer core plus Hall-image data.

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

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

Project Route67's Hall-commutator packet to the Route72 selected core and image shape.

Equations

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

theorem Q2Presentation.Induction.MinimalBlockKernelRoute74FrattiniClosers.frattiniCentralizerSelectedData_from_route74 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniCentralizerSelectedData K)

Route74 selected centralizer core/image data.

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

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

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

Route74 centralizer step.

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

Concrete centrality packet from the Route74 centralizer step.

Fourth-power step

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

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

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

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

Project Route67's fourth-power commutator packet to the Route72 selected core and image shape.

Equations

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

theorem Q2Presentation.Induction.MinimalBlockKernelRoute74FrattiniClosers.fourthPowerKernelSelectedData_from_route74 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FourthPowerKernelSelectedData K)

Route74 selected fourth-power core/image data.

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

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

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

Route74 fourth-power vanishing.

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

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

Elementary Frattini layer

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

Route74 selected square/commutator layer data.

The selected layer is allowed to be the literal Phi(K) layer. This closes the Route72 containment field by reflexivity and leaves only the manuscript collapse implication that Phi(K) has exponent two after the centralizer and fourth-power steps.

• containment : MinimalBlockKernelRoute72FrattiniClosers.FrattiniSquareCommutatorContainmentData K
• exponent : MinimalBlockKernelRoute72FrattiniClosers.FrattiniSquareCommutatorExponentData self.containment

def Q2Presentation.Induction.MinimalBlockKernelRoute74FrattiniClosers.frattiniSquareCommutatorSelectedDataOfElementary {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (E : MinimalBlockKernelFrattiniRoute63Closers.FrattiniElementaryLayerFromCollapseData K) : FrattiniSquareCommutatorSelectedData K

Choose the literal Phi(K) layer and use the Route63 elementary-collapse implication for its exponent-two conclusion.

Equations

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

theorem Q2Presentation.Induction.MinimalBlockKernelRoute74FrattiniClosers.frattiniSquareCommutatorSelectedData_from_route74 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniSquareCommutatorSelectedData K)

Route74 selected square/commutator data, with theorem-level containment.

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

Route67 square/commutator layer packet recovered from Route74 selected data.

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

Route74 elementary Frattini layer from the selected square/commutator data.

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

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

Frattini packet

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

Concrete Frattini packet assembled through the Route74 selected lowerings.

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

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

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

Route54 coherent data supplied through the Route74 kernel packet.

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

Route53 consumed data supplied through Route74.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute74CombinedClosers.groupInvariantRouteData_from_route74 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route53 group/invariant route data supplied through Route74.

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

Group-tower provider using Route74 selected least/Frattini lowerings.

Public provider

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

Drop-in replacement for minimalBlock_groupTowerData_from_kernelRoute72FrattiniClosers, with the ten Route72 Frattini atoms avoided by selected Route74 packets and theorem-level projections.