Route29 minimal-block kernel/head refinement #

Route28 keeps the concrete K, Phi(K), R, M, T, C tower split into the current Section 7 kernel/module leaves, and replaces the old monolithic actual invariant packet by the four route28 head/lower leaves.

This sidecar keeps the same downstream route28 shape, but rebuilds those route28 head/lower leaves on the selected raw quotient tower from the smaller route21-style semantic packets:

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

The same not-pointwise-trivial head action also supplies the concrete nonzero-head field of the raw quotient tower, so the provider no longer depends on minimalBlock_kernelModuleConcreteHeadNonzeroData.

Route29 same-raw-tower head/lower assembly #

source

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute29.headNontrivialOfRawQuotient {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Q : MinimalBlockKernelRawQuotientTowerData K F) :

MinimalBlockHeadNontrivialData Q.rawData.rawTowerData

The concrete raw quotient tower carries the nontrivial-head packet on the same raw tower.

Equations

⋯ = ⋯

Instances For

source

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute29.rawHeadQuotientNoTrivialOfRoute21Split {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (H : MinimalBlockRawInvariantHyperplanesContainTData D) (S : MinimalBlockRawHeadNonzeroStableEqTopData D) (A : MinimalBlockRawHeadActionNotPointwiseTrivialData D) :

MinimalBlockRawHeadQuotientNoTrivialData D

Route29 replacement for the route28 quotient-head no-trivial packet.

It is assembled from the radical-killing hyperplane statement, the nonzero-stable simple-head criterion, and the nontrivial quotient-head action.

Equations

⋯ = ⋯

Instances For

source

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute29.rawHeadSimplicityActualOfRoute21Split {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (S : MinimalBlockRawHeadNonzeroStableEqTopData D) :

MinimalBlockRawHeadSimplicityActualData D

Route29 replacement for the route28 quotient-head simplicity packet.

Equations

⋯ = ⋯

Instances For

source

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute29.rawLowerScalarQuotientOfRoute21Split {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (X : MinimalBlockRawLowerInvariantCharacterExistsData D) :

MinimalBlockRawLowerScalarQuotientData D

Route29 replacement for the route28 lower scalar quotient packet.

Equations

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

Instances For

source

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute29.invariantActualOfRoute21Split {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (N : MinimalBlockHeadNontrivialData D) (H : MinimalBlockRawInvariantHyperplanesContainTData D) (S : MinimalBlockRawHeadNonzeroStableEqTopData D) (A : MinimalBlockRawHeadActionNotPointwiseTrivialData D) (X : MinimalBlockRawLowerInvariantCharacterExistsData D) :

MinimalBlockInvariantActualProofs2Data D

Assemble the actual invariant packet on one fixed raw tower from the route29 head/lower split.

Equations

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

Instances For

Route29 packet and projections #

source

structure Q2Presentation.Induction.MinimalBlockKernelConcreteRoute29Data {p : FramedPair} (chief : NonScalarChiefFactor p) :

Type 1

Route29 coherent Section 7 kernel/head packet.

The fields intentionally match route28, but the assembly theorem below constructs rawQuotient.head from not-pointwise-trivial head action and constructs invariantActual from the route29 head/lower split rather than from the route28 direct leaves.