Route145 Section 7 actual pushout/determinant lowering

This sidecar leaves the Route144 integrated file untouched. It exports the same determinant-packet consumer shape as Section7PushoutRoute143ActualClosers.minimalBlock_preheadDeterminantPackets_from_section7PushoutRoute143ActualClosers, but proves the two Route144 pushout residuals from lower manuscript-shaped pieces:

• minimalBlock_preheadActualScalarCentralPushoutData is reconstructed from minimalBlock_preheadCentralPushoutSquarePolarData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData is reconstructed from the four same-family simple-head determinant pieces: naturality, diagonal zero, polar zero, and radical containment.

The integrated Route145 theorem below reuses the Route144 kernel and Section 8 providers, changing only the Section 7 determinant/pushout provider.

Lower projections for the two Route144 pushout leaves

theorem Q2Presentation.Induction.Section7PushoutRoute145ActualClosers.minimalBlock_preheadActualScalarCentralPushoutData_from_section7PushoutRoute145ActualClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadActualScalarCentralPushoutData D)

Route145 scalar-pushout projection.

This proves the current actual scalar-pushout packet from the lower coherent square/polar packet, so the axiom closure no longer contains minimalBlock_preheadActualScalarCentralPushoutData.

theorem Q2Presentation.Induction.Section7PushoutRoute145ActualClosers.minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData_from_section7PushoutRoute145ActualClosers {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : Nonempty (MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData S)

Route145 actual determinant projection.

This proves the current bundled actual determinant packet from the four same-family final determinant pieces, so the axiom closure no longer contains minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

Route145 packet provider

theorem Q2Presentation.Induction.Section7PushoutRoute145ActualClosers.minimalBlock_preheadPushoutRoute88Data_from_section7PushoutRoute145ActualClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPushoutRoute88Closers.MinimalBlockPreheadPushoutRoute88Data D)

Route145 selected actual-pushout / actual-determinant packet.

It has the same downstream shape as Route143/Route142's Route88 packet, but its closure is lower than Route88's two actual residual axioms.

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

Route145 lower pushout packet, projected from the selected Route88-shaped packet.

theorem Q2Presentation.Induction.Section7PushoutRoute145ActualClosers.minimalBlock_preheadDeterminantPackets_from_section7PushoutRoute145ActualClosers {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 Route143/Route144 Fourier branch.

Integrated Route145 variant

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

Route145 nonterminal Fourier branch: Route144 kernel and Section 8 providers, with only the Section 7 determinant/pushout provider replaced by Section7PushoutRoute145ActualClosers.

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

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

Route145 finite-surjection equality with Route144's kernel/Section 8 providers and the Route145 §7 determinant/pushout lowering.