Finer concrete kernel/module closers for Section 7

This sidecar is route-neutral and does not edit the routed proof files. It targets the five concrete Section 7 kernel/module packets currently exposed by MinimalBlockKernelModuleConcreteProofs:

• minimalBlock_kernelModuleConcreteLeastData;
• minimalBlock_kernelModuleConcreteFrattiniData;
• minimalBlock_kernelModuleConcreteRawData;
• minimalBlock_kernelModuleConcreteBridgeData;
• minimalBlock_kernelModuleConcreteHeadData.

The manuscript tower is kept fixed: choose the least normal K <= P with K S = P, set R = Phi(K), M = K/R, T = (K cap S)/R, and C = Y/K. Where the current Lean API has no literal subgroup quotient construction, this file splits the packet into smaller same-tower obligations rather than replacing it by an unrelated abstract module packet.

Least K from the underlying finite-group choice packet

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

The concrete least-K packet is exactly the underlying least-over-chief finite-group choice packet. This removes the concrete residual name without changing the selected manuscript object.

Frattini-collapse split for the literal Phi(K)

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

Normality in Y of the literal Frattini subgroup Phi(K).

• frattini_normal : (Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub)).Normal

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

Nontriviality of the literal Frattini layer.

• frattini_card_gt_one : 1 < Nat.card ↥(Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub))

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

Centrality of Phi(K) in K, the first conclusion of the Frattini-centralizer collapse.

• frattini_central_in_K (r : p.fst.Y) : r ∈ Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub) → ∀ k ∈ K.Ksub, r * k = k * r

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

The fourth-power vanishing conclusion K^4 = 1.

• K_fourth_eq_one (k : p.fst.Y) : k ∈ K.Ksub → k ^ 4 = 1

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

The elementary-abelian exponent-two conclusion on Phi(K).

• frattini_square_eq_one (r : p.fst.Y) : r ∈ Subgroup.map K.Ksub.subtype (frattini ↥K.Ksub) → r ^ 2 = 1

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

Residual: normality of the literal Frattini subgroup.

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

Residual: nontriviality of the literal Frattini subgroup.

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

Residual: centrality of the literal Frattini subgroup in K.

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

Residual: fourth-power vanishing on K.

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

Residual: exponent-two on the Frattini layer.

def Q2Presentation.Induction.MinimalBlockKernelModuleConcreteFrattiniData.ofSplit {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} (N : MinimalBlockKernelModuleConcreteFrattiniNormalData K) (C : MinimalBlockKernelModuleConcreteFrattiniNontrivialData K) (Z : MinimalBlockKernelModuleConcreteFrattiniCentralData K) (P4 : MinimalBlockKernelModuleConcreteFourthPowerData K) (E : MinimalBlockKernelModuleConcreteFrattiniExponentData K) : MinimalBlockKernelModuleConcreteFrattiniData K

Assemble the current Frattini packet from five smaller manuscript conclusions for the same literal Phi(K).

Equations

• ⋯ = ⋯

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

The current concrete Frattini packet follows from the split Frattini-collapse conclusions.

Raw R, M, T, C objects split from induced actions

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

The raw finite objects from the fixed subgroup tower: R, M = K/R, T = (K cap S)/R, and C = Y/K.

• 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
• T : Submodule (ZMod 2) self.M
• C : Type
• grpC : Group self.C
• finC : Finite self.C

structure Q2Presentation.Induction.MinimalBlockKernelModuleConcreteRawActionsData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (O : MinimalBlockKernelModuleConcreteRawObjectsData K F) : Type

The induced C-actions on R and M, with stability of T, for the same raw object packet.

• actR : O.C →* O.R ≃ₗ[ZMod 2] O.R
• actM : O.C →* O.M ≃ₗ[ZMod 2] O.M
• T_stable (c : O.C) (m : O.M) : m ∈ O.T → (self.actM c) m ∈ O.T

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

Residual: raw finite objects from the fixed K, Phi(K) tower.

axiom Q2Presentation.Induction.minimalBlock_kernelModuleConcreteRawActionsData {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (O : MinimalBlockKernelModuleConcreteRawObjectsData K F) : Nonempty (MinimalBlockKernelModuleConcreteRawActionsData O)

Residual: induced actions for the fixed raw object packet.

def Q2Presentation.Induction.MinimalBlockKernelModuleConcreteRawData.ofObjectsActions {p : FramedPair} {chief : NonScalarChiefFactor p} {K : MinimalBlockKernelLeastOverChiefData chief} {F : MinimalBlockKernelModuleConcreteFrattiniData K} (O : MinimalBlockKernelModuleConcreteRawObjectsData K F) (A : MinimalBlockKernelModuleConcreteRawActionsData O) : MinimalBlockKernelModuleConcreteRawData K F

Assemble the current raw packet from raw objects plus induced actions on the same selected tower.

Equations

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

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

The current concrete raw-data packet follows from raw objects and actions on the same selected tower.

Bridge and head through same-tower lower packets

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

The concrete bridge packet follows from the lower semantic K/R ~= M bridge, instantiated on the same selected K, literal Phi(K), and raw module objects.

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

The concrete head packet follows from the existing nontrivial-head packet on the raw tower assembled from the same concrete raw data.

Aggregate route through the finer concrete closers

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

Assemble the current aggregate actual kernel/module packet while avoiding the five concrete residual names.

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

Lower group/module data through the finer concrete closers in this sidecar.

Same-tower provenance and final group-tower route

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

Concrete provenance through the coherent kernel/Frattini tower sidecar. Its axiom closure avoids the route2 ten-pack of independent kernel, Frattini, raw object/action, bridge, and head residual names.

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

Concrete-final provenance pieces through the finer kernel/module split plus the existing quotient-head and lower-character refinements.

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

Route-ready provenance-semantic replacement through the finer kernel/module concrete split.

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

Route-ready group tower through the finer kernel/module concrete split.

This is the drop-in replacement theorem to use in a future route edit if the final closure should remove the original five concrete packet names.