Route194 Section 7 kernel closers for the Route192 frontier #

This sidecar keeps the Route192 candidate/target route compact and attacks only the Section 7 kernel/provenance frontier.

The two raw R, M, T, C tower packets remain the compact Route167 atoms. The five selected Route78 least/Frattini packets are replaced by the Route67 Lemma 7.2 packets already used by the Route189 diagnostic:

coherent least-kernel selection;
internal nonidentity in Phi(K);
Hall-commutator centralizer collapse;
fourth-power commutator-kernel collapse;
square/commutator Frattini-layer exponent packet.

Route78-facing wrappers through Route67 Lemma 7.2 data #

source

theorem Q2Presentation.Induction.Section7KernelRoute194Closers.leastKernelSelectedData_from_route194Kernel {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockKernelRoute78FrattiniClosers.LeastKernelSelectedData chief)

Route194 replacement for the compact Route78 selected least-kernel packet.

source

theorem Q2Presentation.Induction.Section7KernelRoute194Closers.leastOverChiefData_from_route194Kernel {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockKernelLeastOverChiefData chief)

Route-ready least-over-chief packet for Route194.

source

theorem Q2Presentation.Induction.Section7KernelRoute194Closers.frattiniInternalSelectedData_from_route194Kernel {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FrattiniInternalSelectedData K)

Route194 replacement for the compact Route78 internal Frattini witness.

source

theorem Q2Presentation.Induction.Section7KernelRoute194Closers.frattiniCentralizerSelectedData_from_route194Kernel {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FrattiniCentralizerSelectedData K)

Route194 replacement for the compact Route78 Frattini-centralizer packet.

source

theorem Q2Presentation.Induction.Section7KernelRoute194Closers.fourthPowerKernelSelectedData_from_route194Kernel {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FourthPowerKernelSelectedData K)

Route194 replacement for the compact Route78 fourth-power packet.

source

theorem Q2Presentation.Induction.Section7KernelRoute194Closers.frattiniSquareCommutatorLiteralExponentData_from_route194Kernel {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FrattiniSquareCommutatorLiteralExponentData K)

Route194 replacement for the compact Route78 literal exponent packet.

source

theorem Q2Presentation.Induction.Section7KernelRoute194Closers.frattiniData_from_route194Kernel {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) :

Nonempty (MinimalBlockKernelModuleConcreteFrattiniData K)

Concrete Frattini packet for the Route194 kernel provider.

Kernel provider with compact Route167 raw tower retained #

source

theorem Q2Presentation.Induction.Section7KernelRoute194Closers.kernelRoute194ModuleLayerData_from_section7KernelRoute194Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (Section7KernelRoute167Closers.KernelRoute167ModuleLayerData chief)

Route194 module-layer packet: Route67 Lemma 7.2 Frattini data plus the compact Route167 same-tower raw quotient and simple-head packets.

source

theorem Q2Presentation.Induction.Section7KernelRoute194Closers.minimalBlock_kernelModuleConcreteProvenanceData_from_section7KernelRoute194Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Concrete kernel/module provenance through Route194.

source

theorem Q2Presentation.Induction.Section7KernelRoute194Closers.minimalBlock_lowerGroupModuleData_from_section7KernelRoute194Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockLowerGroupModuleData chief)

Lower group/module data through Route194.

source

theorem Q2Presentation.Induction.Section7KernelRoute194Closers.minimalBlock_groupTowerData_from_section7KernelRoute194Closers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockGroupTowerData p chief)

Drop-in Route194 Section 7 kernel provider.