Route43 minimal-block kernel/head refinement

This sidecar is standalone: no routed or root file imports it yet.

Route43 keeps the Route42 target shape but avoids the Route42 residual constants in the public provider. The replacement surface is closer to the manuscript Section 7 tower:

• raw R, M, and C objects are carried with literal identifications to Phi(K), K/Phi(K), and Y/K;
• raw actions and T-stability are carried as route43 transport packets and converted through Route42's definitional adapters;
• the quotient bridge K/Phi(K) ~= M is supplied by the literal M packet, so MinimalBlockKernelConcreteRoute42.kmodRConcreteEquivData is not used;
• the hyperplane conclusion is proved from the manuscript maximal-submodule form in the proof of lem:simplehead;
• quotient-head irreducibility is taken in orbit-span form, the nontrivial action in witness form, and the lower invariant character in chosen-character form.

The finite-group collapse leaves from lem:collapse and the leastness leaf are unchanged; those remain the hard Section 7 group-theoretic inputs.

Literal raw quotient objects

structure Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.RawFrattiniLiteralModuleObjectData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Type 1

Route43 literal object for R = Phi(K): the abstract F_2 object is identified with the literal Frattini subgroup of the selected kernel.

• toObject : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F
• frattini_equiv_rawR : ↥(Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub)) ≃* Multiplicative self.toObject.R

structure Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.RawQuotientLiteralModuleObjectData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Type 1

Route43 literal object for M = K/Phi(K): the abstract F_2 object is identified with the literal quotient used by the bridge.

• toObject : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F
• KmodR_equiv_rawM : ↥(Subgroup.map (QuotientGroup.mk' (Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub))) K.Ksub) ≃* Multiplicative self.toObject.M

structure Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.RawSubmoduleLiteralObjectData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) : Type

Route43 literal object for T = (K cap S)/Phi(K) inside M.

• toObject : MinimalBlockKernelConcreteRoute42.RawSubmoduleObjectData Mobj

structure Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.RawLowerLiteralQuotientGroupData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Type 1

Route43 literal object for C = Y/K: the abstract quotient group is identified with the literal quotient by the selected kernel.

• toObject : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F
• quotient_equiv_C : p.fst.Y ⧸ K.Ksub ≃* self.toObject.C

axiom Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.rawFrattiniLiteralModuleObjectData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (RawFrattiniLiteralModuleObjectData K F)

Residual literal R = Phi(K) object packet.

axiom Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.rawQuotientLiteralModuleObjectData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (RawQuotientLiteralModuleObjectData K F)

Residual literal M = K/Phi(K) object packet.

axiom Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.rawSubmoduleLiteralObjectData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) : Nonempty (RawSubmoduleLiteralObjectData Mobj)

Residual literal T = (K cap S)/Phi(K) object packet.

axiom Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.rawLowerLiteralQuotientGroupData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (RawLowerLiteralQuotientGroupData K F)

Residual literal C = Y/K quotient-group packet.

Raw quotient actions in transport form

structure Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.RawFrattiniTransportActionData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F) (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) : Type

Route43 transport action on the literal Frattini layer R.

• actR : Cobj.C →* Robj.R ≃ₗ[ZMod 2] Robj.R

structure Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.RawModuleTransportActionData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) : Type

Route43 transport action on the elementary quotient M.

• actM : Cobj.C →* Mobj.M ≃ₗ[ZMod 2] Mobj.M

structure Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.RawSubmoduleTransportStableData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} {Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F} {Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F} (Tobj : MinimalBlockKernelConcreteRoute42.RawSubmoduleObjectData Mobj) (A : RawModuleTransportActionData Mobj Cobj) : Prop

Route43 transport stability of T under the action on M.

• T_stable (c : Cobj.C) (m : Mobj.M) : m ∈ Tobj.T → (A.actM c) m ∈ Tobj.T

axiom Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.rawFrattiniTransportActionData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F) (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) : Nonempty (RawFrattiniTransportActionData Robj Cobj)

Residual transported action on R.

axiom Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.rawModuleTransportActionData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F) (Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F) : Nonempty (RawModuleTransportActionData Mobj Cobj)

Residual transported action on M.

axiom Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.rawSubmoduleTransportStableData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} {Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F} {Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F} (Tobj : MinimalBlockKernelConcreteRoute42.RawSubmoduleObjectData Mobj) (A : RawModuleTransportActionData Mobj Cobj) : Nonempty (RawSubmoduleTransportStableData Tobj A)

Residual transported T-stability packet.

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.RawFrattiniTransportActionData.toRoute42 {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} {Robj : MinimalBlockKernelConcreteRoute42.RawFrattiniModuleObjectData K F} {Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F} (A : RawFrattiniTransportActionData Robj Cobj) : MinimalBlockKernelConcreteRoute42.RawFrattiniActionData Robj Cobj

Equations

