Route101 minimal-block pushout/determinant closer

IntegratedCurrentRouteProofs101 still consumes the Route98 pushout provider

• minimalBlock_preheadDeterminantPackets_from_route98,

whose closure passes through the four Route82 residual packets. This sidecar keeps Route101's candidate, target, and kernel providers unchanged, and swaps only the determinant/pushout provider to the lower actual-central-extension closer from MinimalBlockActualCentralExtensionClosers2.

The resulting pushout frontier avoids the four Route82 packet axioms and is strictly lower: it is the manuscript-shaped extraspecial/simple-head interface used to build the actual central-extension packet.

Route101 drop-in pushout providers

theorem Q2Presentation.Induction.MinimalBlockPushoutRoute101Closers.minimalBlock_preheadActualCentralExtensionPushoutData_from_route101 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadActualCentralExtensionPushoutData D)

Route101 broad actual central-extension pushout provider, routed through the extraspecial/simple-head actual central-extension closer instead of Route82.

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

Route101 lower pushout packet with the four Route82 residuals replaced by the lower extraspecial/simple-head packet interface.

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

Drop-in determinant-packet replacement for the Route101 pushout line.

This has the same conclusion as minimalBlock_preheadDeterminantPackets_from_route98, but its axiom closure no longer contains any of the four Route82 residual providers.

Route101 branch with only the pushout provider swapped

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

Route101 nonterminal branch with the determinant/pushout provider supplied by this sidecar. IntegratedCurrentRouteProofs101 is not edited.

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

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

Route101 finite-surjection equality with only the pushout provider swapped to this sidecar.