Route34 minimal-block kernel/head refinement

Route33 currently uses the route31 kernel/head provider. Route31 keeps the concrete K, Phi(K), R, M, T, C tower split into the fine Section 7 leaves, but it still obtains the final simple-head/lower-character package from the monolithic same-raw-tower residual minimalBlock_invariantActualProofs2Data.

This sidecar exports a route31-compatible provider whose data shape is identical to route31, while sourcing that invariant package through the route29 route21-style simple-head split:

• invariant hyperplanes contain T;
• nonzero stable quotient-head submodules are top;
• the quotient-head action is not pointwise trivial;
• the lower Frattini layer has a nonzero invariant character.

No routed file is edited. This is a genuine refinement of the route33 kernel/head frontier: the route33-listed monolithic invariant residual is no longer in the closure of the exported provider.

Route31-compatible packet

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

Route34 packet with the same downstream fields as route31.

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

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

Route31-compatible packet recovered from route34.

Equations

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

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

Route34 group-tower data, via the route31 downstream projection.

Equations

• P.groupTowerData = P.route31Data.groupTowerData

Assembly

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute34.data_from_route21HeadSplit {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (Data chief)

Route34 packet from the route29 same-tower simple-head/lower-character split.

This keeps the concrete tower split used by route31, but replaces the monolithic route31 invariant residual with four smaller route21-style manuscript obligations on the same raw tower.

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

Route31-shaped packet supplied by route34.

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

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

Public aliases matching route-provider naming style

theorem Q2Presentation.Induction.minimalBlock_kernelConcreteRoute34Data_from_route21HeadSplit {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelConcreteRoute34.Data chief)

Route34 replacement for the route31 kernel/head packet.

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

Route31-shaped packet supplied by route34.

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

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