Route83 kernel closers for the minimal-block route #

This sidecar keeps the Route82 least/Frattini and raw R,M,T,C tower assembly, but lowers the simple-head part of the current Route84 kernel frontier.

Route82 obtains the Route44 simple-head semantic packet from four Route43 residual packets:

maximal invariant submodules contain T;
orbit spans on the quotient head;
a nontrivial head-action witness;
a selected lower invariant character.

Route83 instead builds the same semantic packet from the coherent same-raw-tower actual invariant packet minimalBlock_invariantActualProofs2Data. This avoids the four Route43 raw-head residual names in the group-tower provider closure while preserving the same Route55 consumer interface.

Same-tower actual simple-head projections #

source

theorem Q2Presentation.Induction.MinimalBlockKernelRoute83Closers.rawInvariantHyperplanesContainTData_from_route83 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) :

Nonempty (MinimalBlockRawInvariantHyperplanesContainTData D)

Route83 direct hyperplane form from the same-raw-tower actual packet.

This is the field consumed by Route44; it avoids the Route43 rawInvariantMaximalSubmodulesContainTData residual.

source

theorem Q2Presentation.Induction.MinimalBlockKernelRoute83Closers.rawHeadNonzeroStableEqTopData_from_route83 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) :

Nonempty (MinimalBlockRawHeadNonzeroStableEqTopData D)

Route83 nonzero-stable quotient-head criterion from the actual simple-head packet.

This is the Route44 field consumed downstream, so Route83 does not need the Route43 orbit-span residual.

source

theorem Q2Presentation.Induction.MinimalBlockKernelRoute83Closers.rawHeadActionNotPointwiseTrivialData_from_route83 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) :

Nonempty (MinimalBlockRawHeadActionNotPointwiseTrivialData D)

Route83 not-pointwise-trivial head action from the actual witness.

This avoids the Route43 selected witness residual in the provider closure.

source

theorem Q2Presentation.Induction.MinimalBlockKernelRoute83Closers.rawLowerInvariantCharacterExistsData_from_route83 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) :

Nonempty (MinimalBlockRawLowerInvariantCharacterExistsData D)

Route83 existential lower-character field from the actual character hitting 1.

This avoids the Route43 selected-character residual in the provider closure.

source

theorem Q2Presentation.Induction.MinimalBlockKernelRoute83Closers.rawSimpleHeadSemanticData_from_route83 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) :

Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData D)

Route83 same-tower simple-head semantic packet.

The four fields are all projected from minimalBlock_invariantActualProofs2Data, so the old Route43 raw-head packets are not in this theorem's axiom closure.