Route157 Section 7 pushout/determinant lowering

Route156 still reaches the Section 7 pushout/determinant line through Section7PushoutRoute152Closers.minimalBlock_preheadDeterminantPackets_from_section7PushoutRoute152Closers. Its finite-count closure contains the seven Route28/Route156 determinant atoms:

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

This sidecar does not edit the integrated route. It exports a drop-in replacement determinant provider and a Route156 replay whose only change is the pushout provider. The replacement is routed through Route29's actual central-extension split packets:

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

Manuscript anchors: Section 6 constructs the scalar determinant obstruction from a central double cover and its square/polar form; Section 7, prop:simpleheaddet, proves naturality, annihilation on T, and radical containment for the actual scalar pushouts K_lambda = K / ker lambda.

Lower selected pushout surface

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

Route157 actual central-extension split source.

This is the lower source for the seven Route156 pushout/determinant atoms. Its axiom closure is the split actual central-extension frontier, not the broad Route28 semantic atom frontier.

theorem Q2Presentation.Induction.Section7PushoutRoute157Closers.minimalBlock_preheadRoute156PushoutAtoms_from_section7PushoutRoute157Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (P : MinimalBlockPushoutRoute29ActualCentralExtensionSplitData D), Nonempty (MinimalBlockPreheadCentralPushoutQuadraticFamilyData D) ∧ Nonempty (MinimalBlockPreheadCentralPushoutSquareDiagonalData P.quadraticFamily) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarSymmData P.quadraticFamily) ∧ Nonempty (MinimalBlockPreheadCentralPushoutNaturalitySemanticData P.semantic) ∧ Nonempty (MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData P.semantic) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarZeroSemanticData P.semantic) ∧ Nonempty (MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData P.semantic)

The selected Route156 seven-atom surface, reconstructed from the lower actual central-extension split packets.

This theorem is audit-facing: it shows that the old seven conclusions are available for the selected same-family P, but the proof does not call the old seven residual providers.

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

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

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

Drop-in replacement for Section7PushoutRoute152Closers.minimalBlock_preheadDeterminantPackets_from_section7PushoutRoute152Closers.

The theorem has the same consumer shape as the Route152 provider, but its axiom frontier is strictly lower: it uses the split actual central-extension packets instead of the seven Route156 pushout/determinant atoms.

Route156 replay with only the pushout provider swapped

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

Route156 nonterminal Fourier branch replayed with the Route157 pushout/determinant provider.

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

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

Route156 finite-surjection equality replay with the Route157 pushout/determinant lowering.