Route38 minimal-block kernel/head refinement

Route37 exposes the Section 7 kernel/head frontier through five concrete K/Phi(K) tower packets and four raw head/scalar packets. This sidecar keeps the routed files untouched and exports a drop-in group-tower provider whose closure replaces those nine names by narrower manuscript-shaped obligations:

• least K over the selected chief factor;
• the five Frattini-centralizer collapse conclusions for the literal Phi(K);
• raw R, M, T, C objects and induced actions on the same tower;
• the semantic K/Phi(K) ~= M bridge and nonzero head;
• the simple-head hyperplane, irreducibility, nontrivial-action, and lower invariant-character statements used in the proof of lem:simplehead.

The manuscript proves these facts from the finite target tower. At the current formalization frontier they remain residual packets, but they are strictly closer to the text than the Route37 concrete/raw-head aggregate leaves.

Concrete provenance from split kernel-module packets

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute38.kernelModuleConcreteProvenanceData_from_splitKernelClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Route38 concrete provenance for the selected K/R tower.

This is the Route37 provenance assembly with the five Route37 concrete residual names replaced by the finer split packets in MinimalBlockKernelModuleConcreteClosers2.

Route38 simple-head/scalar residuals

axiom Q2Presentation.Induction.MinimalBlockKernelConcreteRoute38.rawInvariantHyperplanesContainTData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawInvariantHyperplanesContainTData D)

Route38 residual: invariant hyperplanes contain the lower layer T.

This is the first minimality conclusion in manuscript lem:simplehead; it is used to show invariant functionals on M kill T.

axiom Q2Presentation.Induction.MinimalBlockKernelConcreteRoute38.rawHeadIrreducibleData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadIrreducibleData D)

Route38 residual: the quotient head has no nonzero proper stable submodule.

axiom Q2Presentation.Induction.MinimalBlockKernelConcreteRoute38.rawHeadActionNotPointwiseTrivialData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadActionNotPointwiseTrivialData D)

Route38 residual: the quotient-head action is not pointwise trivial.

axiom Q2Presentation.Induction.MinimalBlockKernelConcreteRoute38.rawLowerInvariantCharacterExistsData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawLowerInvariantCharacterExistsData D)

Route38 residual: the lower Frattini layer has a nonzero invariant character.

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute38.rawInvariantFunctionalsKillTData_from_route38 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawInvariantFunctionalsKillTData D)

Invariant functionals kill T, through the Route38 hyperplane packet.

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute38.rawHeadNonzeroStableEqTopData_from_route38 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadNonzeroStableEqTopData D)

The Route37 nonzero-stable criterion follows from Route38 irreducibility.

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute38.rawHeadDualInvariantZeroData_from_route38 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadDualInvariantZeroData D)

The quotient head has no invariant dual functional, through Route38 irreducibility plus nontrivial action.

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute38.rawLowerScalarQuotientData_from_route38 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawLowerScalarQuotientData D)

The lower scalar quotient follows from the Route38 invariant character.

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute38.dualInvariantVanishesData_from_route38 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockDualInvariantVanishesData D)

Direct dual-invariant vanishing through the Route38 head-dual split.

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute38.rawHeadSimplicityActualData_from_route38 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadSimplicityActualData D)

Head simplicity through the Route38 irreducibility packet.

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute38.rawInvariantCharacterData_from_route38 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawInvariantCharacterData D)

Raw invariant character through the Route38 lower scalar split.

Route-ready group tower

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute38.provenanceConcreteFinalPieces_from_route38 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockProvenanceConcreteFinalPieces chief)

Concrete-final provenance through the Route38 kernel and simple-head split.

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute38.provenanceSemanticData_from_route38 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockProvenanceSemanticData chief)

Route38 provenance-semantic replacement for the Route37 provider.

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

Route38 group tower through the finer Section 7 kernel/head split.

Public route38 aliases

theorem Q2Presentation.Induction.minimalBlock_kernelModuleConcreteProvenanceData_from_kernelConcreteRoute38 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Route38 replacement for the Route37 concrete provenance assembly.

theorem Q2Presentation.Induction.minimalBlock_provenanceSemanticData_from_kernelConcreteRoute38 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockProvenanceSemanticData chief)

Route38 replacement for the Route37 provenance-semantic packet.

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

Route38 replacement for the Route37 minimal-block group-tower provider.