Route67 combined kernel provider

This sidecar leaves Route66 and the promoted theorem untouched. It gives a drop-in replacement for minimalBlock_groupTowerData_from_kernelRoute66CombinedClosers, but avoids the six Route66 least/Frattini residual atoms by routing through sharper manuscript-shaped packets:

• a coherent least-kernel selection packet for the single selected K;
• an internal nonidentity witness in Phi(K);
• the Hall-commutator centralizer packet from Lemma 7.2;
• the fourth-power kernel packet with the commutator-normal-closure image;
• the square/commutator layer packet giving the exponent-two Frattini conclusion after the centralizer and fourth-power collapses.

Least kernel selection

structure Q2Presentation.Induction.MinimalBlockKernelRoute67FrattiniClosers.LeastKernelSelectionData {p : FramedPair} (chief : NonScalarChiefFactor p) : Type

Route67 coherent least-kernel packet.

This matches the manuscript's "choose K minimal subject to K S = P" step and keeps the candidate and universal leastness fields attached to the same object.

• least : MinimalBlockKernelLeastOverChiefData chief

axiom Q2Presentation.Induction.MinimalBlockKernelRoute67FrattiniClosers.leastKernelSelectionData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (LeastKernelSelectionData chief)

Residual Route67 least-kernel selection packet.

def Q2Presentation.Induction.MinimalBlockKernelRoute67FrattiniClosers.candidateOfLeastSelection {p : FramedPair} {chief : NonScalarChiefFactor p} (L : LeastKernelSelectionData chief) : MinimalBlockKernelCandidateData chief

Candidate part of the selected Route67 least kernel.

Equations

• Q2Presentation.Induction.MinimalBlockKernelRoute67FrattiniClosers.candidateOfLeastSelection L = L.least.toMinimalBlockKernelCandidateData

def Q2Presentation.Induction.MinimalBlockKernelRoute67FrattiniClosers.universalOfLeastSelection {p : FramedPair} {chief : NonScalarChiefFactor p} (L : LeastKernelSelectionData chief) : MinimalBlockKernelLeastUniversalData (candidateOfLeastSelection L)

Universal leastness for the selected Route67 least kernel.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.MinimalBlockKernelRoute67FrattiniClosers.leastOverChiefData_from_route67 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelLeastOverChiefData chief)

Route67 least-over-chief packet from the coherent least-kernel selection.

Frattini nonidentity

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

Internal witness-form nontriviality of the literal Frattini subgroup.

• r : ↥K.Ksub
• r_mem_frattini : self.r ∈ frattini ↥K.Ksub
• r_ne_one : ↑self.r ≠ 1

axiom Q2Presentation.Induction.MinimalBlockKernelRoute67FrattiniClosers.frattiniInternalNonidentityData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniInternalNonidentityData K)

Residual Route67 internal nonidentity witness for Phi(K).

def Q2Presentation.Induction.MinimalBlockKernelRoute67FrattiniClosers.frattiniNonidentityDataOfInternal {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (W : FrattiniInternalNonidentityData K) : MinimalBlockKernelModuleConcreteFrattiniNonidentityData K

Convert an internal Frattini witness to the ambient witness packet used by the current concrete Frattini interface.

Equations

• ⋯ = ⋯

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

Route67 Frattini nontriviality from an internal nonidentity witness.

Centralizer-collapse step

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

Route67 Hall-commutator packet for the centralizer part of Lemma 7.2.

The manuscript proves that the commutator subgroup generated by the odd Hall action maps onto the chosen chief factor and lies in the centralizer of Phi(K). This packet records exactly the data needed to make the centralizer itself a candidate to which leastness applies.

• 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
• commutatorSub : Subgroup p.fst.Y
• commutatorSub_le_centralizer : self.commutatorSub ≤ self.centralizerSub
• commutatorSub_sup_lower : self.commutatorSub ⊔ chief.lower = chief.upper

axiom Q2Presentation.Induction.MinimalBlockKernelRoute67FrattiniClosers.frattiniCentralizerHallCommutatorData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniCentralizerHallCommutatorData K)

