Concrete refinements for the route8 kernel/Frattini/raw residuals

This sidecar does not edit routed files. It refines the three route8 P3 residuals

• minimalBlock_kernelLeastOverChiefData;
• minimalBlock_kernelFrattiniCollapseFullData;
• minimalBlock_kernelRawQuotientTowerData;

into smaller manuscript-shaped packets on the same Section 7 tower.

The file proves theorem-level replacements for the old three packet shapes, and then reassembles the route-ready lower/module and group-tower theorems through those replacements. The remaining axioms in the replacement route are the finer least-candidate/minimality, Frattini-collapse, raw-object/action, bridge, and head-nonzero packets below.

Least kernel split

axiom Q2Presentation.Induction.minimalBlock_kernelLeastCandidateData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelCandidateData chief)

Candidate part of the least-kernel choice: a normal K <= P with K S = P.

The universal leastness is kept in a separate packet below.

structure Q2Presentation.Induction.MinimalBlockKernelLeastUniversalData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelCandidateData chief) : Prop

Universal leastness for a fixed candidate kernel.

• minimal_K (K' : Subgroup p.fst.Y) : K'.Normal → K' ≤ chief.upper → K' ⊔ chief.lower = chief.upper → K.Ksub ≤ K'

axiom Q2Presentation.Induction.minimalBlock_kernelLeastUniversalData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelCandidateData chief) : Nonempty (MinimalBlockKernelLeastUniversalData K)

Residual: prove universal leastness for the selected candidate kernel.

theorem Q2Presentation.Induction.minimalBlock_kernelLeastOverChiefData_from_frattiniConcreteProofs {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelLeastOverChiefData chief)

Replacement for minimalBlock_kernelLeastOverChiefData, split into a candidate kernel and its universal leastness proof.

Frattini-collapse refinement

theorem Q2Presentation.Induction.minimalBlock_kernelModuleConcreteFrattiniNormalData_from_frattiniConcreteProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniNormalData K)

The literal Frattini subgroup of the selected least kernel is normal in the ambient target group.

structure Q2Presentation.Induction.MinimalBlockKernelModuleConcreteFrattiniNonidentityData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Prop

Witness-form nontriviality of the literal Frattini layer.

• exists_nonidentity : ∃ r ∈ Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub), r ≠ 1

axiom Q2Presentation.Induction.minimalBlock_kernelModuleConcreteFrattiniNonidentityData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniNonidentityData K)

Residual: the literal Frattini layer contains a nonidentity element.

def Q2Presentation.Induction.MinimalBlockKernelModuleConcreteFrattiniNontrivialData.ofNonidentity {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (W : MinimalBlockKernelModuleConcreteFrattiniNonidentityData K) : MinimalBlockKernelModuleConcreteFrattiniNontrivialData K

Convert witness-form nontriviality into the existing cardinal packet.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.minimalBlock_kernelModuleConcreteFrattiniNontrivialData_from_frattiniConcreteProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelModuleConcreteFrattiniNontrivialData K)

The current nontriviality packet follows from a nonidentity Frattini witness.

theorem Q2Presentation.Induction.minimalBlock_kernelFrattiniCollapseFullData_from_frattiniConcreteProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) : Nonempty (MinimalBlockKernelFrattiniCollapseFullData K)

Replacement for minimalBlock_kernelFrattiniCollapseFullData, assembled from theorem-level normality, witness-form nontriviality, and the remaining pointwise collapse conclusions.

Raw object/action split

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

The finite F_2 objects R and M from the fixed K, Phi(K) tower.

• R : Type
• acgR : AddCommGroup self.R
• modR : Module (ZMod 2) self.R
• finR : Fintype self.R
• deqR : DecidableEq self.R
• M : Type
• acgM : AddCommGroup self.M
• modM : Module (ZMod 2) self.M
• finM : Fintype self.M
• deqM : DecidableEq self.M

structure Q2Presentation.Induction.MinimalBlockKernelModuleConcreteRawSubquotientObjectsData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (O : MinimalBlockKernelModuleConcreteRawModuleObjectsData K F) : Type 1

The submodule T and lower quotient group C from the same fixed tower.

• T : Submodule (ZMod 2) O.M
• C : Type
• grpC : Group self.C
• finC : Finite self.C

axiom Q2Presentation.Induction.minimalBlock_kernelModuleConcreteRawModuleObjectsData {p : FramedPair} {chief : NonScalarChiefFactor p} (K : MinimalBlockKernelLeastOverChiefData chief) (F : MinimalBlockKernelModuleConcreteFrattiniData K) : Nonempty (MinimalBlockKernelModuleConcreteRawModuleObjectsData K F)

Residual: construct the raw module objects R and M.

axiom Q2Presentation.Induction.minimalBlock_kernelModuleConcreteRawSubquotientObjectsData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (O : MinimalBlockKernelModuleConcreteRawModuleObjectsData K F) : Nonempty (MinimalBlockKernelModuleConcreteRawSubquotientObjectsData O)

Residual: construct T and C for the selected raw R,M.

