Route30 minimal-block kernel/head concrete-coherent provider

Route29 closes the head/invariant layer from the four route21-style same-raw- tower leaves, but still constructs the selected K, Phi(K), R, M, T, C tower through the split concrete Frattini/raw-object/action leaves.

This sidecar keeps the route29 head/lower assembly and replaces the concrete split calls by the existing manuscript-shaped coherent packets:

• minimalBlock_kernelFrattiniCollapseFullData, the complete Frattini--centralizer collapse for the literal R = Phi(K);
• minimalBlock_kernelRawQuotientTowerData, the same-tower raw quotient, transported actions, literal K/R ~= M bridge, and nonzero head.

The least kernel remains the route26 selected upper-candidate construction, so the only least-kernel residual exposed here is the universal leastness of that selected candidate.

Route29-compatible coherent concrete packet

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

Route30 packet with the same downstream shape as route29, but whose concrete lower tower is supplied by the coherent §7 Frattini-collapse/raw-quotient packets rather than by the split concrete leaves.

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

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute30.Data.route29Data {p : FramedPair} {chief : NonScalarChiefFactor p} (P : Data chief) : MinimalBlockKernelConcreteRoute29Data chief

Route29-compatible packet recovered from route30.

Equations

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

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

Route30 group-tower data, via the route29 downstream projection.

Equations

• P.groupTowerData = P.route29Data.groupTowerData

Assembly

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute30.data_from_coherentConcreteRoute21Split {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (Data chief)

Route30 kernel/head packet from the coherent concrete tower and route21 head/lower leaves on the same raw quotient tower.

Compared with minimalBlock_kernelConcreteRoute29Data_from_route21Split, this theorem no longer calls the split concrete Frattini collapse leaves, raw object leaves, raw action leaves, T-stability leaf, or concrete K/R bridge leaf.

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute30.route29Data_from_coherentConcreteRoute21Split {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelConcreteRoute29Data chief)

Route29-shaped provider recovered from the route30 coherent concrete packet.

This is the compatibility hook for code currently consuming minimalBlock_kernelConcreteRoute29Data_from_route21Split.

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

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

Public aliases matching the surrounding route-provider naming style

theorem Q2Presentation.Induction.minimalBlock_kernelConcreteRoute30Data_from_coherentConcreteRoute21Split {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelConcreteRoute29Data chief)

Route30 replacement for minimalBlock_kernelConcreteRoute29Data_from_route21Split.

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

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