Route42 minimal-block kernel/head refinement

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

Route42 keeps the Route40 selected least kernel and the Route40 field-level Frattini collapse frontier. It refines the remaining Route41 raw quotient/head surface in two ways:

• the raw quotient transport is split into object-level R, M, T, C packets plus induced action and T-stability packets, and the concrete K/Phi(K) ~= M bridge is exposed as its own literal equivalence packet;
• head nontriviality is derived from the same raw tower's nontrivial quotient head action, and the final head/invariant layer is rebuilt from the manuscript lem:simplehead facts: invariant hyperplanes contain T, the quotient head is irreducible, its action is not pointwise trivial, and (R^vee)^C has a nonzero invariant character.

Thus the public provider below has the same target shape as minimalBlock_groupTowerData_from_kernelConcreteRoute41, while its axiom closure no longer contains the Route41 raw/head names minimalBlock_kernelModuleConcreteRawModuleObjectsData, minimalBlock_kernelModuleConcreteRawSubquotientObjectsData, minimalBlock_kernelModuleConcreteRawFrattiniActionData, minimalBlock_kernelModuleConcreteRawModuleActionData, minimalBlock_kernelModuleConcreteRawTStableData, minimalBlock_kernelModuleConcreteKmodRQuotientEquivData, minimalBlock_kernelModuleConcreteHeadNonzeroData, minimalBlock_rawInvariantFunctionalsKillTData, minimalBlock_rawHeadDualInvariantZeroData, minimalBlock_rawHeadNonzeroStableEqTopData, and minimalBlock_rawInvariantCharacterData.

The remaining old Route41 kernel leaves are the genuinely finite-group leastness and Frattini-collapse facts from Section 7.

Raw quotient objects split by manuscript role

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

Route42 raw object: the additive F_2 model of the Frattini layer R = Phi(K).

• R : Type
• acgR : AddCommGroup self.R
• modR : Module (ZMod 2) self.R
• finR : Fintype self.R
• deqR : DecidableEq self.R

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

Route42 raw object: the additive F_2 model of M = K/Phi(K).

• M : Type
• acgM : AddCommGroup self.M
• modM : Module (ZMod 2) self.M
• finM : Fintype self.M
• deqM : DecidableEq self.M

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

Route42 raw object: the submodule T = (K cap S)/Phi(K) inside M.

• T : Submodule (ZMod 2) Mobj.M

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

Route42 raw object: the lower quotient group C = Y/K.

• C : Type
• grpC : Group self.C
• finC : Finite self.C

axiom Q2Presentation.Induction.MinimalBlockKernelConcreteRoute42.rawFrattiniModuleObjectData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (RawFrattiniModuleObjectData K F)

Residual object packet for R = Phi(K).

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

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

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

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

axiom Q2Presentation.Induction.MinimalBlockKernelConcreteRoute42.rawLowerQuotientGroupData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (RawLowerQuotientGroupData K F)

Residual object packet for C = Y/K.

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute42.rawModuleObjectsOfPieces {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : RawFrattiniModuleObjectData K F) (Mobj : RawQuotientModuleObjectData K F) : MinimalBlockKernelModuleConcreteRawModuleObjectsData K F

Assemble the current raw-module-object API from the Route42 R and M object packets.

Equations

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

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute42.rawSubquotientObjectsOfPieces {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : RawFrattiniModuleObjectData K F) (Mobj : RawQuotientModuleObjectData K F) (Tobj : RawSubmoduleObjectData Mobj) (Cobj : RawLowerQuotientGroupData K F) : MinimalBlockKernelModuleConcreteRawSubquotientObjectsData (rawModuleObjectsOfPieces Robj Mobj)

Assemble the current subquotient-object API from the Route42 T and C packets.

Equations

• Q2Presentation.Induction.MinimalBlockKernelConcreteRoute42.rawSubquotientObjectsOfPieces Robj Mobj Tobj Cobj = { T := Tobj.T, C := Cobj.C, grpC := Cobj.grpC, finC := ⋯ }

Raw quotient actions split by target

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

Route42 action packet: conjugation-induced action of C on R.

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

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

Route42 action packet: conjugation-induced action of C on M.

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

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

Route42 stability packet: T is stable under the selected C-action on M.

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

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

Residual action packet on R.

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

Residual action packet on M.

axiom Q2Presentation.Induction.MinimalBlockKernelConcreteRoute42.rawSubmoduleStableData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} {Mobj : RawQuotientModuleObjectData K F} {Cobj : RawLowerQuotientGroupData K F} (Tobj : RawSubmoduleObjectData Mobj) (A : RawModuleActionData Mobj Cobj) : Nonempty (RawSubmoduleStableData Tobj A)

