Determinant-side Section 7 minimal-block closers

This sidecar refines the first determinant-pushout residual in the final Section 7 route without touching the existing minimal-block sidecars.

The current final route already uses MinimalBlockGroupTowerData for the subgroup tower provenance. The remaining determinant family starts from minimalBlock_preheadCentralPushoutSelfDualityData, which only records the self-duality map phi. The manuscript's central pushout, however, carries a square map and a polar map:

• q_lambda(m) = lambda(mtilde^2);
• b_lambda(m,m') is the commutator pairing;
• the self-duality phi_lambda identifies these with the diagonal and symmetrized polar pairing.

The packet below records that square/polar interface and then projects it to the older phi-only packet. Routing the capstone through minimalBlock_of_nonScalar_proven_determinant_refined therefore replaces the old minimalBlock_preheadCentralPushoutSelfDualityData axiom in the final closure by the more concrete minimalBlock_preheadCentralPushoutSquarePolarData packet.

Central pushout square/polar provenance

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

The concrete square/polar data of the scalar central pushouts on the pre-head minimal-block tower.

Manuscript anchor: Section 7, prop:simpleheaddet, where each nonzero invariant lambda : R^vee forms K_lambda = K / ker lambda, with square map q_lambda and polar form b_lambda. The fields square_diagonal and polar_symm record that the self-duality family phi_lambda : M -> M^vee is the source of those maps.

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

  The self-duality family induced by the scalar central pushouts.

• square : Module.Dual (ZMod 2) D.R → Quadratic.QuadF2 D.M

  The square map of each scalar central pushout, as a quadratic form on M.

• square_diagonal (lam : Module.Dual (ZMod 2) D.R) (m : D.M) : (self.square lam).form m = ((self.phi lam) m) m

  The square map is the diagonal of the self-duality pairing.

• polar_symm (lam : Module.Dual (ZMod 2) D.R) (m m' : D.M) : ((self.square lam).polar m) m' = ((self.phi lam) m) m' + ((self.phi lam) m') m

  The polar map is the symmetrized self-duality pairing.

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

Residual Section 7 axiom: concrete square/polar scalar-pushout data.

This replaces the weaker minimalBlock_preheadCentralPushoutSelfDualityData residual in the refined route below.

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

Forget the concrete square/polar maps and retain the older self-duality packet.

Equations

• Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSelfDualityData.ofSquarePolar S = { phi := S.phi }

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

Reassemble the old central-pushout self-duality packet from the concrete square/polar central-pushout data.

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

Build the bare extraspecial family through the concrete square/polar packet, avoiding the old minimalBlock_preheadCentralPushoutSelfDualityData axiom.

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

Reassemble the equivariant determinant family from square/polar pushout data and the existing naturality packet.

Final minimal-block route through the determinant refinement

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

Section 7 reassembly from a realized group tower and square/polar central pushout data.

Compared with minimalBlock_of_nonScalar_proven_groupTower_refined, this route keeps the group-tower provenance packet and the same diagonal/polar/radical packets, but replaces the old central-pushout self-duality residual by minimalBlock_preheadCentralPushoutSquarePolarData.

Acceptance checks