Route143 Section 7 actual pushout closers

This sidecar keeps the public route untouched and replaces only the Route143 Section 7 determinant/pushout provider.

Route143 currently exposes the five extraspecial/self-duality atoms

• minimalBlock_preheadCentralPushoutSelfDualityData,
• minimalBlock_preheadExtraspecialNaturalityData,
• minimalBlock_preheadExtraspecialDiagonalZeroData,
• minimalBlock_preheadExtraspecialPolarZeroData, and
• minimalBlock_preheadExtraspecialRadicalContainmentData.

The replacement below routes the same downstream determinant packet through the Route88 actual-pushout packet already used by Route142. Thus the five Route143 atoms are replaced by the two manuscript-level actual packets:

• minimalBlock_preheadActualScalarCentralPushoutData;
• minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData.

Actual packet hooks

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

Route143 actual scalar-pushout / actual determinant packet.

This is the same coherent manuscript-shaped packet used by Route142, but exposed under a Route143 name so it can replace the pushout provider in IntegratedCurrentRouteProofs143AllLowered.

theorem Q2Presentation.Induction.Section7PushoutRoute143ActualClosers.minimalBlock_preheadRoute143PushoutAtoms_from_section7PushoutRoute143ActualClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (P : MinimalBlockPushoutRoute88Closers.MinimalBlockPreheadPushoutRoute88Data D), Nonempty (MinimalBlockPreheadCentralPushoutSelfDualityData D) ∧ Nonempty (MinimalBlockPreheadExtraspecialNaturalityData P.toPushoutRouteLower.extraspecialFamily) ∧ Nonempty (MinimalBlockPreheadExtraspecialDiagonalZeroData P.toPushoutRouteLower.equivariantFamily) ∧ Nonempty (MinimalBlockPreheadExtraspecialPolarZeroData P.toPushoutRouteLower.equivariantFamily) ∧ Nonempty (MinimalBlockPreheadExtraspecialRadicalContainmentData P.toPushoutRouteLower.equivariantFamily)

Projection of the Route143 five-atom surface from the coherent actual packet.

This theorem is audit-facing: it shows that the old self-duality, naturality, diagonal-zero, polar-zero, and radical-containment packet surfaces are all theorem-level projections from one same-family actual scalar pushout and simple-head determinant theorem.

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

Route143 lower pushout packet through the actual scalar-pushout / actual simple-head determinant packet.

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

Drop-in determinant-packet provider for the Route143 Fourier branch.

This has the same consumer shape as Section7PushoutRoute141SemanticClosers.minimalBlock_preheadDeterminantPackets_from_section7PushoutRoute141SemanticClosers, but its axiom closure is the two actual packet residuals rather than the five Route143 extraspecial/self-duality atoms.

Integrated Route143 variant with only the pushout provider swapped

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

Route143 nonterminal Fourier branch with the current Route143 kernel and Section 8 providers unchanged, and with the pushout provider routed through the actual scalar-pushout / actual determinant packet.

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

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

Route143 finite-surjection equality with the pushout/determinant frontier lowered from five independent Route143 atoms to the two actual packet atoms.