Route138 Section 7 pushout/determinant closers

This sidecar leaves every routed/public file untouched. Route138 currently uses Section7PushoutRoute135Closers, whose determinant provider lowers the Section 7 pushout line to the four Route82 residual packets:

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

Here the same Route138 context is rebuilt with the pushout provider routed through MinimalBlockPushoutRoute83Closers. That provider avoids the four Route82 residual axioms by selecting one actual scalar-pushout family and one same-family coherent semantic determinant packet, matching manuscript Section 7 prop:simpleheaddet.

Route82 packet lowering

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

Route138 replacement for the Route82 pairing-construction leaf.

This proves the same nonempty conclusion as the Route82 construction axiom, but the selected pairing is projected from Route83's actual scalar-pushout family.

theorem Q2Presentation.Induction.Section7PushoutRoute138Closers.minimalBlock_preheadCentralPushoutRoute82SplitPackets_from_section7PushoutRoute138Closers {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)

Coherent selected Route82 split packets for Route138.

The remaining Route82 leaf statements for naturality, annihilation, and descended nonsingularity are not proved for an arbitrary externally supplied Phi; the route only needs them for the selected actual scalar-pushout family. This theorem exposes exactly that smaller manuscript-shaped residual.

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

Coherent Route82 packet for Route138, obtained without invoking the Route82 split-packet residual axioms.

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

Route138 pushout lower packet, routed through Route83's actual-scalar and coherent determinant packet rather than the Route82 residual axioms.

theorem Q2Presentation.Induction.Section7PushoutRoute138Closers.minimalBlock_preheadDeterminantPackets_from_section7PushoutRoute138Closers {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 Route138 pushout line.

Compared with Route138's current provider, this strictly lowers the four Route82 leaves to Route83's actual-scalar/coherent-semantic determinant interface.

Route138 context with only the pushout provider lowered further

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

Route138 nonterminal Fourier branch with candidate/target and kernel providers unchanged, and the Section 7 pushout provider routed through the Route83 actual-scalar/coherent-determinant lowering.

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

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

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