Route175 Section 7 actual pushout/determinant lowering

Route173 reaches the Section 7 pushout/determinant line through Section7PushoutRoute167Closers.minimalBlock_preheadDeterminantPackets_from_section7PushoutRoute167Closers. Its pushout frontier is the seven split actual central-extension packets:

• minimalBlock_preheadActualCentralExtensionPhiData;
• minimalBlock_preheadActualCentralExtensionSquareData;
• minimalBlock_preheadActualCentralExtensionDiagonalData;
• minimalBlock_preheadActualCentralExtensionPolarData;
• minimalBlock_preheadActualCentralExtensionNaturalityData;
• minimalBlock_preheadActualCentralExtensionAnnihilationData;
• minimalBlock_preheadActualCentralExtensionRadicalContainmentData.

This sidecar exports a drop-in determinant provider with the same downstream consumer shape as the Route167 provider, but routes through the actual semantic central-pushout split from MinimalBlockExtraspecialClosers3.

Replacement frontier:

• minimalBlock_preheadCentralPushoutSquarePolarData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

This is a strict manuscript-level split of the seven actual central-extension packets: the square/polar construction of the actual scalar pushouts is kept separate from the simple-head determinant theorem for the same semantic family. It is not the broad minimalBlock_preheadActualCentralExtensionPushoutData wrapper used by Route172.

Route175 actual central-extension provider

theorem Q2Presentation.Induction.Section7PushoutRoute175ActualClosers.minimalBlock_preheadActualCentralExtensionPackets_from_section7PushoutRoute175ActualClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (Phi : MinimalBlockPreheadActualCentralExtensionPhiData D) (Q : MinimalBlockPreheadActualCentralExtensionSquareData Phi), Nonempty (MinimalBlockPreheadActualCentralExtensionDiagonalData Q) ∧ Nonempty (MinimalBlockPreheadActualCentralExtensionPolarData Q) ∧ Nonempty (MinimalBlockPreheadActualCentralExtensionNaturalityData Phi) ∧ Nonempty (MinimalBlockPreheadActualCentralExtensionAnnihilationData Q) ∧ Nonempty (MinimalBlockPreheadActualCentralExtensionRadicalContainmentData Q)

Audit-facing lowering of the seven Route173 actual central-extension packet targets to the actual semantic square-polar construction plus the actual simple-head determinant theorem.

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

Lower pushout-route packet through the actual semantic central-pushout split.

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

Drop-in replacement for Section7PushoutRoute167Closers.minimalBlock_preheadDeterminantPackets_from_section7PushoutRoute167Closers.

The theorem has the same consumer shape as the Route167 provider. Its closure removes all seven split actual central-extension atoms and replaces them by the two actual semantic pushout/determinant atoms listed in the module header.

Route173 replay with only the pushout provider swapped

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

Route173 nonterminal Fourier branch replayed with the Route175 pushout/determinant provider.

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

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

Route173 finite-surjection equality replay with only the Section 7 pushout/determinant provider swapped to Route175.