def Q2Presentation.Induction.MinimalBlockKernelModuleConcreteRawObjectsData.ofModuleSubquotient {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (O : MinimalBlockKernelModuleConcreteRawModuleObjectsData K F) (S : MinimalBlockKernelModuleConcreteRawSubquotientObjectsData O) : MinimalBlockKernelModuleConcreteRawObjectsData K F

Assemble the current raw-object packet from the two object-level packets.

Equations

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

structure Q2Presentation.Induction.MinimalBlockKernelModuleConcreteRawFrattiniActionData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (O : MinimalBlockKernelModuleConcreteRawModuleObjectsData K F) (S : MinimalBlockKernelModuleConcreteRawSubquotientObjectsData O) : Type

The induced action on the Frattini layer R.

• actR : S.C →* O.R ≃ₗ[ZMod 2] O.R

structure Q2Presentation.Induction.MinimalBlockKernelModuleConcreteRawModuleActionData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (O : MinimalBlockKernelModuleConcreteRawModuleObjectsData K F) (S : MinimalBlockKernelModuleConcreteRawSubquotientObjectsData O) : Type

The induced action on the elementary quotient M.

• actM : S.C →* O.M ≃ₗ[ZMod 2] O.M

structure Q2Presentation.Induction.MinimalBlockKernelModuleConcreteRawTStableData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} {O : MinimalBlockKernelModuleConcreteRawModuleObjectsData K F} {S : MinimalBlockKernelModuleConcreteRawSubquotientObjectsData O} (A : MinimalBlockKernelModuleConcreteRawModuleActionData O S) : Prop

Stability of T under the selected action on M.

• T_stable (c : S.C) (m : O.M) : m ∈ S.T → (A.actM c) m ∈ S.T

axiom Q2Presentation.Induction.minimalBlock_kernelModuleConcreteRawFrattiniActionData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (O : MinimalBlockKernelModuleConcreteRawModuleObjectsData K F) (S : MinimalBlockKernelModuleConcreteRawSubquotientObjectsData O) : Nonempty (MinimalBlockKernelModuleConcreteRawFrattiniActionData O S)

Residual: quotient-transported action on R.

axiom Q2Presentation.Induction.minimalBlock_kernelModuleConcreteRawModuleActionData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (O : MinimalBlockKernelModuleConcreteRawModuleObjectsData K F) (S : MinimalBlockKernelModuleConcreteRawSubquotientObjectsData O) : Nonempty (MinimalBlockKernelModuleConcreteRawModuleActionData O S)

Residual: quotient-transported action on M.

axiom Q2Presentation.Induction.minimalBlock_kernelModuleConcreteRawTStableData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} {O : MinimalBlockKernelModuleConcreteRawModuleObjectsData K F} {S : MinimalBlockKernelModuleConcreteRawSubquotientObjectsData O} (A : MinimalBlockKernelModuleConcreteRawModuleActionData O S) : Nonempty (MinimalBlockKernelModuleConcreteRawTStableData A)

Residual: the selected action on M stabilizes T.

def Q2Presentation.Induction.MinimalBlockKernelModuleConcreteRawActionsData.ofSplit {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} {O : MinimalBlockKernelModuleConcreteRawModuleObjectsData K F} {S : MinimalBlockKernelModuleConcreteRawSubquotientObjectsData O} (AR : MinimalBlockKernelModuleConcreteRawFrattiniActionData O S) (AM : MinimalBlockKernelModuleConcreteRawModuleActionData O S) (TS : MinimalBlockKernelModuleConcreteRawTStableData AM) : MinimalBlockKernelModuleConcreteRawActionsData (MinimalBlockKernelModuleConcreteRawObjectsData.ofModuleSubquotient O S)

Assemble the current raw-action packet from the split R action, M action, and T-stability packets.

Equations

• Q2Presentation.Induction.MinimalBlockKernelModuleConcreteRawActionsData.ofSplit AR AM TS = { actR := AR.actR, actM := AM.actM, T_stable := ⋯ }

Concrete bridge and head packets

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

Residual: the concrete same-tower quotient bridge for K/Phi(K) ~= M.

structure Q2Presentation.Induction.MinimalBlockKernelModuleConcreteHeadNonzeroData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : MinimalBlockKernelModuleConcreteRawData K F) : Prop

Witness-form nontriviality of the head quotient.

• exists_nonzero_head : ∃ (x : D.M ⧸ D.T), x ≠ 0

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

Residual: the selected head quotient has a nonzero coset.

def Q2Presentation.Induction.MinimalBlockKernelModuleConcreteHeadData.ofHeadNonzero {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} {D : MinimalBlockKernelModuleConcreteRawData K F} (H : MinimalBlockKernelModuleConcreteHeadNonzeroData D) : MinimalBlockKernelModuleConcreteHeadData D

Convert a nonzero head coset into the current nontrivial-head packet.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.minimalBlock_kernelModuleConcreteHeadData_from_frattiniConcreteProofs {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (D : MinimalBlockKernelModuleConcreteRawData K F) : Nonempty (MinimalBlockKernelModuleConcreteHeadData D)

The concrete head packet from the direct nonzero-coset witness.

Replacements for the route8 raw quotient packet

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

Replacement for minimalBlock_kernelRawQuotientTowerData, split into raw R,M, raw T,C, quotient-transported actions, same-tower bridge, and head nonzero packets.

Route-level assembly through the concrete replacements

theorem Q2Presentation.Induction.minimalBlock_kernelModuleActualProofs_from_frattiniConcreteProofs {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleActualProofs chief)

Assemble the actual kernel/module packet through the concrete replacements for the three route8 residuals.

theorem Q2Presentation.Induction.minimalBlock_lowerGroupModuleData_from_kernelFrattiniConcreteProofs {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockLowerGroupModuleData chief)

Lower group/module data through the concrete P3 replacement route.

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

Group-tower data through the concrete P3 replacement route.