Residual Route67 Hall-commutator centralizer packet.

def Q2Presentation.Induction.MinimalBlockKernelRoute67FrattiniClosers.frattiniCentralizerCandidateDataOfHallCommutator {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (D : FrattiniCentralizerHallCommutatorData K) : MinimalBlockKernelFrattiniRoute63Closers.FrattiniCentralizerCandidateData K

The centralizer candidate required by Route63 follows from the Hall-commutator packet.

Equations

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

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

Route67 centralizer step from the Hall-commutator packet.

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

Concrete centrality packet from the Route67 centralizer step.

Fourth-power step

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

Route67 packet for the fourth-power map step in Lemma 7.2.

The map k ↦ k^4 vanishes on the normal closure of the odd-Hall commutators; that closure still maps onto the selected chief factor, so the kernel of the fourth-power map is a leastness candidate.

• 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
• commutatorSub : Subgroup p.fst.Y
• commutatorSub_le_fourthKernel : self.commutatorSub ≤ self.fourthKernel
• commutatorSub_sup_lower : self.commutatorSub ⊔ chief.lower = chief.upper

axiom Q2Presentation.Induction.MinimalBlockKernelRoute67FrattiniClosers.fourthPowerKernelCommutatorData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FourthPowerKernelCommutatorData K)

Residual Route67 fourth-power kernel/commutator packet.

def Q2Presentation.Induction.MinimalBlockKernelRoute67FrattiniClosers.fourthPowerKernelCandidateDataOfCommutator {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (D : FourthPowerKernelCommutatorData K) : MinimalBlockKernelFrattiniRoute63Closers.FourthPowerKernelCandidateData K

The Route63 fourth-power kernel candidate follows from the kernel/commutator packet.

Equations

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

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

Route67 fourth-power vanishing from the kernel/commutator packet.

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

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

Elementary Frattini layer

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

Route67 square/commutator generation packet for the final elementary-layer part of Lemma 7.2.

This isolates the manuscript identity Phi(K) = K^2 [K,K]: after the centralizer and fourth-power collapses, the square/commutator layer has exponent two and contains the literal Frattini subgroup.

• squareCommutatorLayer : Subgroup p.fst.Y
• frattini_le_squareCommutatorLayer : Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub) ≤ self.squareCommutatorLayer
• squareCommutatorLayer_square_eq_one_of_collapse : MinimalBlockKernelRoute60FrattiniClosers.FrattiniCentralizerStepData K → MinimalBlockKernelRoute60FrattiniClosers.FourthPowerMapVanishesData K → ∀ r ∈ self.squareCommutatorLayer, r ^ 2 = 1

axiom Q2Presentation.Induction.MinimalBlockKernelRoute67FrattiniClosers.frattiniSquareCommutatorLayerData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (FrattiniSquareCommutatorLayerData K)

Residual Route67 square/commutator layer packet.

def Q2Presentation.Induction.MinimalBlockKernelRoute67FrattiniClosers.frattiniElementaryLayerFromSquareCommutator {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (E : FrattiniSquareCommutatorLayerData K) : MinimalBlockKernelFrattiniRoute63Closers.FrattiniElementaryLayerFromCollapseData K

The Route63 elementary-layer implication follows from the square/commutator layer packet.

Equations

• ⋯ = ⋯

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

Route67 elementary Frattini layer from the square/commutator packet.

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

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

Frattini packet

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

Concrete Frattini packet assembled through the Route67 lowerings.

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

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

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

Route54 coherent data supplied through the Route67 kernel packet.

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

Route53 consumed data supplied through Route67.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute67CombinedClosers.groupInvariantRouteData_from_route67 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route53 group/invariant route data supplied through Route67.

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

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

Public provider

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

Drop-in replacement for minimalBlock_groupTowerData_from_kernelRoute66CombinedClosers, with the six Route66 least/Frattini atoms replaced by Route67 lower packets.