Concrete kernel/module closers for the Section 7 subgroup tower

This sidecar is intentionally route-neutral. It replaces the five current concrete kernel/module residual names by one same-tower provenance packet.

The packet is closer to the manuscript construction than the five independent residual calls: it carries one realized subgroup tower R = Phi(K) <= K <= L_Y, the Frattini-collapse facts from lem:collapse, the raw objects R, M = K/R, T, C, the induced actions, the literal K/R ~= M bridge, and the nonzero simple head.

One same-tower provenance packet

structure Q2Presentation.Induction.MinimalBlockKernelModuleConcreteProvenanceData {p : FramedPair} (chief : NonScalarChiefFactor p) : Type 1

Concrete provenance for the Section 7 minimal-block kernel/module tower.

This is the manuscript data behind the current five concrete residuals, bundled so downstream routes cannot mix a least K, a Frattini layer, raw module data, a quotient bridge, and a head proof coming from different towers.

• Ksub : Subgroup p.fst.Y

  The least normal subgroup K <= P with K S = P.

• Ksub_normal : self.Ksub.Normal
• Ksub_le_upper : self.Ksub ≤ chief.upper
• Ksub_le_LY : self.Ksub ≤ p.fst.LY
• KS_eq_upper : self.Ksub ⊔ chief.lower = chief.upper
• minimal_K (K' : Subgroup p.fst.Y) : K'.Normal → K' ≤ chief.upper → K' ⊔ chief.lower = chief.upper → self.Ksub ≤ K'
• Rsub : Subgroup p.fst.Y

  The realized Frattini subgroup R = Phi(K) inside Y.

• Rsub_normal : self.Rsub.Normal
• Rsub_le_Ksub : self.Rsub ≤ self.Ksub
• Rsub_card_gt_one : 1 < Nat.card ↥self.Rsub
• Rsub_eq_frattini : self.Rsub = Subgroup.map self.Ksub.subtype (frattini ↥self.Ksub)
• Rsub_central_in_K (r : p.fst.Y) : r ∈ self.Rsub → ∀ k ∈ self.Ksub, r * k = k * r

  lem:collapse: R centralizes K.

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

  lem:collapse: K^4 = 1.

• Rsub_square_eq_one (r : p.fst.Y) : r ∈ self.Rsub → r ^ 2 = 1

  lem:collapse: the Frattini layer is elementary abelian.

• rawModuleData : MinimalBlockRawModuleData p chief

  The raw finite objects R, M, T, and C.

• rawActionData : MinimalBlockRawActionData self.rawModuleData

  The induced C-actions on R and M, with T stable.

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

  The literal quotient K/R realizes the abstract raw module M.

• headNontrivialData : MinimalBlockHeadNontrivialData (MinimalBlockRawTowerData.ofModuleAction self.rawModuleData self.rawActionData)

  The simple head M/T is nonzero.

def Q2Presentation.Induction.MinimalBlockKernelModuleConcreteProvenanceData.leastData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelModuleConcreteProvenanceData chief) : MinimalBlockKernelLeastOverChiefData chief

Forget provenance to the least-kernel concrete packet.

Equations

• P.leastData = { Ksub := P.Ksub, Ksub_normal := ⋯, Ksub_le_upper := ⋯, KS_eq_upper := ⋯, minimal_K := ⋯ }

def Q2Presentation.Induction.MinimalBlockKernelModuleConcreteProvenanceData.frattiniData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelModuleConcreteProvenanceData chief) : MinimalBlockKernelModuleConcreteFrattiniData P.leastData

Forget provenance to the concrete Frattini-collapse packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockKernelModuleConcreteProvenanceData.rawData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelModuleConcreteProvenanceData chief) : MinimalBlockKernelModuleConcreteRawData P.leastData ⋯

Forget provenance to the concrete raw tower packet.

Equations

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

def Q2Presentation.Induction.MinimalBlockKernelModuleConcreteProvenanceData.bridgeData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelModuleConcreteProvenanceData chief) : MinimalBlockKernelModuleConcreteBridgeData P.rawData

Forget provenance to the concrete K/Phi(K) ~= M bridge packet.

Equations

• P.bridgeData = { KmodR_equiv_rawM := id P.KmodR_equiv_rawM }

def Q2Presentation.Induction.MinimalBlockKernelModuleConcreteProvenanceData.headData {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelModuleConcreteProvenanceData chief) : MinimalBlockKernelModuleConcreteHeadData P.rawData

Forget provenance to the concrete nontrivial-head packet.

Equations

• ⋯ = ⋯

Coherent replacement for the five residual calls

structure Q2Presentation.Induction.MinimalBlockKernelModuleConcreteBundle {p : FramedPair} (chief : NonScalarChiefFactor p) : Type 1

The five concrete packets, tied to one selected subgroup tower.

• K : MinimalBlockKernelLeastOverChiefData chief
• F : MinimalBlockKernelModuleConcreteFrattiniData self.K
• D : MinimalBlockKernelModuleConcreteRawData self.K ⋯
• B : MinimalBlockKernelModuleConcreteBridgeData self.D
• H : MinimalBlockKernelModuleConcreteHeadData self.D

def Q2Presentation.Induction.MinimalBlockKernelModuleConcreteBundle.actualProofs {p : FramedPair} {chief : NonScalarChiefFactor p} (X : MinimalBlockKernelModuleConcreteBundle chief) : MinimalBlockKernelModuleActualProofs chief

Assemble the current actual packet from a coherent concrete bundle.

Equations

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

def Q2Presentation.Induction.MinimalBlockKernelModuleConcreteBundle.ofProvenance {p : FramedPair} {chief : NonScalarChiefFactor p} (P : MinimalBlockKernelModuleConcreteProvenanceData chief) : MinimalBlockKernelModuleConcreteBundle chief

Turn one provenance packet into the coherent five-packet bundle.

Equations

• Q2Presentation.Induction.MinimalBlockKernelModuleConcreteBundle.ofProvenance P = { K := P.leastData, F := ⋯, D := P.rawData, B := P.bridgeData, H := ⋯ }

New residual and route-ready closers

axiom Q2Presentation.Induction.minimalBlock_kernelModuleConcreteProvenanceData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteProvenanceData chief)

Single residual replacing the five concrete kernel/module residual calls.

It is one same-tower subgroup/module construction, not five independently queried packets.

theorem Q2Presentation.Induction.minimalBlock_kernelModuleConcreteBundle_from_concreteClosers {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockKernelModuleConcreteBundle chief)

Coherent closure of the five concrete packets from the new provenance packet.

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

Route-ready replacement for minimalBlock_kernelModuleActualProofs_from_concreteProofs.

The axiom closure contains the one provenance packet above, not the five concrete residual names from MinimalBlockKernelModuleConcreteProofs.

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

Drop-in lower group/module projection through the one-packet concrete closer.

Auditable projections of the coherent closure

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

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

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

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

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

Acceptance checks