Residual stability packet for T.

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute42.rawFrattiniActionOfPieces {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : RawFrattiniModuleObjectData K F) (Mobj : RawQuotientModuleObjectData K F) (Tobj : RawSubmoduleObjectData Mobj) (Cobj : RawLowerQuotientGroupData K F) (A : RawFrattiniActionData Robj Cobj) : MinimalBlockKernelModuleConcreteRawFrattiniActionData (rawModuleObjectsOfPieces Robj Mobj) (rawSubquotientObjectsOfPieces Robj Mobj Tobj Cobj)

Convert the Route42 action on R to the current concrete action API.

Equations

• Q2Presentation.Induction.MinimalBlockKernelConcreteRoute42.rawFrattiniActionOfPieces Robj Mobj Tobj Cobj A = { actR := A.actR }

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute42.rawModuleActionOfPieces {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : RawFrattiniModuleObjectData K F) (Mobj : RawQuotientModuleObjectData K F) (Tobj : RawSubmoduleObjectData Mobj) (Cobj : RawLowerQuotientGroupData K F) (A : RawModuleActionData Mobj Cobj) : MinimalBlockKernelModuleConcreteRawModuleActionData (rawModuleObjectsOfPieces Robj Mobj) (rawSubquotientObjectsOfPieces Robj Mobj Tobj Cobj)

Convert the Route42 action on M to the current concrete action API.

Equations

• Q2Presentation.Induction.MinimalBlockKernelConcreteRoute42.rawModuleActionOfPieces Robj Mobj Tobj Cobj A = { actM := A.actM }

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute42.rawTStableOfPieces {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (Robj : RawFrattiniModuleObjectData K F) (Mobj : RawQuotientModuleObjectData K F) (Tobj : RawSubmoduleObjectData Mobj) (Cobj : RawLowerQuotientGroupData K F) (A : RawModuleActionData Mobj Cobj) (TS : RawSubmoduleStableData Tobj A) : MinimalBlockKernelModuleConcreteRawTStableData (rawModuleActionOfPieces Robj Mobj Tobj Cobj A)

Convert Route42 T-stability to the current concrete action API.

Equations

• ⋯ = ⋯

Literal K/Phi(K) ~= M bridge

structure Q2Presentation.Induction.MinimalBlockKernelConcreteRoute42.KmodRConcreteEquivData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : MinimalBlockKernelModuleConcreteRawData K F) : Type

Route42 bridge packet: the literal quotient K/Phi(K) realizes the raw module M.

• KmodR_equiv_rawM : ↥(Subgroup.map (QuotientGroup.mk' (Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub))) K.Ksub) ≃* Multiplicative D.M

axiom Q2Presentation.Induction.MinimalBlockKernelConcreteRoute42.kmodRConcreteEquivData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : MinimalBlockKernelModuleConcreteRawData K F) : Nonempty (KmodRConcreteEquivData D)

Residual literal quotient-equivalence packet.

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute42.KmodRConcreteEquivData.bridgeData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} {D : MinimalBlockKernelModuleConcreteRawData K F} (B : KmodRConcreteEquivData D) : MinimalBlockKernelModuleConcreteBridgeData D

Convert the Route42 bridge packet to the current bridge API.

Equations

• B.bridgeData = { KmodR_equiv_rawM := B.KmodR_equiv_rawM }

Simple-head Route42 residuals

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

Route42 head leaf: invariant hyperplanes in M contain T.

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

Route42 head leaf: the quotient head has no nonzero proper stable submodule.

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

Route42 head leaf: the quotient-head action is not pointwise trivial.

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

Route42 lower-Frattini leaf: (R^vee)^C has a nonzero invariant character.

def Q2Presentation.Induction.MinimalBlockKernelConcreteRoute42.headDataOfNotPointwiseTrivial {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : MinimalBlockKernelModuleConcreteRawData K F) (A : MinimalBlockRawHeadActionNotPointwiseTrivialData D.rawTowerData) : MinimalBlockKernelModuleConcreteHeadData D

Concrete head nontriviality follows from the same raw tower's nontrivial quotient-head action.

Equations

• ⋯ = ⋯

Raw quotient transport from Route42 packets

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

Raw quotient tower assembled from Route42 object/action/equivalence packets, with head nontriviality derived from the same raw tower's nontrivial action.

Concrete provenance through the Route42 raw transport

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

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

Route42 simple-head/invariant conversions

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

Invariant functionals kill T, through the Route42 hyperplane packet.

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

The nonzero-stable criterion follows from Route42 irreducibility.

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

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

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

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

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

Head simplicity through the Route42 irreducibility packet.

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

Raw invariant character through the Route42 lower invariant-character existence packet.

Route-ready group tower

theorem Q2Presentation.Induction.MinimalBlockKernelConcreteRoute42.provenanceConcreteFinalPieces_from_route42 {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockProvenanceConcreteFinalPieces chief)

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

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

Route42 provenance-semantic data with the Route41 raw/head leaves refined.

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

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

Public Route42 aliases

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

Route42 replacement for the Route41 concrete provenance assembly.

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

Route42 replacement for the Route41 provenance-semantic packet.

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

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