Route146 Section 7 kernel raw Route43 closers #

This route-neutral sidecar leaves Route145 and all integrated files untouched. It supplies Route145-shape replacements for the two raw/head providers whose Route145 axiom closure still exposed the Route43 literal/raw/head atoms.

The raw quotient tower is assembled from the Route141-owned lower literal object/equivalence/action-family packets. The simple-head semantic packet is assembled from the lower head no-trivial, head-simplicity, head-nontrivial, and lower-scalar quotient packets rather than from the Route43 head atoms.

Lower raw object/action bridge #

source

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

Nonempty (MinimalBlockKernelRoute78RawObjectClosers.RawObjectActionBridgeData K F)

Route146 raw object/action bridge.

This is the concrete raw quotient/module/action part of the Route145 raw tower, but routed through the Route141 lower fields instead of the Route43 literal atoms.

Lower simple-head projections #

source

theorem Q2Presentation.Induction.Section7KernelRoute146RawClosers.rawInvariantHyperplanesContainTData_from_route146HeadSplit {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) :

Nonempty (MinimalBlockRawInvariantHyperplanesContainTData D)

Invariant hyperplanes contain T, derived from the no-trivial-dual head packet rather than the Route43 maximal-submodule atom.

source

theorem Q2Presentation.Induction.Section7KernelRoute146RawClosers.rawHeadNonzeroStableEqTopData_from_route146HeadSplit {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) :

Nonempty (MinimalBlockRawHeadNonzeroStableEqTopData D)

The quotient-head nonzero-stable criterion, derived from the lower head simplicity packet rather than the Route43 orbit-span atom.

source

theorem Q2Presentation.Induction.Section7KernelRoute146RawClosers.rawHeadActionNotPointwiseTrivialData_from_route146HeadSplit {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) :

Nonempty (MinimalBlockRawHeadActionNotPointwiseTrivialData D)

Not-pointwise-trivial head action, derived from the no-trivial-dual packet, head nontriviality, and head simplicity rather than the Route43 action witness.

source

theorem Q2Presentation.Induction.Section7KernelRoute146RawClosers.rawLowerInvariantCharacterExistsData_from_route146LowerScalar {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) :

Nonempty (MinimalBlockRawLowerInvariantCharacterExistsData D)

Existential lower invariant character, derived from the lower scalar quotient packet rather than the Route43 selected-character atom.

Route145-shape replacement providers #

source

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

Nonempty (MinimalBlockKernelRawQuotientTowerData K F)

Route146 replacement for Section7KernelRoute145ActualClosers.minimalBlock_kernelRawQuotientTowerData_from_section7KernelRoute145ActualClosers.

The raw objects/actions/bridge come from Route141 lower literal fields, and the nonzero head is obtained from the Route146 lower head split.

source

theorem Q2Presentation.Induction.Section7KernelRoute146RawClosers.rawSimpleHeadSemanticData_from_section7KernelRoute146RawClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) :

Nonempty (MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData D)

Route146 replacement for Section7KernelRoute145ActualClosers.rawSimpleHeadSemanticData_from_section7KernelRoute145ActualClosers.

This exports the same Route44 semantic shape while replacing the Route43 maximal/orbit/action-witness/lower-character atoms by lower head and lower scalar packets.

source

theorem Q2Presentation.Induction.Section7KernelRoute146RawClosers.minimalBlock_invariantActualProofs2Data_from_section7KernelRoute146RawClosers_lower {p : FramedPair} {chief : NonScalarChiefFactor p} (lower : MinimalBlockLowerGroupModuleData chief) :

Nonempty (MinimalBlockInvariantActualProofs2Data lower.rawTowerData)

Selected-lower invariant packet through the Route146 raw/head lowering.