Route63 raw/head closers for the Route42 frontier

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

Route60 currently assembles its raw/head transport through the twelve Route42 raw/head atoms. Route63 keeps the same consumer shapes, but obtains them from the lower Route43 manuscript packets:

• literal R = Phi(K), M = K/Phi(K), T, and C = Y/K object packets;
• transported actions on R and M, plus T-stability;
• the literal K/Phi(K) ~= M bridge carried by the Route43 M packet;
• the simple-head maximal/orbit/nontrivial-action/lower-character packets.

The public raw-head provider below has the same target as MinimalBlockKernelRoute60RawHead.rawHeadTransportPieces_from_route60RawHeadClosers, but its axiom closure avoids the twelve Route42 atom constants.

Exact Route42-shape providers from lower Route43 packets

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute63RawHeadClosers.rawFrattiniModuleObjectData_from_route63 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F)

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute63RawHeadClosers.rawQuotientModuleObjectData_from_route63 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F)

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute63RawHeadClosers.rawSubmoduleObjectData_from_route63 {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) : Nonempty (MinimalBlockKernelConcreteRoute42.RawSubmoduleObjectData Mobj)

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute63RawHeadClosers.rawLowerQuotientGroupData_from_route63 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F)

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute63RawHeadClosers.rawFrattiniActionData_from_route63 {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F) (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) : Nonempty (MinimalBlockKernelConcreteRoute42.RawFrattiniActionData Robj Cobj)

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute63RawHeadClosers.rawModuleActionData_from_route63 {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) : Nonempty (MinimalBlockKernelConcreteRoute42.RawModuleActionData Mobj Cobj)

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute63RawHeadClosers.rawSubmoduleStableData_from_route63Transport {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} {Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F} {Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F} (Tobj : MinimalBlockKernelConcreteRoute42.RawSubmoduleObjectData Mobj) (A43 : MinimalBlockKernelConcreteRoute43.RawModuleTransportActionData Mobj Cobj) : Nonempty (MinimalBlockKernelConcreteRoute42.RawSubmoduleStableData Tobj A43.toRoute42)

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute63RawHeadClosers.rawModuleActionStablePair_from_route63 {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} {Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F} {Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F} (Tobj : MinimalBlockKernelConcreteRoute42.RawSubmoduleObjectData Mobj) : ∃ (A : MinimalBlockKernelConcreteRoute42.RawModuleActionData Mobj Cobj), Nonempty (MinimalBlockKernelConcreteRoute42.RawSubmoduleStableData Tobj A)

Narrow same-pieces bridge provider

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute63RawHeadClosers.kmodRConcreteEquivDataOfLiteralM {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Rlit : MinimalBlockKernelConcreteRoute43.RawFrattiniLiteralModuleObjectData K F) (Mlit : MinimalBlockKernelConcreteRoute43.RawQuotientLiteralModuleObjectData K F) (Tlit : MinimalBlockKernelConcreteRoute43.RawSubmoduleLiteralObjectData Mlit.toObject) (Clit : MinimalBlockKernelConcreteRoute43.RawLowerLiteralQuotientGroupData K F) (AR : MinimalBlockKernelConcreteRoute43.RawFrattiniTransportActionData Rlit.toObject Clit.toObject) (AM : MinimalBlockKernelConcreteRoute43.RawModuleTransportActionData Mlit.toObject Clit.toObject) (TS : MinimalBlockKernelConcreteRoute43.RawSubmoduleTransportStableData Tlit.toObject AM) : MinimalBlockKernelConcreteRoute42.KmodRConcreteEquivData (MinimalBlockKernelRoute60RawHead.rawDataOfPieces Rlit.toObject Mlit.toObject Tlit.toObject Clit.toObject AR.toRoute42 AM.toRoute42 ⋯)

Equations

• Q2Presentation.Induction.MinimalBlockKernelConcreteRoute63RawHeadClosers.kmodRConcreteEquivDataOfLiteralM Rlit Mlit Tlit Clit AR AM TS = { KmodR_equiv_rawM := id Mlit.KmodR_equiv_rawM }

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute63RawHeadClosers.kmodRConcreteEquivData_from_route63Pieces {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Rlit : MinimalBlockKernelConcreteRoute43.RawFrattiniLiteralModuleObjectData K F) (Mlit : MinimalBlockKernelConcreteRoute43.RawQuotientLiteralModuleObjectData K F) (Tlit : MinimalBlockKernelConcreteRoute43.RawSubmoduleLiteralObjectData Mlit.toObject) (Clit : MinimalBlockKernelConcreteRoute43.RawLowerLiteralQuotientGroupData K F) (AR : MinimalBlockKernelConcreteRoute43.RawFrattiniTransportActionData Rlit.toObject Clit.toObject) (AM : MinimalBlockKernelConcreteRoute43.RawModuleTransportActionData Mlit.toObject Clit.toObject) (TS : MinimalBlockKernelConcreteRoute43.RawSubmoduleTransportStableData Tlit.toObject AM) : Nonempty (MinimalBlockKernelConcreteRoute42.KmodRConcreteEquivData (MinimalBlockKernelRoute60RawHead.rawDataOfPieces Rlit.toObject Mlit.toObject Tlit.toObject Clit.toObject AR.toRoute42 AM.toRoute42 ⋯))

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute63RawHeadClosers.rawDataAndKmodRConcreteEquivData_from_route63 {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : ∃ (D : MinimalBlockKernelModuleConcreteRawData K F), Nonempty (MinimalBlockKernelConcreteRoute42.KmodRConcreteEquivData D)

Exact simple-head/lower-character providers from Route43 lower forms

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute63RawHeadClosers.rawInvariantHyperplanesContainTData_from_route63 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawInvariantHyperplanesContainTData D)

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute63RawHeadClosers.rawHeadIrreducibleData_from_route63 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadIrreducibleData D)

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute63RawHeadClosers.rawHeadActionNotPointwiseTrivialData_from_route63 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadActionNotPointwiseTrivialData D)

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute63RawHeadClosers.rawLowerInvariantCharacterExistsData_from_route63 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawLowerInvariantCharacterExistsData D)

Route60-compatible raw/head transport provider

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute63RawHeadClosers.rawHeadTransportPieces_from_route63RawHeadClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelRoute60RawHead.RawHeadTransportPieces K F)

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

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute63RawHeadClosers.rawSimpleHeadSemanticData_from_route63RawHeadClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData D)