Group-tower determinant closers for Section 7

This sidecar keeps the final target-quotient route but refines the determinant packet used at the Section 7 minimal block. The existing final route already uses minimalBlock_groupTowerData for the subgroup tower R = Phi(K) <= K <= L_Y. The remaining combined central-pushout packet minimalBlock_preheadCentralPushoutSquarePolarData is split here into:

• a shared central-pushout quadratic family (phi_lambda, q_lambda);
• the statement that q_lambda is the diagonal of phi_lambda;
• the statement that the polar form of q_lambda is the symmetrized phi_lambda pairing.

The split is tied to the same family, so the square and polar witnesses cannot silently come from unrelated pushouts.

A finer central-pushout square/polar split

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

Shared central-pushout determinant family over a pre-head Section 7 tower.

Manuscript anchor: Section 7, prop:simpleheaddet, where a nonzero invariant lambda : R^vee gives the scalar central pushout K_lambda, its square map q_lambda, and the self-duality pairing phi_lambda.

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

  The self-duality pairing induced by the scalar central pushout.

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

  The square map of the same scalar central pushout.

structure Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSquareDiagonalData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Q : MinimalBlockPreheadCentralPushoutQuadraticFamilyData D) : Prop

The central-pushout square map is the diagonal of the shared pairing.

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

structure Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutPolarSymmData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Q : MinimalBlockPreheadCentralPushoutQuadraticFamilyData D) : Prop

The polar map of the square form is the symmetrized shared pairing.

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

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

Residual Section 7 axiom: the shared scalar-pushout determinant family.

This is the common provenance for the diagonal and polar statements below.

axiom Q2Presentation.Induction.minimalBlock_preheadCentralPushoutSquareDiagonalData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Q : MinimalBlockPreheadCentralPushoutQuadraticFamilyData D) : Nonempty (MinimalBlockPreheadCentralPushoutSquareDiagonalData Q)

Residual Section 7 axiom: q_lambda(m) is the diagonal of phi_lambda.

axiom Q2Presentation.Induction.minimalBlock_preheadCentralPushoutPolarSymmData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Q : MinimalBlockPreheadCentralPushoutQuadraticFamilyData D) : Nonempty (MinimalBlockPreheadCentralPushoutPolarSymmData Q)

Residual Section 7 axiom: the polar form is the symmetrized phi_lambda pairing.

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSquarePolarData.ofQuadraticFamily {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Q : MinimalBlockPreheadCentralPushoutQuadraticFamilyData D) (S : MinimalBlockPreheadCentralPushoutSquareDiagonalData Q) (P : MinimalBlockPreheadCentralPushoutPolarSymmData Q) : MinimalBlockPreheadCentralPushoutSquarePolarData D

Reassemble the previous square/polar packet from the shared determinant family and its two concrete identities.

Equations

• Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSquarePolarData.ofQuadraticFamily Q S P = { phi := Q.phi, square := Q.square, square_diagonal := ⋯, polar_symm := ⋯ }

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

Compatibility theorem replacing the old combined square/polar residual by the finer shared-family, square-diagonal, and polar-symmetry residuals.

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

Forget the finer square/polar split to the self-duality packet consumed by the existing extraspecial-family API.

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

Build the bare extraspecial family through the finer determinant packets.

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

Reassemble the equivariant determinant family from the finer determinant packets plus the existing naturality residual.

Final route using the finer Section 7 determinant packet

theorem Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch_groupTowerDeterminantPackets (p : FramedPair) : ¬ScalarTerminal p → Nonempty (FourierBranchData p)

Nonterminal branch routed through the Section 7 group tower and the finer central-pushout determinant packets.

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_groupTowerDeterminantPackets (p : FramedPair) (h : ¬ScalarTerminal p) : ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

Recursive branch using the finer Section 7 determinant packet.

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_groupTowerDeterminantPackets (p : FramedPair) : framedCountA p = framedCountQ p ∨ ∃ (children : List FramedPair) (combine : List Cardinal.{0} → Cardinal.{0}), (∀ c ∈ children, framedMeasure c < framedMeasure p) ∧ framedCountA p = combine (List.map framedCountA children) ∧ framedCountQ p = combine (List.map framedCountQ children)

Recursion step using the finer Section 7 determinant packet.

theorem Q2Presentation.Induction.boundaryFramed_counts_equal_groupTowerDeterminantPackets (p : FramedPair) : framedCountA p = framedCountQ p

Boundary-framed counts equal through the finer Section 7 determinant route.

theorem Q2Presentation.Induction.finite_surjection_counts_equal_groupTowerDeterminantPackets (G : Type) [Group G] [Finite G] [Nonempty G] : Cardinal.mk (Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))) = Cardinal.mk (Profinite.SurjContHom GQ2Profinite (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G)))

Equal finite surjection counts through the group-tower determinant route.