Route112 invariant-packet closers

This sidecar leaves IntegratedCurrentRouteProofs112 untouched. It targets the compact Route112 kernel invariant residual

• minimalBlock_invariantActualProofs2Data.

The replacement below rebuilds that actual packet from the same raw-head semantic fields used by the Route63/Route106 head lowering:

• invariant hyperplanes contain T;
• every nonzero stable quotient-head submodule is top;
• the quotient-head action is not pointwise trivial;
• the lower Frattini layer has a nonzero invariant character.

Thus the theorem has the old packet target, but its axiom closure is the smaller manuscript-shaped raw-head frontier rather than the monolithic minimalBlock_invariantActualProofs2Data axiom.

Actual packet from the raw-head semantic packet

def Q2Presentation.Induction.MinimalBlockInvariantRoute112Closers.rawHeadSimpleNoTrivialActualData_of_rawSimpleHeadSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (S : MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData D) : MinimalBlockRawHeadSimpleNoTrivialActualData D

Convert the Route63/Route44 semantic simple-head packet into the stronger head component used by MinimalBlockInvariantActualProofs2Data.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockInvariantRoute112Closers.rawLowerInvariantCharacterActualData_of_rawSimpleHeadSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (S : MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData D) : MinimalBlockRawLowerInvariantCharacterActualData D

Convert the existential lower-character field into the actual character field used by MinimalBlockInvariantActualProofs2Data.

Equations

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

def Q2Presentation.Induction.MinimalBlockInvariantRoute112Closers.invariantActualProofs2Data_of_rawSimpleHeadSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (S : MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData D) : MinimalBlockInvariantActualProofs2Data D

Reassemble the old actual invariant packet from a same-tower raw-head semantic packet.

Equations

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

Route112-ready providers

theorem Q2Presentation.Induction.MinimalBlockInvariantRoute112Closers.invariantActualProofs2Data_from_route112Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockInvariantActualProofs2Data D)

Route112 replacement for minimalBlock_invariantActualProofs2Data.

The target is the old actual packet, but the proof goes through the Route63 raw-head semantic fields, so the closure does not contain the monolithic minimalBlock_invariantActualProofs2Data axiom.

theorem Q2Presentation.Induction.MinimalBlockInvariantRoute112Closers.invariantActualProofs2Data_from_route112Lower {p : FramedPair} {chief : NonScalarChiefFactor p} (lower : MinimalBlockLowerGroupModuleData chief) : Nonempty (MinimalBlockInvariantActualProofs2Data lower.rawTowerData)

Selected-lower-tower form for the current Route112 kernel route.

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

Compact Route112 kernel provider with the invariant packet lowered through the raw-head semantic fields. The lower tower is the same one selected by the current Route112 raw-head closer.

Public aliases

theorem Q2Presentation.Induction.minimalBlock_invariantActualProofs2Data_from_route112Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockInvariantActualProofs2Data D)

Public Route112 replacement for the monolithic actual invariant packet.

theorem Q2Presentation.Induction.minimalBlock_invariantActualProofs2Data_from_route112Lower {p : FramedPair} {chief : NonScalarChiefFactor p} (lower : MinimalBlockLowerGroupModuleData chief) : Nonempty (MinimalBlockInvariantActualProofs2Data lower.rawTowerData)

Public selected-lower-tower Route112 replacement for the monolithic actual invariant packet.

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

Public compact Route112 kernel provider with the invariant packet lowered.