Route31 minimal-block kernel/head concrete split

Route30 exposes the Section 7 kernel/head frontier through three coherent kernel packets plus four route21 head/lower leaves. This sidecar keeps the route30 downstream shape, but rebuilds the provider through the route27-style actual same-tower head packet and the finer concrete Frattini/raw tower split.

The exported group-tower theorem is intended as a kernel/head-only replacement for minimalBlock_groupTowerData_from_kernelConcreteRoute30. It does not edit the integrated route files.

Route30-compatible packet

structure Q2Presentation.Induction.MinimalBlockKernelConcreteRoute31.Data {p : FramedPair} (chief : NonScalarChiefFactor p) : Type 1

Route31 packet with the same downstream fields as route30.

The lower tower is assembled from concrete split leaves, while the head action and invariant/lower layer are projected from one actual same-raw-tower packet.

• least : MinimalBlockKernelLeastOverChiefData chief
• frattiniFull : MinimalBlockKernelFrattiniCollapseFullData self.least
• rawQuotient : MinimalBlockKernelRawQuotientTowerData self.least ⋯
• invariantActual : MinimalBlockInvariantActualProofs2Data self.rawQuotient.rawData.rawTowerData

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute31.Data.route30Data {p : FramedPair} {chief : NonScalarChiefFactor p} (P : Data chief) : MinimalBlockKernelConcreteRoute30.Data chief

Route30-compatible packet recovered from route31.

Equations

• P.route30Data = { least := P.least, frattiniFull := ⋯, rawQuotient := P.rawQuotient, invariantActual := P.invariantActual }

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute31.Data.groupTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : Data chief) : MinimalBlockGroupTowerData p chief

Route31 group-tower data, via the route30 downstream projection.

Equations

• P.groupTowerData = P.route30Data.groupTowerData

Assembly

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute31.data_from_concreteSplitActualHead {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (Data chief)

Route31 kernel/head packet from the concrete split tower and one actual same-tower simple-head/lower-character packet.

Compared with route30, this theorem avoids the exact residual names minimalBlock_kernelFrattiniCollapseFullData, minimalBlock_kernelRawQuotientTowerData, and the four minimalBlock_route21_raw... leaves. The least-kernel universal packet remains explicit.

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute31.route30Data_from_concreteSplitActualHead {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelConcreteRoute30.Data chief)

Route30-shaped packet recovered from the route31 construction.

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

Route31 replacement for the current minimal-block group-tower provider.

Public aliases matching route-provider naming style

theorem Q2Presentation.Induction.minimalBlock_kernelConcreteRoute31Data_from_concreteSplitActualHead {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelConcreteRoute31.Data chief)

Route31 replacement for the route30 kernel/head packet.

theorem Q2Presentation.Induction.minimalBlock_kernelConcreteRoute30Data_from_kernelConcreteRoute31 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelConcreteRoute30.Data chief)

Route30-shaped packet supplied by route31.

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

Route31 replacement for the minimal-block group-tower provider.