Route4 extraspecial/determinant closers

This sidecar keeps PresentationCorrect untouched. It replaces the seven current route3 Section 7 central-pushout residual targets by projections from one actual scalar central-extension pushout family:

• minimalBlock_preheadCentralPushoutQuadraticFamilyData;
• minimalBlock_preheadCentralPushoutSquareDiagonalData;
• minimalBlock_preheadCentralPushoutPolarSymmData;
• minimalBlock_preheadCentralPushoutNaturalitySemanticData;
• minimalBlock_preheadCentralPushoutDiagonalZeroSemanticData;
• minimalBlock_preheadCentralPushoutPolarZeroSemanticData;
• minimalBlock_preheadCentralPushoutRadicalContainmentSemanticData.

The route4 packet below is backed by the split actual K_lambda = K / ker lambda construction packets from MinimalBlockActualCentralExtensionPushoutProofs. Thus the square/polar and determinant projections all use the same actual scalar pushout family.

Same-family route4 packet

structure Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutRoute4Data {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Type

One actual scalar central-extension pushout family, used as the common source for the route3 square/polar and determinant residual targets.

• actualPushout : MinimalBlockPreheadActualCentralExtensionPushoutData D

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutRoute4Data.quadraticFamily {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutRoute4Data D) : MinimalBlockPreheadCentralPushoutQuadraticFamilyData D

The current quadratic-family packet projected from the actual pushout.

Equations

• P.quadraticFamily = P.actualPushout.toQuadraticFamily

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutRoute4Data.squareDiagonal {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutRoute4Data D) : MinimalBlockPreheadCentralPushoutSquareDiagonalData P.quadraticFamily

The square-diagonal packet for the same projected quadratic family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutRoute4Data.polarSymm {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutRoute4Data D) : MinimalBlockPreheadCentralPushoutPolarSymmData P.quadraticFamily

The polar-symmetry packet for the same projected quadratic family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutRoute4Data.semanticData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutRoute4Data D) : MinimalBlockPreheadCentralPushoutSemanticData D

The semantic central-pushout family obtained from the same actual pushout.

Equations

• P.semanticData = P.actualPushout.toSemanticData

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutRoute4Data.actualDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutRoute4Data D) : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData P.semanticData

The actual simple-head determinant packet for the same semantic family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutRoute4Data.naturality {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutRoute4Data D) : MinimalBlockPreheadCentralPushoutNaturalitySemanticData P.semanticData

Naturality of the same actual pushout family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutRoute4Data.diagonalZero {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutRoute4Data D) : MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData P.semanticData

Diagonal vanishing on T for the same actual pushout family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutRoute4Data.polarZero {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutRoute4Data D) : MinimalBlockPreheadCentralPushoutPolarZeroSemanticData P.semanticData

Polar vanishing on T x M for the same actual pushout family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutRoute4Data.radicalContainment {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutRoute4Data D) : MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData P.semanticData

Polar-radical containment for the same actual pushout family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutRoute4Data.toPushoutRouteLower {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutRoute4Data D) : MinimalBlockPreheadPushoutRouteLowerData D

Coherent lower route packet obtained from the same actual pushout family.

Equations

• P.toPushoutRouteLower = { selfDuality := P.semanticData.toSelfDuality, simpleHeadDeterminant := ⋯ }

Closures of the route3 residual targets from route4 data

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutRoute4Data_from_actualCentralExtension {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadCentralPushoutRoute4Data D)

Construct the route4 packet from the split actual central-extension packets.

The axiom closure of this theorem contains the split actual K_lambda construction packets, not the seven current route3 central-pushout residual axioms.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutRoute4_residualPackets {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (Q : MinimalBlockPreheadCentralPushoutQuadraticFamilyData D), Nonempty (MinimalBlockPreheadCentralPushoutSquareDiagonalData Q) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarSymmData Q) ∧ ∃ (S : MinimalBlockPreheadCentralPushoutSemanticData D), Nonempty (MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutPolarZeroSemanticData S) ∧ Nonempty (MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData S)

The seven route3 central-pushout/determinant targets, all projected from one actual scalar central-extension pushout family.

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

Route-ready lower pushout packet through route4.

Current integrated route with only the Section 7 pushout step swapped

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

Nonterminal Fourier branch using the current route3 kernel/target path and the route4 actual scalar central-extension pushout packet.

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

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

Current integrated finite-surjection equality with route4 supplying the Section 7 actual scalar central-extension pushout step.

theorem Q2Presentation.Induction.surj_counts_equal_currentIntegrated3_route4 (G : Type) [Group G] [Finite G] : Cardinal.mk (Profinite.SurjContHom GammaA (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G))) = Cardinal.mk (Profinite.SurjContHom GQ2Profinite (ProfiniteGrp.ofFiniteGrp (FiniteGrp.of G)))

Equal finite surjection counts with [Nonempty G] discharged, using route4.

theorem Q2Presentation.Induction.presentation_correct_currentIntegrated3_route4 : Nonempty (GammaA ≅ GQ2Profinite)

Alternate capstone theorem for auditing route4 without editing PresentationCorrect.

Acceptance checks / exact residual report