Route44 minimal-block kernel/raw tower cleanup

This sidecar is route-neutral: no routed/root file imports it yet.

Route43 exposes the Section 7 kernel/head frontier through many independent literal/raw packets. Route44 keeps the Route43 target shape, but routes the kernel/module tower through the coherent manuscript packets already present in the tree:

• the route26 upper-candidate least-kernel construction, so the only remaining least-kernel content is the universal leastness packet;
• the full lem:collapse Frattini packet for the selected K;
• the same-tower raw quotient/action/bridge/head packet for R, M, T, and C;
• one same-raw-tower semantic lem:simplehead packet, rather than the Route43 maximal/orbit/witness/character leaves.

Thus the public Route44 provider avoids the Route43 namespace-local raw/literal leaves and the split Frattini pointwise leaves in its axiom closure. The remaining residuals are the coherent manuscript-shaped Section 7 packets.

Same-tower simple-head semantic packet

structure Q2Presentation.Induction.MinimalBlockKernelConcreteRoute44.RawSimpleHeadSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Prop

Route44 semantic simple-head packet for the fixed raw tower.

This is the manuscript lem:simplehead interface in the form needed downstream: invariant hyperplanes contain T, nonzero stable submodules of the head are top, the head action is not pointwise trivial, and the lower Frattini layer has a nonzero invariant character. Bundling these fields prevents downstream assembly from mixing head facts attached to different raw towers.

• invariantHyperplanes : MinimalBlockRawInvariantHyperplanesContainTData D
• headNonzeroStable : MinimalBlockRawHeadNonzeroStableEqTopData D
• headActionNotPointwiseTrivial : MinimalBlockRawHeadActionNotPointwiseTrivialData D
• lowerInvariantCharacter : MinimalBlockRawLowerInvariantCharacterExistsData D

axiom Q2Presentation.Induction.MinimalBlockKernelConcreteRoute44.rawSimpleHeadSemanticData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (RawSimpleHeadSemanticData D)

Residual same-tower lem:simplehead packet.

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute44.rawInvariantHyperplanesContainTData_from_route44 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawInvariantHyperplanesContainTData D)

Route44 closes the Route43 maximal-submodule detour by using the direct hyperplane form.

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute44.rawHeadOrbitSpansData_from_route44 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadOrbitSpansData D)

Route44 orbit-span packet from the simple-head nonzero-stable criterion.

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute44.rawHeadActionNontrivialData_from_route44 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadActionNontrivialData D)

Route44 witness-form nontriviality from not-pointwise-triviality.

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute44.rawLowerNonzeroInvariantCharacterData_from_route44 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawLowerNonzeroInvariantCharacterData D)

Route44 chosen-character packet from the existential lower-character form.

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

Invariant functionals kill T through the direct hyperplane form.

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

The quotient head has no invariant dual functional through the Route44 same-tower simple-head packet.

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

Direct dual-invariant vanishing through the Route44 simple-head packet.

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

Head simplicity through the Route44 nonzero-stable criterion.

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

Raw invariant-character data through the Route44 lower-character field.

Kernel/raw tower through coherent manuscript packets

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute44.frattiniData_from_route44Collapse {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniData K)

Route44 Frattini data from the coherent lem:collapse packet.

This avoids the Route43/Route40 split leaves minimalBlock_kernelModuleConcreteFrattiniNonidentityData, minimalBlock_kernelModuleConcreteFrattiniCentralData, minimalBlock_kernelModuleConcreteFourthPowerData, and minimalBlock_kernelModuleConcreteFrattiniExponentData.

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

Concrete provenance through the Route44 least/collapse/raw tower route.

Route-ready group tower

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute44.provenanceConcreteFinalPieces_from_route44 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockProvenanceConcreteFinalPieces chief)

Concrete-final provenance through Route44 kernel/raw/head packets.

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

Route44 provenance-semantic data.

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

Route44 group tower through the coherent Section 7 kernel/raw route.

Public Route44 aliases

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

Route44 replacement for the Route43 concrete provenance assembly.

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

Route44 replacement for the Route43 provenance-semantic packet.

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

Drop-in Route44 provider for the minimal-block group tower.