Route36 minimal-block kernel/head refinement

Route35 exposes the Section 7 kernel/head contribution as one concrete provenance packet plus the four route21 raw head/lower leaves. This sidecar keeps routed files untouched and exports a drop-in group-tower provider whose closure replaces those five names by the coherent same-tower MinimalBlockProvenanceSemanticData packet.

For auditability, the file also includes a more transparent two-packet provider: it keeps the concrete provenance packet and replaces the four route21 leaves by the existing actual same-raw-tower head/lower-character packet.

Transparent actual-head split

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

Coherent provenance-semantic data from Route35's concrete provenance packet plus the actual same-raw-tower invariant packet.

This avoids the four route21 raw head/lower residual names while keeping the concrete K/R provenance residual explicit.

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

Route36 group tower through the transparent two-packet split.

One-packet provenance-semantic provider

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

Route36 group tower through the coherent provenance-semantic packet.

This is the strongest current kernel/head provider in this file: the five Route35 kernel/head residual names are absent from its axiom closure.

Public route36 aliases

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

Route36 transparent provider: concrete provenance plus actual same-head packet.

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

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