Route141 Section 7 pushout semantic closers

This sidecar keeps the public route and all existing Route141 files untouched. The Route141 implementation frontier exposes seven Section 7 pushout/determinant semantic atoms:

• the central-pushout quadratic family, square-diagonal, and polar-symmetry packets;
• central-pushout naturality, diagonal-zero, polar-zero, and radical-containment packets.

The replacement below routes the same downstream determinant provider through the lower extraspecial/self-duality surface already available in MinimalBlockActualCentralExtensionClosers2. Thus the integrated route no longer depends on the seven central-pushout semantic atoms.

Lower semantic packet hooks

def Q2Presentation.Induction.Section7PushoutRoute141SemanticClosers.semanticOfSelfDuality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSelfDualityData D) : MinimalBlockPreheadCentralPushoutSemanticData D

The central-pushout semantic family selected from the lower self-duality packet. The induced square is the extraspecial square of this same family, so the square-diagonal and polar-symmetry fields are definitional projections.

Equations

• Q2Presentation.Induction.Section7PushoutRoute141SemanticClosers.semanticOfSelfDuality S = { phi := S.phi }

theorem Q2Presentation.Induction.Section7PushoutRoute141SemanticClosers.minimalBlock_preheadCentralPushoutSquarePolarPackets_from_section7PushoutRoute141SemanticClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (Q : MinimalBlockPreheadCentralPushoutQuadraticFamilyData D), Nonempty (MinimalBlockPreheadCentralPushoutSquareDiagonalData Q) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarSymmData Q)

Route141 replacement for the first three central-pushout semantic atoms.

The chosen quadratic family is induced from one lower self-duality packet, and the diagonal/polar identities are theorem-level projections of the extraspecial square attached to that same phi_lambda.

theorem Q2Presentation.Induction.Section7PushoutRoute141SemanticClosers.minimalBlock_preheadCentralPushoutDeterminantSemanticPackets_from_section7PushoutRoute141SemanticClosers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (S : MinimalBlockPreheadCentralPushoutSemanticData D), Nonempty (MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarZeroSemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData S)

Route141 replacement for the four central-pushout determinant-semantic atoms.

The same lower self-duality family supplies the semantic phi; naturality, diagonal-zero, polar-zero, and radical-containment are converted from the lower extraspecial packet surface for that same family.

theorem Q2Presentation.Induction.Section7PushoutRoute141SemanticClosers.minimalBlock_preheadDeterminantPackets_from_section7PushoutRoute141SemanticClosers {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 Route141 Fourier branch.

Compared with the Route141 provider, the axiom closure replaces the seven named central-pushout semantic atoms by the lower self-duality and extraspecial naturality/zero/radical packets.

Route141 integration with only the pushout semantic provider swapped

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

Route141 nonterminal Fourier branch with candidate/target/kernel providers unchanged, and the Section 7 pushout provider routed through the Route141 semantic closer above.

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

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

Route141 finite-surjection equality with the Section 7 pushout semantic frontier lowered.