Route189 Lemma 7.2 kernel closers

This sidecar keeps Route187 and Route188 untouched. It narrows the Route188 Lemma 7.2 slice by replacing the six Route164 residual names with the existing Route67 manuscript packets:

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

The raw R, M, T, C tower remains the Route188/Route183 Route43 lowering.

Least kernel via the coherent Route67 selection

theorem Q2Presentation.Induction.Section7KernelRoute189Lemma72Closers.leastKernelSelectedData_from_route189Lemma72 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelRoute78FrattiniClosers.LeastKernelSelectedData chief)

Route189 selected least-kernel packet. This replaces the Route164 candidate/universal pair by the existing coherent Route67 least selection.

theorem Q2Presentation.Induction.Section7KernelRoute189Lemma72Closers.leastOverChiefData_from_route189Lemma72 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelLeastOverChiefData chief)

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

Internal Frattini witness

theorem Q2Presentation.Induction.Section7KernelRoute189Lemma72Closers.frattiniNonidentityData_from_route189Lemma72 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (Section7KernelRoute164Closers.FrattiniNonidentityData K)

Route164-shaped ambient nonidentity witness, derived from Route67's internal witness in frattini K.

theorem Q2Presentation.Induction.Section7KernelRoute189Lemma72Closers.frattiniInternalSelectedData_from_route189Lemma72 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FrattiniInternalSelectedData K)

Route78-shaped selected internal-Frattini witness through Route189.

Centralizer-collapse step

theorem Q2Presentation.Induction.Section7KernelRoute189Lemma72Closers.frattiniCentralizerStepData_from_route189Lemma72 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (Section7KernelRoute164Closers.FrattiniCentralizerStepData K)

Route164-shaped centralizer step, derived from the Route67 Hall-commutator centralizer packet by the existing leastness argument.

theorem Q2Presentation.Induction.Section7KernelRoute189Lemma72Closers.frattiniCentralizerSelectedData_from_route189Lemma72 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FrattiniCentralizerSelectedData K)

Route78-shaped selected centralizer packet through the Route67 Hall-commutator data.

Fourth-power collapse

theorem Q2Presentation.Induction.Section7KernelRoute189Lemma72Closers.fourthPowerMapVanishesData_from_route189Lemma72 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (Section7KernelRoute164Closers.FourthPowerMapVanishesData K)

Route164-shaped fourth-power step, derived from the Route67 commutator-kernel packet by the existing leastness argument.

theorem Q2Presentation.Induction.Section7KernelRoute189Lemma72Closers.fourthPowerKernelSelectedData_from_route189Lemma72 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FourthPowerKernelSelectedData K)

Route78-shaped selected fourth-power packet through the Route67 commutator-kernel data.

Elementary Frattini layer

theorem Q2Presentation.Induction.Section7KernelRoute189Lemma72Closers.frattiniSquareCommutatorLiteralExponentData_from_route189Lemma72 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelRoute78FrattiniClosers.FrattiniSquareCommutatorLiteralExponentData K)

Route78-shaped literal exponent packet through the Route67 square/commutator layer.

theorem Q2Presentation.Induction.Section7KernelRoute189Lemma72Closers.frattiniElementaryLayerData_from_route189Lemma72 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (Section7KernelRoute164Closers.FrattiniElementaryLayerData K)

Route164-shaped elementary Frattini layer through the Route67 square/commutator packet.

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

Concrete Frattini packet for the Route189 kernel provider.

Drop-in kernel provider

theorem Q2Presentation.Induction.Section7KernelRoute189Lemma72Closers.kernelRoute189ModuleLayerData_from_section7KernelRoute189Lemma72Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (Section7KernelRoute183Closers.KernelRoute183ModuleLayerData chief)

Route189 module-layer packet with Route67 Lemma 7.2 data and the Route188 Route43 raw tower.

theorem Q2Presentation.Induction.Section7KernelRoute189Lemma72Closers.minimalBlock_kernelModuleConcreteProvenanceData_from_section7KernelRoute189Lemma72Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Concrete kernel/module provenance through Route189.

theorem Q2Presentation.Induction.Section7KernelRoute189Lemma72Closers.minimalBlock_lowerGroupModuleData_from_section7KernelRoute189Lemma72Closers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockLowerGroupModuleData chief)

Lower group/module data through Route189.

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

Drop-in Route189 Section 7 kernel provider.