Route48 minimal-block kernel/head sharpening

This sidecar is route-neutral: no routed/root file imports it yet.

Route47's kernel provider closes the Section 7 lower/head slice through the aggregate packet

• minimalBlock_groupInvariantActualData.

That packet keeps a coherent lower tower, but it also stores the stronger head-quotient no-trivial packet and the stronger lower scalar quotient packet. The framed route only consumes the lower tower, dual-invariant vanishing on its raw module, and one raw nonzero invariant character on the Frattini layer.

Route48 therefore routes through the smaller same-tower packet minimalBlock_groupInvariantRouteData from MinimalBlockGroupInvariantActualProofs. The exported provider below is a drop-in replacement for minimalBlock_groupTowerData_from_kernelConcreteRoute47 with a strictly smaller manuscript-shaped obligation.

Same-tower consumed lower/head packet

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute48.groupInvariantRouteData_from_route48 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupInvariantRouteData chief)

Route48 lower/head packet.

This is the exact data consumed by the current group-tower construction: the coherent lower subgroup/module tower, dual-invariant vanishing on the raw module from that tower, and a raw invariant determinant character on the same Frattini layer.

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

Projection to the coherent lower group/module tower selected by the Route48 packet.

Route-ready group tower

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

Route48 group tower through the smaller same-tower lower/head packet, avoiding the stronger Route47 aggregate minimalBlock_groupInvariantActualData.

Public Route48 alias

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

Drop-in Route48 provider replacing minimalBlock_groupTowerData_from_kernelConcreteRoute47.