Route35 minimal-block kernel/head refinement

Route34 keeps the route21-style simple-head/lower-character split, but its concrete kernel/raw tower is still assembled from independent leaves. This sidecar keeps the same downstream packet shape and replaces that concrete tower cluster by the existing same-tower provenance packet MinimalBlockKernelModuleConcreteProvenanceData.

The exported group-tower theorem is route34-compatible: it still produces the same MinimalBlockGroupTowerData, and it preserves the four route21 head/lower leaves rather than replacing them by older broader invariant packets.

Route34-compatible packet

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

Route35 packet with the same downstream fields as route34.

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

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

Route34-compatible packet recovered from route35.

Equations

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

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

Route35 group-tower data, via the route34 downstream projection.

Equations

• P.groupTowerData = P.route34Data.groupTowerData

Concrete tower from one provenance packet

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute35.frattiniFullOfProvenance {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelModuleConcreteProvenanceData chief) : MinimalBlockKernelFrattiniCollapseFullData P.leastData

The full Frattini-collapse packet carried by the coherent concrete provenance object.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute35.rawQuotientOfProvenance {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelModuleConcreteProvenanceData chief) : MinimalBlockKernelRawQuotientTowerData P.leastData ⋯

Raw quotient/action/head packet carried by the same coherent concrete provenance object.

Equations

• One or more equations did not get rendered due to their size.

Assembly

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute35.data_from_provenanceRoute21HeadSplit {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (Data chief)

Route35 packet from one coherent concrete provenance object plus the route21 simple-head/lower-character split on the selected raw tower.

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

Route34-shaped packet supplied by route35.

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

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

Public aliases matching route-provider naming style

theorem Q2Presentation.Induction.minimalBlock_kernelConcreteRoute35Data_from_provenanceRoute21HeadSplit {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelConcreteRoute35.Data chief)

Route35 replacement for the route34 kernel/head packet.

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

Route34-shaped packet supplied by route35.

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

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