Actual Section 7 central-pushout/determinant closers, fourth pass

This sidecar leaves the routed capstone files untouched. It replaces the two current final-route extraspecial residuals

• minimalBlock_preheadCentralPushoutSquarePolarData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData;

by one route through the actual scalar central-pushout family and the four same-family prop:simpleheaddet pieces:

• naturality of phi_lambda;
• diagonal vanishing q_lambda|_T = 0;
• polar vanishing b_lambda(T,M) = 0;
• polar-radical containment in T.

The determinant pieces below are indexed by P.actualScalar.toSemanticData, so they cannot drift to a different self-duality family than the square/polar packet.

Same-family actual central-pushout packet

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

Actual central-pushout data plus the same-family simple-head determinant pieces for that actual scalar family.

The field actualScalar is the scalar central-pushout family: it carries phi_lambda, the square map, scalar quotient surjectivity, and the theorem that the square is the extraspecial square of the same phi_lambda. The determinant field is then stated for actualScalar.toSemanticData, so naturality, diagonal/polar vanishing, and radical containment are all tied to the same family.

• actualScalar : MinimalBlockPreheadActualScalarCentralPushoutData D
• determinantPieces : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualSplitData self.actualScalar.toSemanticData

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutActualClosers4Data.toSquarePolar {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutActualClosers4Data D) : MinimalBlockPreheadCentralPushoutSquarePolarData D

The actual scalar family supplies the current square/polar packet by theorem-level projection, without using the old square/polar axiom.

Equations

• P.toSquarePolar = Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSquarePolarData.ofActualScalar P.actualScalar

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutActualClosers4Data.toActualDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutActualClosers4Data D) : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData P.actualScalar.toSemanticData

The same-family determinant pieces supply the current actual determinant packet for the semantic family projected from actualScalar.

Equations

• ⋯ = ⋯

Constructors from lower manuscript-shaped packets

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

Assemble the fourth-pass actual central-pushout packet from lower packets.

The square/polar side is obtained from the standard same-family determinant packets and the theorem-level extraspecial comparison. The determinant side is obtained from the four semantic prop:simpleheaddet packets for exactly the semantic family projected from that actual scalar pushout.

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

Current square/polar packet through the fourth-pass actual scalar family.

Its closure avoids the old minimalBlock_preheadCentralPushoutSquarePolarData axiom; the remaining square/polar assumptions are the lower standard same-family family, diagonal, and polar packets.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData_from_actualClosers4 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (S : MinimalBlockPreheadCentralPushoutSemanticData D), Nonempty (MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData S)

Actual determinant packet for the same actual scalar central-pushout family.

This does not prove the old axiom for an arbitrary semantic family S; it gives the route-relevant actual family P.actualScalar.toSemanticData together with the determinant packet for that same family.

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

Lower pushout route using the actual scalar family and same-family determinant pieces from this sidecar.

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

Determinant packet projection through the fourth-pass actual route.

Current integrated route with only the Section 7 extraspecial step swapped

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

Nonterminal Fourier branch through the current route, but with the Section 7 extraspecial central-pushout/determinant step supplied by this sidecar.

theorem Q2Presentation.Induction.boundaryFramed_recursive_branch_from_fourier_currentIntegrated2_actualClosers4 (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_currentIntegrated2_actualClosers4 (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_currentIntegrated2_actualClosers4 (p : FramedPair) : framedCountA p = framedCountQ p

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

Current integrated finite-surjection equality with the Section 7 extraspecial central-pushout/determinant step routed through ActualClosers4.

Alternate capstone theorem for axiom-closure auditing

theorem Q2Presentation.Induction.surj_counts_equal_actualClosers4 (G : Type) [Group G] [Finite 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 with [Nonempty G] discharged, using the fourth-pass actual central-pushout route.

theorem Q2Presentation.Induction.presentation_correct_actualClosers4 : Nonempty (GammaA ≅ GQ2Profinite)

Alternate capstone theorem using the fourth-pass actual central-pushout route, for direct final-closure auditing without editing PresentationCorrect.

Acceptance checks / exact residual report