Route184 Section 7 kernel Frattini closers

This sidecar changes only the Frattini/provenance half of the Route183 kernel diagnostic. The Route43 raw R,M,T,C object/action/head leaves remain exactly where Route183 exposes them.

The fourteen Route141 Frattini leaves are bypassed by using the direct Route164 Lemma 7.2 packets:

• selected least candidate plus universal leastness;
• a single nonidentity element in the literal embedded Phi(K);
• the final centralizer step K centralizes Phi(K);
• the final fourth-power step K^4 = 1;
• the final elementary Frattini-layer exponent step.

Those packets assemble the same Route78-selected Frattini interfaces consumed downstream, while avoiding the Route141 section-local leaf names.

Least kernel

theorem Q2Presentation.Induction.Section7KernelRoute184FrattiniClosers.leastOverChiefData_from_route184Frattini {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelLeastOverChiefData chief)

Route184 least-over-chief packet from the Route164 selected candidate/universal split.

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

Route78-shaped selected least-kernel packet through Route184.

Frattini nonidentity

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

Route78-shaped internal Frattini witness through the Route164 nonidentity packet.

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

Concrete Frattini nontriviality through Route184.

Centralizer collapse

def Q2Presentation.Induction.Section7KernelRoute184FrattiniClosers.frattiniCentralizerCoreDataOfRoute184 {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (C : Section7KernelRoute164Closers.FrattiniCentralizerStepData K) : MinimalBlockKernelRoute72FrattiniClosers.FrattiniCentralizerCoreData K

Route72 centralizer core obtained by taking the selected core to be K itself after the Route164 centralizer step.

Equations

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

def Q2Presentation.Induction.Section7KernelRoute184FrattiniClosers.frattiniCentralizerHallImageDataOfRoute184 {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (C : Section7KernelRoute164Closers.FrattiniCentralizerStepData K) : MinimalBlockKernelRoute72FrattiniClosers.FrattiniCentralizerHallImageData (frattiniCentralizerCoreDataOfRoute184 C)

Route72 Hall-image field for the Route184 selected centralizer core. The chosen image subgroup is K, using K S = P.

Equations

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

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

Route78-shaped Frattini-centralizer packet through Route184.

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

Route60 centralizer-step packet through Route184.

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

Concrete Frattini centrality through Route184.

Fourth-power collapse

def Q2Presentation.Induction.Section7KernelRoute184FrattiniClosers.fourthPowerKernelCoreDataOfRoute184 {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (P4 : Section7KernelRoute164Closers.FourthPowerMapVanishesData K) : MinimalBlockKernelRoute72FrattiniClosers.FourthPowerKernelCoreData K

Route72 fourth-power core obtained by taking the selected kernel to be K itself after the Route164 fourth-power step.

Equations

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

def Q2Presentation.Induction.Section7KernelRoute184FrattiniClosers.fourthPowerKernelHallImageDataOfRoute184 {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (P4 : Section7KernelRoute164Closers.FourthPowerMapVanishesData K) : MinimalBlockKernelRoute72FrattiniClosers.FourthPowerKernelHallImageData (fourthPowerKernelCoreDataOfRoute184 P4)

Route72 Hall-image field for the Route184 selected fourth-power core. The chosen image subgroup is K, using K S = P.

Equations

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

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

Route78-shaped fourth-power packet through Route184.

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

Route60 fourth-power-map packet through Route184.

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

Concrete fourth-power vanishing through Route184.

Elementary Frattini layer

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

Route78 literal exponent packet through the Route164 elementary Frattini layer.

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

Route60 elementary Frattini-layer packet through Route184.

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

Concrete exponent-two Frattini packet through Route184.

Frattini and raw tower assembly

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

Concrete Frattini packet assembled through the Route184 replacements.

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

Route184 module-layer packet: Route184 Frattini data plus Route183's raw Route43 tower.

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

Concrete kernel/module provenance through Route184.

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

Lower group/module data through Route184.

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

Drop-in Route184 Section 7 kernel provider.