Route17 kernel/concrete provenance sidecar for Section 7

This sidecar leaves the routed proof files untouched. Route16 exposed one coherent residual packet,

minimalBlock_kernelConcreteRoute16Data,

for the Section 7 minimal-block kernel construction. Route17 proves that Route16 packet from narrower manuscript-shaped leaves already present in the tree:

• the least normal subgroup K over the selected chief factor;
• the full Frattini--centralizer collapse for literal R = Phi(K);
• raw R, M, T, C objects, induced actions, and the literal K/R ~= M bridge;
• the same-raw-tower simple-head/invariant semantic packet.

The exported theorem minimalBlock_groupTowerData_from_kernelConcreteRoute17 has the same supervisor integration shape as Route16's group-tower provider, but its axiom closure no longer contains minimalBlock_kernelConcreteRoute16Data.

Raw provenance for the fixed K, Phi(K) tower

structure Q2Presentation.Induction.MinimalBlockKernelConcreteRoute17RawProvenanceData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Type 1

Route17 raw provenance: raw quotient objects/actions plus the literal K/R ~= M bridge, all for the same selected K and Frattini packet.

This is the raw/provenance part of manuscript eq:targettower; the simple-head and invariant consequences are kept as a separate same-raw-tower input below.

• objects : MinimalBlockKernelModuleConcreteRawObjectsData K F
• actions : MinimalBlockKernelModuleConcreteRawActionsData self.objects
• bridge : MinimalBlockKernelModuleConcreteBridgeData (MinimalBlockKernelModuleConcreteRawData.ofObjectsActions self.objects self.actions)

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute17RawProvenanceData.rawData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (P : MinimalBlockKernelConcreteRoute17RawProvenanceData K F) : MinimalBlockKernelModuleConcreteRawData K F

Forget Route17 raw provenance to the existing concrete raw-data packet.

Equations

• P.rawData = Q2Presentation.Induction.MinimalBlockKernelModuleConcreteRawData.ofObjectsActions P.objects P.actions

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute17RawProvenanceData.bridgeData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (P : MinimalBlockKernelConcreteRoute17RawProvenanceData K F) : MinimalBlockKernelModuleConcreteBridgeData P.rawData

The same bridge, restated over rawData.

Equations

• P.bridgeData = id P.bridge

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute17RawProvenanceData.route16RawCore {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (P : MinimalBlockKernelConcreteRoute17RawProvenanceData K F) : MinimalBlockKernelRawQuotientCoreRoute16Data K F

Forget Route17 raw provenance to Route16's raw-core structure.

Equations

• P.route16RawCore = { objects := P.objects, actions := P.actions, bridge := P.bridge }

theorem Q2Presentation.Induction.minimalBlock_kernelConcreteRoute17RawProvenanceData_from_currentClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelConcreteRoute17RawProvenanceData K F)

Build the Route17 raw provenance from the existing narrower raw object/action packets and the existing same-tower K/R ~= M bridge theorem.

The axiom closure of this theorem exposes raw objects, raw actions, and the lower semantic bridge input separately; it does not use the Route16 monolithic kernel/concrete packet.

Route16 package recovered from narrower Route17 pieces

theorem Q2Presentation.Induction.minimalBlock_kernelConcreteRoute16Data_from_kernelConcreteRoute17 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelConcreteRoute16Data chief)

Route17 proves the Route16 coherent kernel/concrete package from narrower manuscript-shaped leaves:

• minimalBlock_kernelLeastOverChiefData;
• minimalBlock_kernelFrattiniCollapseFullData;
• raw object/action packets and the minimalBlock_kmodRBridgeData bridge input;
• minimalBlock_headInvariantSemanticRoute12Data on the resulting raw tower.

This theorem is intentionally named as a Route17 provenance theorem rather than redeclaring the existing Route16 axiom.

theorem Q2Presentation.Induction.minimalBlock_kernelModuleActualProofs_from_kernelConcreteRoute17 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleActualProofs chief)

Aggregate actual kernel/module packet through the Route17 provenance split.

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

Lower group/module data through the Route17 provenance split.

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

Route17 group-tower provider, suitable for replacing the Route16 provider in supervisor integration.