Realization-side Section 7 minimal-block closers

This sidecar leaves the routed files and the root import untouched. It records a group-tower provenance interface, plus two alternative Section 7 reassembly routes over the existing APIs:

• MinimalBlockGroupTowerData is the manuscript-facing provenance packet for the subgroup tower R = Phi(K) <= K <= L_Y, the elementary layer M = K/R, the submodule T, the lower quotient C, and the induced actions. It feeds the raw module/action/head/dual-invariant/raw-character packets and also supplies the K/R ~= M bridge needed by CentralCoverTargetSubgroupConcreteData.

• minimalBlock_of_nonScalar_proven_concrete_noHeadResidual keeps the concrete residual split of MinimalBlockConcreteClosers, but derives the head nontriviality field from determinant nonzeroness. Its closure drops the current minimalBlock_headNontrivialData residual and replaces it by the manuscript-facing determinant nonzero packet.

• minimalBlock_of_nonScalar_proven_realization_refined also uses the existing pre-head invariant-character packet from MinimalBlockPacketClosers2, so its closure drops both minimalBlock_headNontrivialData and the raw-character residual from the concrete route.

The point is not to reroute the main proof here. It is to give follow-up workers strictly smaller closure targets that can be compared by #print axioms.

Group-tower provenance for Section 7

structure Q2Presentation.Induction.MinimalBlockGroupTowerData (p : FramedPair) (chief : NonScalarChiefFactor p) : Type 1

Manuscript-facing provenance for the minimal-block subgroup tower.

The current downstream interfaces are intentionally module-level. This structure keeps the missing finite-group provenance in one place: a minimal normal subgroup K, its Frattini subgroup R = Phi(K), the raw module/action data extracted from R, M = K/R, T, and C, the simple-head conclusions of lem:simplehead, and the K/R ~= M bridge consumed by the target-tower concrete packet.

• Ksub : Subgroup p.fst.Y

  The realized minimal normal subgroup K <= P.

• Ksub_normal : self.Ksub.Normal

  K is normal in Y.

• Ksub_le_upper : self.Ksub ≤ chief.upper

  K lies in the selected chief-factor upper group.

• Ksub_le_LY : self.Ksub ≤ p.fst.LY

  K lies in the marked wild kernel.

• KS_eq_upper : self.Ksub ⊔ chief.lower = chief.upper

  The minimality condition is imposed among Y-normal subgroups with K S = P.

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

  Minimality of K subject to K S = P.

• Rsub : Subgroup p.fst.Y

  The realized Frattini subgroup R = Phi(K).

• Rsub_normal : self.Rsub.Normal

  R is normal in Y.

• Rsub_le_Ksub : self.Rsub ≤ self.Ksub

  Manuscript tower condition R <= K.

• Rsub_card_gt_one : 1 < Nat.card ↥self.Rsub

  R is nontrivial, so the middle quotient is a genuine strict step.

• Rsub_eq_frattini : self.Rsub = Subgroup.map self.Ksub.subtype (frattini ↥self.Ksub)

  Manuscript R = Phi(K), realized inside Y.

• rawModuleData : MinimalBlockRawModuleData p chief

  The additive F_2 raw module objects R, M, T, and C.

• rawActionData : MinimalBlockRawActionData self.rawModuleData

  The conjugation actions of C on R and M, with T stable.

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

  Nontriviality of the simple head M/T.

• dualInvariantData : MinimalBlockDualInvariantVanishesData (MinimalBlockRawTowerData.ofModuleAction self.rawModuleData self.rawActionData)

  The dual-invariant vanishing (M^vee)^C = 0.

• rawInvariantCharacterData : MinimalBlockRawInvariantCharacterData (MinimalBlockRawTowerData.ofModuleAction self.rawModuleData self.rawActionData)

  A raw invariant determinant character on R.

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

  The quotient K/R realizes the abstract elementary module M.

def Q2Presentation.Induction.MinimalBlockGroupTowerData.rawTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (G : MinimalBlockGroupTowerData p chief) : MinimalBlockRawTowerData p chief

The raw tower assembled from the group-tower module and action packets.

Equations

• G.rawTowerData = Q2Presentation.Induction.MinimalBlockRawTowerData.ofModuleAction G.rawModuleData G.rawActionData

def Q2Presentation.Induction.MinimalBlockGroupTowerData.preheadTowerData {p : FramedPair} {chief : NonScalarChiefFactor p} (G : MinimalBlockGroupTowerData p chief) : MinimalBlockPreheadTowerData p chief

The pre-head tower assembled from the group-tower raw tower and dual-invariant vanishing.

Equations

• G.preheadTowerData = Q2Presentation.Induction.MinimalBlockPreheadTowerData.ofRaw G.rawTowerData ⋯

def Q2Presentation.Induction.MinimalBlockGroupTowerData.preheadInvariantCharacterData {p : FramedPair} {chief : NonScalarChiefFactor p} (G : MinimalBlockGroupTowerData p chief) : MinimalBlockPreheadInvariantCharacterData G.preheadTowerData

The pre-head invariant character induced by the raw determinant character.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockGroupTowerData.toMinimalBlock {p : FramedPair} {chief : NonScalarChiefFactor p} (G : MinimalBlockGroupTowerData p chief) (h : ¬ScalarTerminal p) (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData G.preheadTowerData) (A : MinimalBlockPreheadExtraspecialAnnihilationData F) (R : MinimalBlockPreheadExtraspecialRadicalData F) : MinimalBlock p

