Route167 Section 7 pushout/determinant lowering

Route166 reaches the Section 7 pushout/determinant line through Section7PushoutRoute164Closers.minimalBlock_preheadDeterminantPackets_from_section7PushoutRoute164Closers. Its pushout frontier contains the two Route164 actual atoms:

• minimalBlock_preheadActualScalarCentralPushoutData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

This sidecar exports a drop-in determinant provider with the same downstream consumer shape, but routes through the split actual central-extension packet from MinimalBlockPushoutRoute29Proofs. The replacement frontier is the strictly lower same-family scalar central-extension split:

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

Manuscript anchors: Section 6 constructs determinant obstructions from central double covers and their square/polar forms; Section 7, prop:simpleheaddet, applies this to the scalar pushouts K_lambda = K / ker lambda.

Lower selected pushout source

theorem Q2Presentation.Induction.Section7PushoutRoute167Closers.minimalBlock_pushoutRoute29ActualCentralExtensionSplitData_from_section7PushoutRoute167Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPushoutRoute29ActualCentralExtensionSplitData D)

Route167 actual central-extension split source.

This is the lower source under the two Route166 actual pushout atoms. Its axiom closure is the split actual central-extension frontier, not the broad actual scalar-pushout or bundled simple-head determinant atoms.

theorem Q2Presentation.Induction.Section7PushoutRoute167Closers.minimalBlock_preheadRoute166PushoutAtoms_from_section7PushoutRoute167Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (P : MinimalBlockPushoutRoute29ActualCentralExtensionSplitData D), Nonempty (MinimalBlockPreheadActualScalarCentralPushoutData D) ∧ Nonempty (MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData P.actualScalar.toSemanticData)

Audit-facing bridge: the two Route166 actual pushout atom surfaces are theorem-level projections of the Route167 split actual central-extension data.

The proof does not call either Route166 actual atom provider.

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

Route167 lower pushout packet through the split actual central-extension frontier.

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

Drop-in replacement for Section7PushoutRoute164Closers.minimalBlock_preheadDeterminantPackets_from_section7PushoutRoute164Closers.

The theorem has the same consumer shape as the Route164 provider, but its axiom frontier replaces the two Route166 actual pushout atoms by the split actual central-extension packets listed in the module header.

Route166 replay with only the pushout provider swapped

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

Route166 nonterminal Fourier branch replayed with the Route167 pushout/determinant provider.

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

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

Route166 finite-surjection equality replay with the Route167 pushout/determinant lowering.