Route126 minimal-block pushout/determinant closer

Route126 currently consumes

• MinimalBlockPushoutRoute122Closers.minimalBlock_preheadDeterminantPackets_from_route122,

whose pushout/determinant frontier is the single broad Section 7 atom

• minimalBlock_preheadActualCentralExtensionPushoutData.

This sidecar leaves the public integrated route files untouched and exports a Route126-named provider with the same downstream determinant-packet shape. It routes through the Route82 central-pushout packets, where the actual square is the extraspecial square attached to one scalar-pushout pairing family and the simple-head proof is split into annihilation on T and descended nonsingularity.

Residual effect for the determinant provider:

• removed: minimalBlock_preheadActualCentralExtensionPushoutData;
• added: MinimalBlockPushoutRoute82Closers.minimalBlock_preheadCentralPushoutPairingConstructionData_route82; MinimalBlockPushoutRoute82Closers.minimalBlock_preheadCentralPushoutPairingNaturalityData_route82; MinimalBlockPushoutRoute82Closers.minimalBlock_preheadCentralPushoutAnnihilationData_route82; MinimalBlockPushoutRoute82Closers.minimalBlock_preheadCentralPushoutDescendedNonsingularData_route82.

The first hook below also reconstructs the old broad actual central-extension packet from those four atoms, for audit purposes, without calling the old broad axiom.

Route126 broad-packet reduction hook

def Q2Presentation.Induction.MinimalBlockPushoutRoute126Closers.actualCentralExtensionPushoutDataOfRoute82 {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadPushoutRoute82Data D) : MinimalBlockPreheadActualCentralExtensionPushoutData D

Reconstruct the current broad actual central-extension pushout packet from the lower Route82 packets.

This is an audit hook: it has the old broad packet conclusion, but its axiom closure is the four concrete Route82 atoms rather than minimalBlock_preheadActualCentralExtensionPushoutData.

Equations

• One or more equations did not get rendered due to their size.

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

Route126 reduction of the broad actual central-extension pushout atom to the four lower Route82 packets.

Route-ready provider

theorem Q2Presentation.Induction.MinimalBlockPushoutRoute126Closers.minimalBlock_preheadCentralPushoutActualPackets_from_route126 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (S : MinimalBlockPreheadCentralPushoutSemanticData D), Nonempty (MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData S)

Route126 selected semantic family and actual simple-head determinant packet, both projected from the same Route82 scalar-pushout construction.

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

Route126 lower pushout packet through the Route82 concrete central-pushout packets.

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

Drop-in replacement for MinimalBlockPushoutRoute122Closers.minimalBlock_preheadDeterminantPackets_from_route122.

It has the same downstream conclusion consumed by the nonterminal Fourier branch, but avoids the broad Route122 central-extension atom and uses the four Route82 Section 7 atoms listed in the module header.

Current Route126 audit route with only the pushout provider swapped

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

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

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

Route126 finite-surjection equality with the pushout/determinant line routed through the lower Route82 central-pushout atoms.