Route152 Section 7 pushout/determinant closers

Route152 currently reaches the Section 7 determinant line through Section7PushoutRoute151Closers, whose audit closure contains the four Route82 residual packets:

• construction of the scalar-pushout pairing family phi_lambda;
• naturality of that pairing;
• annihilation of the extraspecial square on T;
• nonsingularity after descent to the simple head.

The manuscript proves the last three assertions for the scalar pushouts actually obtained from K_lambda = K / ker lambda, not for an arbitrary externally supplied pairing family. This sidecar therefore exposes the strict selected-family lowering supported by the current API: Route83's actual scalar pushout plus same-family coherent determinant packet is bridged to the Route82 packet shape, and the Route152 finite-count route is replayed with that lower pushout provider.

Manuscript anchors: Section 6 constructs the quadratic determinant obstruction from a central double cover and its square/polar pairing; Section 7, prop:simpleheaddet, proves annihilation on T and nonsingularity after descent to the simple head for the scalar pushouts in the prehead tower.

Bridge from actual scalar pushouts to the selected Route82 packet

theorem Q2Presentation.Induction.Section7PushoutRoute152Closers.route82SelectedSplitLeaves_of_route152ActualScalarCoherentDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute83Closers.MinimalBlockPreheadPushoutRoute83Data D) : ∃ (Phi : MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D), Nonempty (MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutPairingNaturalityDataRoute82 Phi) ∧ ∃ (Ann : MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutAnnihilationDataRoute82 Phi), Nonempty (MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutDescendedNonsingularDataRoute82 Phi Ann)

Bridge an actual scalar pushout plus same-family coherent determinant packet to the selected Route82 split leaves.

This is the manuscript-faithful replacement for the universal Route82 split axioms: the naturality, annihilation, and descended nonsingularity packets are for the Phi induced by the actual scalar pushout in P.

def Q2Presentation.Induction.Section7PushoutRoute152Closers.route82Data_of_route152ActualScalarCoherentDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute83Closers.MinimalBlockPreheadPushoutRoute83Data D) : MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadPushoutRoute82Data D

Bridge the same actual-scalar/coherent-determinant data to the coherent Route82 packet consumed by downstream Route81 projections.

Equations

• Q2Presentation.Induction.Section7PushoutRoute152Closers.route82Data_of_route152ActualScalarCoherentDeterminant P = P.toRoute82

Route152 selected lower providers

theorem Q2Presentation.Induction.Section7PushoutRoute152Closers.minimalBlock_preheadCentralPushoutPairingConstructionData_from_section7PushoutRoute152Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadCentralPushoutPairingConstructionDataRoute82 D)

Route152 replacement for the Route82 pairing-construction leaf.

The selected pairing is projected from the actual scalar pushout family rather than supplied by minimalBlock_preheadCentralPushoutPairingConstructionData_route82.

theorem Q2Presentation.Induction.Section7PushoutRoute152Closers.minimalBlock_preheadCentralPushoutRoute82SelectedSplitLeaves_from_section7PushoutRoute152Closers {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)

Selected Route82 split leaves for Route152.

This theorem strictly lowers the four Route82 residual axioms to the smaller actual-scalar/coherent-determinant interface. It deliberately exposes an existentially selected Phi; the current Lean API does not prove the manuscript's prop:simpleheaddet conclusions for arbitrary unrelated pairing families.

theorem Q2Presentation.Induction.Section7PushoutRoute152Closers.minimalBlock_preheadPushoutRoute82Data_from_section7PushoutRoute152Closers {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPushoutRoute82Closers.MinimalBlockPreheadPushoutRoute82Data D)

Coherent selected Route82 packet for Route152, without invoking the Route82 split-packet residual axioms.

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

Route152 lower pushout packet through the selected actual scalar pushout and coherent determinant packet.

theorem Q2Presentation.Induction.Section7PushoutRoute152Closers.minimalBlock_preheadDeterminantPackets_from_section7PushoutRoute152Closers {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 Route152 pushout line.

Compared with Section7PushoutRoute151Closers, its closure avoids the four Route82 residual axioms and instead uses the lower square/polar and semantic determinant facts that construct the selected actual scalar pushout family.

Route152 replay with only the pushout provider lowered further

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

Route152 nonterminal Fourier branch with the Route151 kernel provider unchanged and the pushout/determinant line routed through the selected actual-scalar/coherent-determinant bridge in this file.

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

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

Route152 finite-surjection equality with the pushout/determinant line lowered past the four Route82 residual axioms.