Route169 Section 7 pushout/determinant lowering

Route168 reaches the Section 7 pushout/determinant line through Section7PushoutRoute167Closers.minimalBlock_preheadDeterminantPackets_from_section7PushoutRoute167Closers. Its remaining 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 consumer shape as Route167, but routes through the lower Route12 central-pushout split. The replacement frontier is the finer manuscript square/polar and simple-head-determinant semantic family:

• minimalBlock_preheadCentralPushoutQuadraticFamilyData;
• minimalBlock_preheadCentralPushoutSquareDiagonalData;
• minimalBlock_preheadCentralPushoutPolarSymmData;
• minimalBlock_preheadCentralPushoutNaturalitySemanticData;
• minimalBlock_preheadCentralPushoutDiagonalZeroSemanticData;
• minimalBlock_preheadCentralPushoutPolarZeroSemanticData;
• minimalBlock_preheadCentralPushoutRadicalContainmentSemanticData.

Manuscript anchors: Section 6 constructs the square and polar determinant obstruction from the central double cover; Section 7, prop:simpleheaddet, proves the diagonal/polar vanishing on T and radical containment for the descended simple-head form.

Route169 pushout provider

theorem Q2Presentation.Induction.Section7PushoutRoute169Closers.minimalBlock_preheadCentralPushoutRoute12Data_from_section7PushoutRoute169Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadCentralPushoutRoute12Data D)

Route169 lower central-pushout packet.

This exposes the Route12 same-family packet used below, so the audit can see the new residual boundary directly.

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

Route169 lower pushout route through the Route12 central-pushout split.

theorem Q2Presentation.Induction.Section7PushoutRoute169Closers.minimalBlock_preheadDeterminantPackets_from_section7PushoutRoute169Closers {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 downstream consumer shape as the Route167 provider. Its axiom closure removes all seven Route168 actual-central-extension atoms and replaces them by Route12's lower central-pushout square/polar and semantic determinant atoms.

Route168 replay with only the pushout provider swapped

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

Route168 nonterminal Fourier branch replayed with the Route169 pushout/determinant provider.

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

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

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