• A.toRoute42 = { actR := A.actR }

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.RawModuleTransportActionData.toRoute42 {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} {Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F} {Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F} (A : RawModuleTransportActionData Mobj Cobj) : MinimalBlockKernelConcreteRoute42.RawModuleActionData Mobj Cobj

Equations

• A.toRoute42 = { actM := A.actM }

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.RawSubmoduleTransportStableData.toRoute42 {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} {Mobj : MinimalBlockKernelConcreteRoute42.RawQuotientModuleObjectData K F} {Cobj : MinimalBlockKernelConcreteRoute42.RawLowerQuotientGroupData K F} {Tobj : MinimalBlockKernelConcreteRoute42.RawSubmoduleObjectData Mobj} {A : RawModuleTransportActionData Mobj Cobj} (TS : RawSubmoduleTransportStableData Tobj A) : MinimalBlockKernelConcreteRoute42.RawSubmoduleStableData Tobj A.toRoute42

Equations

• ⋯ = ⋯

Simple-head route43 refinements

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.rawMStable {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) (U : Submodule (ZMod 2) D.M) : Prop

Stability of a submodule of M under the transported C-action.

Equations

• Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.rawMStable D U = ∀ (c : D.C), ∀ m ∈ U, (D.actM c) m ∈ U

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

Manuscript maximal-submodule form used in the proof of lem:simplehead: every maximal C-stable submodule of M contains T.

• T_le_of_maximal_stable (U : Submodule (ZMod 2) D.M) : U ≠ ⊤ → (∀ (W : Submodule (ZMod 2) D.M), U < W → W = ⊤) → rawMStable D U → D.T ≤ U

axiom Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.rawInvariantMaximalSubmodulesContainTData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (RawInvariantMaximalSubmodulesContainTData D)

Residual maximal-submodule packet for the first non-scalar layer.

axiom Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.rawHeadOrbitSpansData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadOrbitSpansData D)

Residual orbit-span form of quotient-head irreducibility.

axiom Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.rawHeadActionNontrivialData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadActionNontrivialData D)

Residual witness-form nontriviality of the quotient-head action.

axiom Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.rawLowerNonzeroInvariantCharacterData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawLowerNonzeroInvariantCharacterData D)

Residual chosen-character form of the lower invariant character.

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.rawInvariantHyperplanesContainTDataOfMaximal {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (H : RawInvariantMaximalSubmodulesContainTData D) : MinimalBlockRawInvariantHyperplanesContainTData D

The maximal-submodule form of lem:simplehead implies that invariant hyperplanes contain T.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.rawHeadIrreducibleDataOfOrbitSpans {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (S : MinimalBlockRawHeadOrbitSpansData D) : MinimalBlockRawHeadIrreducibleData D

The orbit-span form implies the irreducibility packet used by Route42.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.rawHeadActionNotPointwiseTrivialDataOfWitness {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (A : MinimalBlockRawHeadActionNontrivialData D) : MinimalBlockRawHeadActionNotPointwiseTrivialData D

A witness of nontrivial action implies not-pointwise-triviality.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.rawLowerInvariantCharacterExistsDataOfNonzero {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} (X : MinimalBlockRawLowerNonzeroInvariantCharacterData D) : MinimalBlockRawLowerInvariantCharacterExistsData D

A chosen nonzero invariant character implies the existential packet.

Equations

• ⋯ = ⋯

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

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.rawHeadIrreducibleData_from_route43 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadIrreducibleData D)

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.rawHeadActionNotPointwiseTrivialData_from_route43 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawHeadActionNotPointwiseTrivialData D)

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.rawLowerInvariantCharacterExistsData_from_route43 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawLowerInvariantCharacterExistsData D)

Raw quotient transport from Route43 packets

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.rawQuotientTowerData_from_route43Transport {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelRawQuotientTowerData K F)

Raw quotient tower assembled from Route43 literal/transport packets.

Concrete provenance and Route43 simple-head/invariant conversions

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

Route43 concrete provenance: Route40 least/Frattini data plus Route43 raw quotient transport.

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

Invariant functionals kill T, through the Route43 maximal-submodule packet.

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

The nonzero-stable criterion follows from Route43 orbit spanning.

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

The quotient head has no invariant dual functional, through Route43 orbit spanning plus the nontrivial-action witness.

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

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

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

Head simplicity through the Route43 orbit-span packet.

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

Raw invariant character through the Route43 chosen-character packet.

Route-ready group tower

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute43.provenanceConcreteFinalPieces_from_route43 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockProvenanceConcreteFinalPieces chief)

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

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

Route43 provenance-semantic data with the Route42 namespace leaves removed.

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

Route43 group tower through the lowered Section 7 kernel/head route.

Public Route43 aliases

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

Route43 replacement for the Route42 concrete provenance assembly.

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

Route43 replacement for the Route42 provenance-semantic packet.

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

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