Documentation

Q2Presentation.Induction.MinimalBlockKernelRoute60RawHeadClosers

Route60 raw transport, K/R bridge, and simple-head closers #

This sidecar is route-neutral. It does not edit the active integrated route.

Route58 compressed the Section 7 raw/head frontier into broad same-tower packets. Route60 keeps the same manuscript tower, but exports theorem-level providers whose axiom closures are the lower-level leaves:

raw R, M, T, and C object packets;
induced actions on R and M, plus T-stability;
the literal K/Phi(K) ~= M bridge;
invariant-hyperplane, irreducible-head, nontrivial-head-action, and lower-character packets.

The public provider has the Route55 target shape, so a future integrated route can swap it in where minimalBlock_groupTowerData_from_kernelRoute55 is used.

Raw object/action glue over the Route42 leaves #

def Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.rawModuleObjectsOfPieces {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F) (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) :

MinimalBlockKernelModuleConcreteRawModuleObjectsData K F

Equations

Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.rawModuleObjectsOfPieces Robj Mobj = Q2Presentation.Induction.MinimalBlockKernelConcreteRoute42.rawModuleObjectsOfPieces Robj Mobj

Instances For

def Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.rawSubquotientObjectsOfPieces {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F) (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) (Tobj : MinimalBlockKernelConcreteRoute42.RawSubmoduleObjectData Mobj) (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) :

MinimalBlockKernelModuleConcreteRawSubquotientObjectsData (rawModuleObjectsOfPieces Robj Mobj)

Equations

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

Instances For

def Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.rawObjectsOfPieces {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F) (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) (Tobj : MinimalBlockKernelConcreteRoute42.RawSubmoduleObjectData Mobj) (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) :

MinimalBlockKernelModuleConcreteRawObjectsData K F

Equations

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

Instances For

def Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.rawFrattiniActionOfPieces {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F) (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) (Tobj : MinimalBlockKernelConcreteRoute42.RawSubmoduleObjectData Mobj) (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) (A : MinimalBlockKernelConcreteRoute42.RawFrattiniActionData Robj Cobj) :

MinimalBlockKernelModuleConcreteRawFrattiniActionData (rawModuleObjectsOfPieces Robj Mobj) (rawSubquotientObjectsOfPieces Robj Mobj Tobj Cobj)

Equations

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

Instances For

def Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.rawModuleActionOfPieces {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F) (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) (Tobj : MinimalBlockKernelConcreteRoute42.RawSubmoduleObjectData Mobj) (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) (A : MinimalBlockKernelConcreteRoute42.RawModuleActionData Mobj Cobj) :

MinimalBlockKernelModuleConcreteRawModuleActionData (rawModuleObjectsOfPieces Robj Mobj) (rawSubquotientObjectsOfPieces Robj Mobj Tobj Cobj)

Equations

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

Instances For

def Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.rawTStableOfPieces {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F) (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) (Tobj : MinimalBlockKernelConcreteRoute42.RawSubmoduleObjectData Mobj) (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) (A : MinimalBlockKernelConcreteRoute42.RawModuleActionData Mobj Cobj) (TS : MinimalBlockKernelConcreteRoute42.RawSubmoduleStableData Tobj A) :

MinimalBlockKernelModuleConcreteRawTStableData (rawModuleActionOfPieces Robj Mobj Tobj Cobj A)

Equations

⋯ = ⋯

Instances For

def Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.rawActionsOfPieces {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F) (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) (Tobj : MinimalBlockKernelConcreteRoute42.RawSubmoduleObjectData Mobj) (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) (AR : MinimalBlockKernelConcreteRoute42.RawFrattiniActionData Robj Cobj) (AM : MinimalBlockKernelConcreteRoute42.RawModuleActionData Mobj Cobj) (TS : MinimalBlockKernelConcreteRoute42.RawSubmoduleStableData Tobj AM) :

MinimalBlockKernelModuleConcreteRawActionsData (rawObjectsOfPieces Robj Mobj Tobj Cobj)

Equations

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

Instances For

def Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.rawDataOfPieces {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F) (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) (Tobj : MinimalBlockKernelConcreteRoute42.RawSubmoduleObjectData Mobj) (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) (AR : MinimalBlockKernelConcreteRoute42.RawFrattiniActionData Robj Cobj) (AM : MinimalBlockKernelConcreteRoute42.RawModuleActionData Mobj Cobj) (TS : MinimalBlockKernelConcreteRoute42.RawSubmoduleStableData Tobj AM) :

MinimalBlockKernelModuleConcreteRawData K F