Build the module-level MinimalBlock from group-tower provenance and the remaining determinant-pushout packets.

Equations

• G.toMinimalBlock h F A R = Q2Presentation.Induction.minimalBlock_of_preheadRefinedData h chief G.preheadTowerData ⋯ F A R ⋯

Group-tower packet projections

axiom Q2Presentation.Induction.minimalBlock_groupTowerData {p : FramedPair} (chief : NonScalarChiefFactor p) : Nonempty (MinimalBlockGroupTowerData p chief)

Residual Section 7 axiom: realized group tower behind the raw packets.

This is intentionally stronger than the separate raw module/action/head/dual and raw-character residuals: it keeps the subgroup provenance required later by the target-tower construction instead of losing it at the module boundary.

theorem Q2Presentation.Induction.minimalBlock_rawModuleData_from_groupTower {p : FramedPair} (chief : NonScalarChiefFactor p) (G : MinimalBlockGroupTowerData p chief) : Nonempty (MinimalBlockRawModuleData p chief)

A realized group tower supplies the raw finite module objects.

theorem Q2Presentation.Induction.minimalBlock_rawActionData_from_groupTower {p : FramedPair} {chief : NonScalarChiefFactor p} (G : MinimalBlockGroupTowerData p chief) : Nonempty (MinimalBlockRawActionData G.rawModuleData)

A realized group tower supplies the raw quotient actions.

theorem Q2Presentation.Induction.minimalBlock_headNontrivialData_from_groupTower {p : FramedPair} {chief : NonScalarChiefFactor p} (G : MinimalBlockGroupTowerData p chief) : Nonempty (MinimalBlockHeadNontrivialData G.rawTowerData)

A realized group tower supplies the nontrivial simple-head packet.

theorem Q2Presentation.Induction.minimalBlock_dualInvariantVanishesData_from_groupTower {p : FramedPair} {chief : NonScalarChiefFactor p} (G : MinimalBlockGroupTowerData p chief) : Nonempty (MinimalBlockDualInvariantVanishesData G.rawTowerData)

A realized group tower supplies the dual-invariant vanishing packet.

theorem Q2Presentation.Induction.minimalBlock_rawInvariantCharacterData_from_groupTower {p : FramedPair} {chief : NonScalarChiefFactor p} (G : MinimalBlockGroupTowerData p chief) : Nonempty (MinimalBlockRawInvariantCharacterData G.rawTowerData)

A realized group tower supplies the raw determinant-character packet.

theorem Q2Presentation.Induction.centralCover_targetSubgroupConcreteData_from_groupTower {p : FramedPair} {chief : NonScalarChiefFactor p} (G : MinimalBlockGroupTowerData p chief) (B : MinimalBlock p) (hM : ↥(Subgroup.map (QuotientGroup.mk' G.Rsub) G.Ksub) ≃* Multiplicative B.M) : Nonempty (CentralCoverTargetSubgroupConcreteData B)

A realized group tower plus a K/R ~= B.M bridge supplies the target subgroup concrete packet for any already-selected block B.

The extra bridge is the explicit provenance tying the abstract MinimalBlock.M to the quotient module extracted from the subgroup tower.

Group-tower reassembly

theorem Q2Presentation.Induction.minimalBlock_of_nonScalar_proven_groupTower_refined (p : FramedPair) : ¬ScalarTerminal p → Nonempty (MinimalBlock p)

Section 7 reassembly from a realized group tower, leaving only the determinant pushout packets as separate residuals.

This theorem is the Pro-recommended direction: the single group-tower provenance packet replaces the raw module, action, simple-head, dual-invariant, and raw determinant-character packets in the closure. The determinant pushout packets remain split as central-pushout self-duality/naturality, diagonal/polar vanishing, and radical containment.

Concrete split with determinant nonzero supplying the head

theorem Q2Presentation.Induction.minimalBlock_of_nonScalar_proven_concrete_noHeadResidual (p : FramedPair) : ¬ScalarTerminal p → Nonempty (MinimalBlock p)

Concrete Section 7 reassembly without the separate head-nontrivial residual.

Compared with minimalBlock_of_nonScalar_proven_concrete_refined, this uses minimalBlock_headNontrivial_from_determinant through minimalBlock_of_preheadRefinedData, rather than supplying MinimalBlockPreheadExtraspecialNonzeroData from minimalBlock_headNontrivialData. The resulting axiom closure drops minimalBlock_headNontrivialData and adds the determinant-nonzero packet minimalBlock_preheadExtraspecialNonzeroData.

Pre-head character plus determinant nonzero realization route

theorem Q2Presentation.Induction.minimalBlock_of_nonScalar_proven_realization_refined (p : FramedPair) : ¬ScalarTerminal p → Nonempty (MinimalBlock p)

Section 7 reassembly using the pre-head invariant-character packet and the determinant-nonzero packet.

This theorem keeps the concrete central-pushout/naturality, diagonal/polar, and radical-containment splits, but avoids two residuals from minimalBlock_of_nonScalar_proven_concrete_refined:

• minimalBlock_headNontrivialData;
• minimalBlock_rawInvariantCharacterData.

Acceptance checks