Route212 Frattini sidecar for the Section 7 kernel cluster

This file is route-neutral: it does not edit the current Route212 integrated proof. It gives a drop-in Section 7 kernel provider whose least-kernel and Frattini-collapse side avoids the Route199 field-level atoms by reusing the existing coherent least-kernel packet and the Route67 Lemma 7.2 packets. The raw quotient/simple-head side remains the current Route199 raw/head lowering.

Least kernel and Frattini collapse without Route199 field atoms

theorem Q2Presentation.Induction.MinimalBlockKernelRoute212FrattiniClosers.leastOverChiefData_from_route212Frattini {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelLeastOverChiefData chief)

Route212 least-over-chief provider through the existing coherent kernel choice API.

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

Route67-shaped least-kernel packet obtained from the coherent least-over-chief provider.

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

Route212 internal Frattini nonidentity provider through the existing Route67 packet.

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

Route212 Frattini nontriviality from the Route67 internal witness.

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

Route212 centralizer-collapse packet through the existing Route67 Hall-commutator provider.

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

Route212 centralizer proof-step obtained from the Route67 Hall-commutator packet.

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

Route212 concrete Frattini-centrality packet.

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

Route212 fourth-power kernel packet through the existing Route67 commutator-normal-closure provider.

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

Route212 fourth-power proof-step obtained from the Route67 packet.

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

Route212 concrete fourth-power packet.

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

Route212 square/commutator layer packet through the existing Route67 Frattini-layer provider.

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

Route212 elementary Frattini-layer proof-step obtained from the Route67 square/commutator layer together with the two collapse steps.

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

Route212 concrete exponent-two packet for the literal Frattini subgroup.

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

Concrete Frattini packet assembled without using the Route199 Frattini field atoms.

structure Q2Presentation.Induction.MinimalBlockKernelRoute212FrattiniClosers.LeastFrattiniData {p : FramedPair} (chief : NonScalarChiefFactor p) : Type

Coherent least-kernel plus Frattini-collapse packet for Route212.

• least : MinimalBlockKernelLeastOverChiefData chief
• frattini : MinimalBlockKernelModuleConcreteFrattiniData self.least

theorem Q2Presentation.Induction.MinimalBlockKernelRoute212FrattiniClosers.leastFrattiniData_from_route212Frattini {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (LeastFrattiniData chief)

Route212 coherent least/Frattini packet.

structure Q2Presentation.Induction.Section7KernelRoute212FrattiniClosers.KernelRoute212FrattiniLayerData {p : FramedPair} (chief : NonScalarChiefFactor p) : Type 1

Route212 module-layer packet: Route212 Frattini data plus the current Route199 raw/head lowering.

• least : MinimalBlockKernelLeastOverChiefData chief
• frattini : MinimalBlockKernelModuleConcreteFrattiniData self.least
• rawTower : MinimalBlockKernelRawQuotientTowerData self.least ⋯
• rawSimple : MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData self.rawTower.rawData.rawTowerData

def Q2Presentation.Induction.Section7KernelRoute212FrattiniClosers.KernelRoute212FrattiniLayerData.concreteProvenanceData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute212FrattiniLayerData chief) : MinimalBlockKernelModuleConcreteProvenanceData chief

Forget the Route212 module-layer packet to concrete kernel provenance.

Equations

• D.concreteProvenanceData = Q2Presentation.Induction.Section7KernelRoute167Closers.concreteProvenanceDataOfRawQuotientTower D.least ⋯ D.rawTower

def Q2Presentation.Induction.Section7KernelRoute212FrattiniClosers.KernelRoute212FrattiniLayerData.lowerGroupModuleData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute212FrattiniLayerData chief) : MinimalBlockLowerGroupModuleData chief

Lower group/module data selected by the Route212 packet.

Equations

• D.lowerGroupModuleData = Q2Presentation.Induction.minimalBlock_lowerFromConcreteProvenance D.concreteProvenanceData

def Q2Presentation.Induction.Section7KernelRoute212FrattiniClosers.KernelRoute212FrattiniLayerData.invariantActualData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute212FrattiniLayerData chief) : MinimalBlockInvariantActualProofs2Data D.lowerGroupModuleData.rawTowerData

Same-tower invariant packet from the Route199 raw simple-head semantics.

Equations

• D.invariantActualData = id (Q2Presentation.Induction.MinimalBlockInvariantRoute112Closers.invariantActualProofs2Data_of_rawSimpleHeadSemanticData ⋯)

def Q2Presentation.Induction.Section7KernelRoute212FrattiniClosers.KernelRoute212FrattiniLayerData.groupTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : KernelRoute212FrattiniLayerData chief) : MinimalBlockGroupTowerData p chief

The group tower consumed by the Section 7 Fourier branch.

Equations

• D.groupTowerData = D.lowerGroupModuleData.groupTowerData ⋯ ⋯

theorem Q2Presentation.Induction.Section7KernelRoute212FrattiniClosers.kernelRoute212FrattiniLayerData_from_section7KernelRoute212FrattiniClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (KernelRoute212FrattiniLayerData chief)

Route212 module-layer packet through the Route212 Frattini sidecar and the current Route199 raw/head lowering.

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

Drop-in Section 7 kernel provider for a future Route212 replay.