Section 7 extraspecial determinant packet refinement

This sidecar refines the four independent extraspecial determinant residuals in the final Section 7 route:

• minimalBlock_preheadExtraspecialNaturalityData;
• minimalBlock_preheadExtraspecialDiagonalZeroData;
• minimalBlock_preheadExtraspecialPolarZeroData;
• minimalBlock_preheadExtraspecialRadicalContainmentData.

The replacement residual is one same-family prop:simpleheaddet packet on the actual extraspecial family induced by a central-pushout self-duality family. It states the manuscript conclusions directly on Quadratic.Extraspecial.extraspecialForm: naturality, annihilation of T, and polar-radical containment. The four old packets are then projections from that single object, so the routed closure no longer needs them as independent inputs.

One coherent extraspecial determinant residual

axiom Q2Presentation.Induction.minimalBlock_preheadExtraspecialSimpleHeadDeterminantData_residual {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSelfDualityData D) : Nonempty (MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData (MinimalBlockPreheadExtraspecialFamilyData.ofCentralPushoutSelfDuality S))

The refined Section 7 extraspecial determinant residual.

Manuscript anchor: prop:simpleheaddet, applied to the scalar central pushouts K_lambda = K / ker lambda for the central-pushout family S.phi.

Projections to the four previous packet boundaries

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialNaturalityData_from_determinantResidual {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSelfDualityData D) : Nonempty (MinimalBlockPreheadExtraspecialNaturalityData (MinimalBlockPreheadExtraspecialFamilyData.ofCentralPushoutSelfDuality S))

Naturality of the actual central-pushout extraspecial family, projected from the refined simple-head determinant packet.

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialDiagonalZeroData_from_determinantResidual {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSelfDualityData D) : ∃ (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D), Nonempty (MinimalBlockPreheadExtraspecialDiagonalZeroData F)

Diagonal vanishing on T, projected from the refined simple-head determinant packet for the same extraspecial family.

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialPolarZeroData_from_determinantResidual {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSelfDualityData D) : ∃ (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D), Nonempty (MinimalBlockPreheadExtraspecialPolarZeroData F)

Polar vanishing on T x M, projected from the refined simple-head determinant packet for the same extraspecial family.

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialRadicalContainmentData_from_determinantResidual {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSelfDualityData D) : ∃ (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D), Nonempty (MinimalBlockPreheadExtraspecialRadicalContainmentData F)

Polar-radical containment, projected from the refined simple-head determinant packet for the same extraspecial family.

theorem Q2Presentation.Induction.minimalBlock_preheadExtraspecialPackets_from_determinantResidual {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSelfDualityData D) : ∃ (F : MinimalBlockPreheadExtraspecialEquivariantFamilyData D), Nonempty (MinimalBlockPreheadExtraspecialAnnihilationData F) ∧ Nonempty (MinimalBlockPreheadExtraspecialRadicalData F)

The determinant half needed by the final Section 7 route, now closed from one coherent extraspecial prop:simpleheaddet residual instead of four independent extraspecial packet residuals.

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

Route-packet replacement using the refined extraspecial determinant residual.

The resulting closure keeps the central-pushout self-duality residual and replaces the four extraspecial determinant residuals by minimalBlock_preheadExtraspecialSimpleHeadDeterminantData_residual.

Final route using the refined determinant residual

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

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_targetFramedMarkedQuotientExtraspecialDeterminantProofs (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)

theorem Q2Presentation.Induction.boundaryFramed_recursion_step_targetFramedMarkedQuotientExtraspecialDeterminantProofs (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)

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

theorem Q2Presentation.Induction.finite_surjection_counts_equal_targetFramedMarkedQuotientExtraspecialDeterminantProofs (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)))