Concrete Section 7 minimal-block closers

This sidecar keeps the routed capstone files untouched and adds a more concrete Section 7 reassembly route, following the manuscript's tower Y -> B -> C -> H and determinant pushout (eq:targettower, lem:simplehead, lem:collapse, prop:simpleheaddet).

The main theorem below avoids the current pre-head invariant-character and pre-head determinant-nonzero residuals. It also splits the extraspecial pushout packets into central-pushout self-duality, naturality, diagonal/polar vanishing, and radical-containment witnesses.

Raw Frattini character data

structure Q2Presentation.Induction.MinimalBlockRawInvariantCharacterData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Prop

Nonzero invariant determinant characters at the raw tower level.

This is the manuscript's X_R = (R^vee)^B = (R^vee)^C, stated before the pre-head tower is assembled from lem:simplehead's dual-invariant vanishing.

• exists_nonzero_invariant : ∃ (lam : Module.Dual (ZMod 2) D.R), lam ≠ 0 ∧ ∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam

axiom Q2Presentation.Induction.minimalBlock_rawInvariantCharacterData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) : Nonempty (MinimalBlockRawInvariantCharacterData D)

Residual Section 7 axiom: raw nonzero invariant determinant character.

Manuscript anchor: the determinant character space X_R = (R^vee)^B = (R^vee)^C used in prop:simpleheaddet. This is deliberately attached to the raw Frattini quotient tower rather than to a later pre-head package.

def Q2Presentation.Induction.MinimalBlockRawInvariantCharacterData.toPrehead {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockRawTowerData p chief} {V : MinimalBlockDualInvariantVanishesData D} (X : MinimalBlockRawInvariantCharacterData D) : MinimalBlockPreheadInvariantCharacterData (MinimalBlockPreheadTowerData.ofRaw D V)

Transport a raw invariant character through the pre-head tower assembled from the same raw tower and dual-invariant-vanishing data.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.minimalBlock_preheadInvariantCharacterData_from_rawCharacter {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) (V : MinimalBlockDualInvariantVanishesData D) (hX : Nonempty (MinimalBlockRawInvariantCharacterData D)) : Nonempty (MinimalBlockPreheadInvariantCharacterData (MinimalBlockPreheadTowerData.ofRaw D V))

Reassemble the pre-head invariant-character packet from the raw determinant character residual.

theorem Q2Presentation.Induction.minimalBlock_preheadInvariantCharacterData_from_rawCharacterResidual {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockRawTowerData p chief) (V : MinimalBlockDualInvariantVanishesData D) : Nonempty (MinimalBlockPreheadInvariantCharacterData (MinimalBlockPreheadTowerData.ofRaw D V))

Residual-backed version of minimalBlock_preheadInvariantCharacterData_from_rawCharacter.

Central-pushout self-duality and naturality

structure Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSelfDualityData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Type

The central-pushout self-duality family underlying the extraspecial square maps, before naturality is installed.

Manuscript anchor: the scalar central pushouts K_lambda = K / ker lambda and their square/polar maps in prop:simpleheaddet.

• phi : Module.Dual (ZMod 2) D.R → D.M →ₗ[ZMod 2] Module.Dual (ZMod 2) D.M

axiom Q2Presentation.Induction.minimalBlock_preheadCentralPushoutSelfDualityData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadCentralPushoutSelfDualityData D)

Residual Section 7 axiom: central-pushout self-duality family.

def Q2Presentation.Induction.MinimalBlockPreheadExtraspecialFamilyData.ofCentralPushoutSelfDuality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSelfDualityData D) : MinimalBlockPreheadExtraspecialFamilyData D

View central-pushout self-duality as the existing bare extraspecial family packet.

Equations

• Q2Presentation.Induction.MinimalBlockPreheadExtraspecialFamilyData.ofCentralPushoutSelfDuality S = { phi := S.phi }

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialFamilyData_from_centralPushoutSelfDuality {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) (hS : Nonempty (MinimalBlockPreheadCentralPushoutSelfDualityData D)) : Nonempty (MinimalBlockPreheadExtraspecialFamilyData D)

Reassemble the bare extraspecial-family packet from central-pushout self-duality.

axiom Q2Presentation.Induction.minimalBlock_preheadExtraspecialNaturalityData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockPreheadExtraspecialFamilyData D) : Nonempty (MinimalBlockPreheadExtraspecialNaturalityData F)

Residual Section 7 axiom: naturality of the central-pushout self-duality.

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialInvariantData_from_naturalityResidual {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockPreheadExtraspecialFamilyData D) : Nonempty (MinimalBlockPreheadExtraspecialInvariantData F)

Reassemble the diagonal-invariance packet from the more concrete naturality residual.

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialEquivariantFamilyData_from_centralPushoutNaturality {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadExtraspecialEquivariantFamilyData D)

Reassemble the equivariant family from central-pushout self-duality and naturality, avoiding the old pre-head family and invariance residuals.

Diagonal, polar, and radical-containment splits

axiom Q2Presentation.Induction.minimalBlock_preheadExtraspecialDiagonalZeroData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D) : Nonempty (MinimalBlockPreheadExtraspecialDiagonalZeroData F)

Residual Section 7 axiom: diagonal vanishing of the pushout square map on T.

axiom Q2Presentation.Induction.minimalBlock_preheadExtraspecialPolarZeroData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D) : Nonempty (MinimalBlockPreheadExtraspecialPolarZeroData F)

Residual Section 7 axiom: polar vanishing on T x M.

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialAnnihilationData_from_diagonalPolarResidual {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D) : Nonempty (MinimalBlockPreheadExtraspecialAnnihilationData F)

Reassemble determinant annihilation from diagonal and polar vanishing.

structure Q2Presentation.Induction.MinimalBlockPreheadExtraspecialRadicalContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D) : Prop

The concrete radical-containment witness for the symmetrized pushout polar pairing.

• symm_polar_radical_subset_T (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → (∀ (c : D.C), lam ∘ₗ ↑(D.actR c) = lam) → ∀ (m : D.M), (∀ (m' : D.M), ((F.phi lam) m) m' + ((F.phi lam) m') m = 0) → m ∈ D.T

axiom Q2Presentation.Induction.minimalBlock_preheadExtraspecialRadicalContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D) : Nonempty (MinimalBlockPreheadExtraspecialRadicalContainmentData F)

Residual Section 7 axiom: radical containment for the symmetrized polar form.

def Q2Presentation.Induction.MinimalBlockPreheadExtraspecialRadicalData.ofContainment {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D} (R : MinimalBlockPreheadExtraspecialRadicalContainmentData F) : MinimalBlockPreheadExtraspecialRadicalData F

View the concrete radical-containment witness as the current radical packet.

Equations

• ⋯ = ⋯

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialRadicalData_from_containmentResidual {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D) : Nonempty (MinimalBlockPreheadExtraspecialRadicalData F)

Reassemble the determinant radical packet from radical containment.

Concrete minimal-block reassembly

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

A concrete Section 7 replacement route for minimalBlock_of_nonScalar.

This combines the raw invariant-character route with the simple-head/radical route: the old pre-head invariant-character residual is replaced by a raw Frattini-character witness, and the old pre-head determinant-nonzero residual is proved from lem:simplehead's nontrivial head plus radical containment.

Acceptance checks