Equations

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

Instances For

Route60 coherent raw transport packet, theorem-built from lower leaves #

structure Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.RawHeadTransportPieces {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) :

Route60 raw/head transport data for one selected K, Phi(K) tower.

This is not declared as a residual axiom. The provider below builds it from the individual object, action, stability, K/R-bridge, and head-action leaves.

Robj : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F
Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F
Tobj : MinimalBlockKernelConcreteRoute42.RawSubmoduleObjectData self.Mobj
Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F
actR : MinimalBlockKernelConcreteRoute42.RawFrattiniActionData self.Robj self.Cobj
actM : MinimalBlockKernelConcreteRoute42.RawModuleActionData self.Mobj self.Cobj
stable : MinimalBlockKernelConcreteRoute42.RawSubmoduleStableData self.Tobj self.actM
kmodR : MinimalBlockKernelConcreteRoute42.KmodRConcreteEquivData (rawDataOfPieces self.Robj self.Mobj self.Tobj self.Cobj self.actR self.actM ⋯)
headAction : MinimalBlockRawHeadActionNotPointwiseTrivialData (rawDataOfPieces self.Robj self.Mobj self.Tobj self.Cobj self.actR self.actM ⋯).rawTowerData

Instances For

def Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.RawHeadTransportPieces.moduleObjects {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (P : RawHeadTransportPieces K F) :

MinimalBlockKernelModuleConcreteRawModuleObjectsData K F

Equations

P.moduleObjects = Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.rawModuleObjectsOfPieces P.Robj P.Mobj

Instances For

def Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.RawHeadTransportPieces.subquotientObjects {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (P : RawHeadTransportPieces K F) :

MinimalBlockKernelModuleConcreteRawSubquotientObjectsData P.moduleObjects

Equations

P.subquotientObjects = Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.rawSubquotientObjectsOfPieces P.Robj P.Mobj P.Tobj P.Cobj

Instances For

def Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.RawHeadTransportPieces.rawObjects {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (P : RawHeadTransportPieces K F) :

MinimalBlockKernelModuleConcreteRawObjectsData K F

Equations

P.rawObjects = Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.rawObjectsOfPieces P.Robj P.Mobj P.Tobj P.Cobj

Instances For

def Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.RawHeadTransportPieces.frattiniAction {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (P : RawHeadTransportPieces K F) :

MinimalBlockKernelModuleConcreteRawFrattiniActionData P.moduleObjects P.subquotientObjects

Equations

P.frattiniAction = Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.rawFrattiniActionOfPieces P.Robj P.Mobj P.Tobj P.Cobj P.actR

Instances For

def Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.RawHeadTransportPieces.moduleAction {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (P : RawHeadTransportPieces K F) :

MinimalBlockKernelModuleConcreteRawModuleActionData P.moduleObjects P.subquotientObjects

Equations

P.moduleAction = Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.rawModuleActionOfPieces P.Robj P.Mobj P.Tobj P.Cobj P.actM

Instances For

def Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.RawHeadTransportPieces.tStable {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (P : RawHeadTransportPieces K F) :

MinimalBlockKernelModuleConcreteRawTStableData P.moduleAction

Equations

⋯ = ⋯

Instances For

def Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.RawHeadTransportPieces.rawActions {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (P : RawHeadTransportPieces K F) :

MinimalBlockKernelModuleConcreteRawActionsData P.rawObjects

Equations

P.rawActions = Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.rawActionsOfPieces P.Robj P.Mobj P.Tobj P.Cobj P.actR P.actM ⋯

Instances For

def Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.RawHeadTransportPieces.rawData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (P : RawHeadTransportPieces K F) :

MinimalBlockKernelModuleConcreteRawData K F

Equations

P.rawData = Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.rawDataOfPieces P.Robj P.Mobj P.Tobj P.Cobj P.actR P.actM ⋯

Instances For

def Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.RawHeadTransportPieces.bridgeData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (P : RawHeadTransportPieces K F) :

MinimalBlockKernelModuleConcreteBridgeData P.rawData

Equations

P.bridgeData = id P.kmodR.bridgeData

Instances For

def Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.RawHeadTransportPieces.headData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (P : RawHeadTransportPieces K F) :

MinimalBlockKernelModuleConcreteHeadData P.rawData

Equations

⋯ = ⋯

Instances For

def Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.RawHeadTransportPieces.rawQuotient {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (P : RawHeadTransportPieces K F) :

MinimalBlockKernelRawQuotientTowerData K F

Equations

P.rawQuotient = { objects := P.rawObjects, actions := P.rawActions, bridge := id P.bridgeData, head := ⋯ }

Instances For

Individual theorem-level providers for the requested raw subset #

theorem Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.minimalBlock_kernelModuleConcreteRawModuleObjectsData_from_route60RawHeadClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) :

Nonempty (MinimalBlockKernelModuleConcreteRawModuleObjectsData K F)

theorem Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.minimalBlock_kernelModuleConcreteRawSubquotientObjectsData_from_route60RawHeadClosers {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F) (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) :

Nonempty (MinimalBlockKernelModuleConcreteRawSubquotientObjectsData (rawModuleObjectsOfPieces Robj Mobj))

theorem Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.minimalBlock_kernelModuleConcreteRawFrattiniActionData_from_route60RawHeadClosers {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F) (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) (Tobj : MinimalBlockKernelConcreteRoute42.RawSubmoduleObjectData Mobj) (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) :

Nonempty (MinimalBlockKernelModuleConcreteRawFrattiniActionData (rawModuleObjectsOfPieces Robj Mobj) (rawSubquotientObjectsOfPieces Robj Mobj Tobj Cobj))

theorem Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.minimalBlock_kernelModuleConcreteRawModuleActionData_from_route60RawHeadClosers {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F) (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) (Tobj : MinimalBlockKernelConcreteRoute42.RawSubmoduleObjectData Mobj) (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) :

Nonempty (MinimalBlockKernelModuleConcreteRawModuleActionData (rawModuleObjectsOfPieces Robj Mobj) (rawSubquotientObjectsOfPieces Robj Mobj Tobj Cobj))

theorem Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.minimalBlock_kernelModuleConcreteRawTStableData_from_route60RawHeadClosers {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F) (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) (Tobj : MinimalBlockKernelConcreteRoute42.RawSubmoduleObjectData Mobj) (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) (A : MinimalBlockKernelConcreteRoute42.RawModuleActionData Mobj Cobj) :

Nonempty (MinimalBlockKernelModuleConcreteRawTStableData (rawModuleActionOfPieces Robj Mobj Tobj Cobj A))

theorem Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.rawHeadTransportPieces_from_route60RawHeadClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) :

Nonempty (RawHeadTransportPieces K F)

theorem Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.rawQuotientTowerData_from_route60RawHeadClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) :

Nonempty (MinimalBlockKernelRawQuotientTowerData K F)

theorem Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.rawDataAndKmodRQuotientEquivData_from_route60RawHeadClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) :

∃ (D : MinimalBlockKernelModuleConcreteRawData K F), Nonempty (MinimalBlockKernelModuleConcreteBridgeData D)

Head and lower-scalar closers from lower-level simple-head leaves #

theorem Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.minimalBlock_rawHeadQuotientNoTrivialData_from_route60RawHeadClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) :

Nonempty (MinimalBlockRawHeadQuotientNoTrivialData D)

theorem Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.minimalBlock_rawHeadSimplicityActualData_from_route60RawHeadClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) :

Nonempty (MinimalBlockRawHeadSimplicityActualData D)

theorem Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.minimalBlock_rawLowerScalarQuotientData_from_route60RawHeadClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) :

Nonempty (MinimalBlockRawLowerScalarQuotientData D)

theorem Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.rawSimpleHeadSemanticData_from_route60RawHeadClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) :

Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData D)

Route55-shaped and group-tower providers #

theorem Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.kernelRoute55Data_from_route60RawHeadClosers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockKernelRoute55.KernelRoute55Data chief)

theorem Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.kernelRoute54Data_from_route60RawHeadClosers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockKernelRoute54.KernelRoute54Data chief)

theorem Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.consumedData_from_route60RawHeadClosers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockKernelRoute53.ConsumedData chief)

theorem Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.groupInvariantRouteData_from_route60RawHeadClosers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockGroupInvariantRouteData chief)

theorem Q2Presentation.Induction.MinimalBlockKernelRoute60RawHead.groupTowerData_from_route60RawHeadClosers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockGroupTowerData p chief)

Public Route60 provider #

theorem Q2Presentation.Induction.minimalBlock_groupTowerData_from_kernelRoute60RawHeadClosers {p : FramedPair} (chief : NonScalarChiefFactor p) :

Nonempty (MinimalBlockGroupTowerData p chief)

Route60 drop-in kernel/raw provider for future integration.

Its target matches minimalBlock_groupTowerData_from_kernelRoute55, while the raw/KmodR/head/lower-scalar closure is split into the Route60 lower-level manuscript leaves instead of the nine broad residual names targeted by this sidecar.