Route135 Section 7 pushout/determinant closers

This sidecar leaves all routed files untouched. It keeps the current Route135 candidate/target and Section 7 kernel providers, but replaces the Section 7 pushout/determinant provider by the Route82 scalar-pushout packetization.

The Route82 frontier is closer to the manuscript's prop:simpleheaddet:

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

Consequently the current Route135 pushout leaves minimalBlock_preheadCentralPushoutQuadraticFamilyData, minimalBlock_preheadCentralPushoutSquareDiagonalData, minimalBlock_preheadCentralPushoutPolarSymmData, and minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData are avoided by the route-context theorem below.

Pushout packet lowering

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

Route135 pushout/determinant packets lowered to the Route82 prop:simpleheaddet packetization.

This is the route-level provider consumed below. Its downstream shape matches the current Route135 determinant provider, but its axiom closure is the Route82 four-packet frontier rather than the current square/diagonal/polar/actual determinant leaves.

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

The current split square/polar family packets, reconstructed from the same Route82 scalar-pushout construction.

The existential form is intentional: it supplies one coherent same-family quadratic packet and its diagonal/polar witnesses, which is what the route needs.

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

The actual same-family simple-head determinant packet reconstructed from Route82's construction/naturality/annihilation/descended-nonsingularity packets.

theorem Q2Presentation.Induction.Section7PushoutRoute135Closers.minimalBlock_preheadCentralPushoutRoute135Leaves_from_route82Packets {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : (∃ (Q : MinimalBlockPreheadCentralPushoutQuadraticFamilyData D), Nonempty (MinimalBlockPreheadCentralPushoutSquareDiagonalData Q) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarSymmData Q)) ∧ ∃ (S : MinimalBlockPreheadCentralPushoutSemanticData D), Nonempty (MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData S)

One audit theorem exposing all four current Route135 pushout packet surfaces, but supplied from the lower Route82 packetization.

Route135 context with only pushout provider swapped

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

Route135 nonterminal Fourier branch with candidate/target and kernel providers unchanged, and only the Section 7 pushout provider lowered to Route82.

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

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

Route135 finite-surjection equality with only the Section 7 pushout provider lowered to the Route82 scalar-pushout packets.