Route37 minimal-block kernel/head refinement

Route36 exported the minimal-block group tower through the broad minimalBlock_provenanceSemanticData packet. This sidecar keeps routed files untouched and exports a drop-in provider whose axiom closure replaces that packet by the finer concrete provenance and same-tower simple-head/scalar closers already available in MinimalBlockProvenanceConcreteClosers2.

The Route36 transparent two-packet bridge is retained as an audit comparison: it honestly lowers the broad semantic packet to concrete provenance plus the actual invariant packet. The public Route37 provider below uses the finer concrete-closer route instead.

Audit bridge from Route36

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

Route36's transparent bridge, kept here as an explicit comparison point.

Route37 concrete-closer provider

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute37.provenanceSemanticData_from_concreteClosers2 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockProvenanceSemanticData chief)

Route37 closes the broad provenance-semantic packet through the finer concrete/head-dual/head-stability/lower-scalar packets.

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

Route37 group tower through the finer provenance split.

Public route37 aliases

theorem Q2Presentation.Induction.minimalBlock_provenanceSemanticData_from_kernelConcreteRoute37 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockProvenanceSemanticData chief)

Route37 replacement for the Route36 provenance-semantic packet.

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

Route37 replacement for the Route36 minimal-block group-tower provider.