Route106 kernel Frattini/raw-module closers

This sidecar is isolated from the integrated route files. It targets the Route106 concrete Section 7 Frattini/raw-module subcluster exposed through MinimalBlockKernelConcreteRoute45.kernelModuleConcreteProvenanceData_from_route45.

The replacement keeps the manuscript tower coherent:

• choose the least normal K <= P with K S = P;
• use one Frattini--centralizer collapse packet for R = Phi(K);
• use one raw quotient tower packet for R, M = K/R, T, C, the induced actions, the K/R ~= M bridge, and the nonzero head.

Thus the route-ready provider below has the same consumer shape as the Route103 kernel provider, but its closure no longer contains the eleven independent concrete Frattini/raw-module leaves singled out in Route106.

Coherent Section 7 packets

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

Frattini data for the selected K, projected from the coherent manuscript lem:collapse packet rather than the independent concrete Frattini leaves.

theorem Q2Presentation.Induction.MinimalBlockKernelRoute106FrattiniClosers.rawQuotientTowerData_from_route106Coherent {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelRawQuotientTowerData K F)

Raw quotient tower for the selected K and Phi(K), kept as one same-tower manuscript packet.

Route45-shaped concrete provenance replacement

theorem Q2Presentation.Induction.MinimalBlockKernelRoute106FrattiniClosers.kernelModuleConcreteProvenanceData_from_route106FrattiniClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Concrete provenance through the Route106 coherent Frattini/raw route.

This is a replacement for MinimalBlockKernelConcreteRoute45.kernelModuleConcreteProvenanceData_from_route45 when the goal is to remove the eleven independent concrete Frattini/raw-module leaves from the Route106 kernel closure.

Route103-shaped provider

theorem Q2Presentation.Induction.MinimalBlockKernelRoute106FrattiniClosers.lowerGroupModuleData_from_route106FrattiniClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockLowerGroupModuleData chief)

Lower group/module data through the coherent Route106 Frattini/raw route.

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

Route106 kernel group-tower provider with the concrete Frattini/raw-module subcluster replaced by coherent same-tower manuscript packets.

Public aliases

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

Public concrete-provenance alias for the Route106 Frattini/raw-module closer.

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

Public lower-tower alias for the Route106 Frattini/raw-module closer.

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

Public drop-in kernel provider for Route106-style branches.

Acceptance checks