Route130 minimal-block pushout/determinant closer #

Route130's public pushout frontier is still the single coherent Section 7 atom

minimalBlock_preheadActualCentralExtensionPushoutData.

This sidecar keeps the promoted Route130 files untouched and reuses the Route127 pushout attack decomposition. The downstream provider has the same conclusion as MinimalBlockPushoutRoute122Closers.minimalBlock_preheadDeterminantPackets_from_route122, but its pushout closure is routed through Route83's actual-scalar plus coherent semantic determinant packets instead of the broad Route122 atom.

Route127-shaped pushout lowering, exposed for Route130 #

source

theorem Q2Presentation.Induction.MinimalBlockPushoutRoute130Closers.minimalBlock_preheadCentralPushoutPairingConstructionData_from_route130 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) :

Nonempty (MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D)

Route130 pairing-construction packet, obtained through the Route127 Route83-based decomposition.

source

theorem Q2Presentation.Induction.MinimalBlockPushoutRoute130Closers.minimalBlock_preheadCentralPushoutRoute82SplitPackets_from_route130 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) :

∃ (Phi : MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D), Nonempty (MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutPairingNaturalityDataRoute82 Phi) ∧ ∃ (Ann : MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutAnnihilationDataRoute82 Phi), Nonempty (MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutDescendedNonsingularDataRoute82 Phi Ann)

Route130 selected Route82 split packets, all tied to the same pairing selected by the Route127/Route83 decomposition.

source

theorem Q2Presentation.Induction.MinimalBlockPushoutRoute130Closers.minimalBlock_preheadPushoutRoute82Data_from_route130 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) :

Nonempty (MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadPushoutRoute82Data D)

Route130 coherent Route82 packet through the Route127/Route83 lowering.

source

theorem Q2Presentation.Induction.MinimalBlockPushoutRoute130Closers.minimalBlock_preheadActualCentralExtensionPushoutData_from_route130 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) :

Nonempty (MinimalBlockPreheadActualCentralExtensionPushoutData D)

Route130 reconstruction of the broad public pushout atom from the narrowed Route83 route. This does not call the broad atom axiom.

source

theorem Q2Presentation.Induction.MinimalBlockPushoutRoute130Closers.minimalBlock_preheadPushoutRouteLowerData_from_route130 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) :

Nonempty (MinimalBlockPreheadPushoutRouteLowerData D)

Route130 lower pushout packet through the Route127/Route83 lowering.

source

theorem Q2Presentation.Induction.MinimalBlockPushoutRoute130Closers.minimalBlock_preheadDeterminantPackets_from_route130 {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 Route130 pushout line.

This has the same downstream conclusion as MinimalBlockPushoutRoute122Closers.minimalBlock_preheadDeterminantPackets_from_route122, but routes through Route127/Route83's narrower actual-scalar and coherent determinant semantic packets.

Current Route130 audit route with only the pushout provider swapped #

source

theorem Q2Presentation.Induction.boundaryFramed_nonterminal_fourier_branch_currentIntegrated130_route130PushoutClosers (p : FramedPair) :

¬ScalarTerminal p → Nonempty (FourierBranchData p)

Route130 nonterminal Fourier branch with the pushout provider supplied by MinimalBlockPushoutRoute130Closers. The promoted Route130 files are not edited.

source

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

source

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

source

theorem Q2Presentation.Induction.boundaryFramed_counts_equal_currentIntegrated130_route130PushoutClosers (p : FramedPair) :

framedCountA p = framedCountQ p

source

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

Route130 finite-surjection equality with only the pushout/determinant line routed through the lower Route130 closer in this file.