Route45 minimal-block kernel/raw tower cleanup

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

Route45 is an integration-ready replacement for minimalBlock_groupTowerData_from_kernelConcreteRoute44. It removes the four Route44 kernel/raw aggregate leaves from the provider closure:

• the route26 fixed-upper universal leastness shortcut is not used; the route selects the genuine least-over-chief Section 7 packet;
• the coherent minimalBlock_kernelFrattiniCollapseFullData leaf is replaced by the field-level Frattini-collapse packets already isolated lower in the tree;
• the coherent minimalBlock_kernelRawQuotientTowerData leaf is replaced by the raw object/subquotient/action/bridge/head transport packets;
• the Route44 rawSimpleHeadSemanticData aggregate is replaced by the same-tower InvariantActualProofs3 route.

Route44 simple-head aggregate from lower same-tower packets

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute45.lowerInvariantCharacterExistsOfActual {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (Q : MinimalBlockRawLowerInvariantCharacterActualData D) : MinimalBlockRawLowerInvariantCharacterExistsData D

Lower invariant character in the existential Route44 form.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute45.rawSimpleHeadSemanticData_from_route45Lower {p : FramedPair} {chief : NonScalarChiefFactor p} (lower : MinimalBlockLowerGroupModuleData chief) : Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData lower.rawTowerData)

Route45 replacement for the Route44 raw simple-head aggregate, tied to a selected lower tower so the nonzero-head field is not reselected separately.

Least, collapse, and raw quotient replacements

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute45.leastOverChiefData_from_route45 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelLeastOverChiefData chief)

Route45 selects the genuine least-over-chief packet instead of the route26 fixed-upper universal leastness shortcut.

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute45.frattiniData_from_route45Split {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniData K)

Route45 Frattini data through the field-level lem:collapse split.

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute45.rawQuotientTowerData_from_route45Transport {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelRawQuotientTowerData K F)

Route45 raw quotient tower through the raw object/subquotient/action and same-tower bridge/head transport packets.

Route-ready group tower

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute45.kernelModuleConcreteProvenanceData_from_route45 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Concrete provenance through the Route45 least/collapse/raw route.

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute45.provenanceConcreteFinalPieces_from_route45 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockProvenanceConcreteFinalPieces chief)

Concrete-final provenance through the Route45 kernel/raw route and the same-tower InvariantActualProofs3 simple-head split.

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

Route45 provenance-semantic data.

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

Route45 group tower through the lowered Section 7 kernel/raw route.

Public Route45 aliases

theorem Q2Presentation.Induction.minimalBlock_kernelModuleConcreteProvenanceData_from_kernelConcreteRoute45 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Route45 replacement for the Route44 concrete provenance assembly.

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

Route45 replacement for the Route44 provenance-semantic packet.

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

Drop-in Route45 provider replacing minimalBlock_groupTowerData_from_kernelConcreteRoute44.