Route63 minimal-block pushout/determinant closers

Route62's integrated theorem still consumes minimalBlock_preheadDeterminantPackets_from_route60, whose axiom closure contains five Route60 determinant-pushout atoms. This sidecar leaves routed files untouched and reconstructs the same Route60 packet surface from the lower standard/extraspecial pushout packets already exposed by the Section 7 semantic API.

The main exported replacement is minimalBlock_preheadDeterminantPackets_from_route63. It has the same downstream surface as the Route60 provider, but its closure avoids the five Route60 atoms:

• minimalBlock_route60ScalarPushoutPairingData;
• minimalBlock_route60PairingNaturalityData;
• minimalBlock_route60DiagonalVanishingOnTData;
• minimalBlock_route60PolarVanishingOnTData;
• minimalBlock_route60PolarRadicalContainmentData.

For integration auditing, the file also mirrors the current Route62 final theorems under currentIntegrated63 names without editing IntegratedCurrentRouteProofs62.lean or PresentationCorrect.lean.

Semantic pushout packets as Route60 packets

def Q2Presentation.Induction.MinimalBlockRoute60ScalarPushoutPairingData.ofSemantic {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (S : MinimalBlockPreheadCentralPushoutSemanticData D) : MinimalBlockRoute60ScalarPushoutPairingData D

Reindex a semantic central-pushout family as the Route60 scalar pushout pairing family.

Equations

• Q2Presentation.Induction.MinimalBlockRoute60ScalarPushoutPairingData.ofSemantic S = { phi := S.phi }

def Q2Presentation.Induction.MinimalBlockRoute60PairingNaturalityData.ofSemantic {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (N : MinimalBlockPreheadCentralPushoutNaturalitySemanticData S) : MinimalBlockRoute60PairingNaturalityData (MinimalBlockRoute60ScalarPushoutPairingData.ofSemantic S)

Project semantic central-pushout naturality to Route60 naturality for the same pairing family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockRoute60DiagonalVanishingOnTData.ofSemantic {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (Z : MinimalBlockPreheadCentralPushoutDiagonalZeroSemanticData S) : MinimalBlockRoute60DiagonalVanishingOnTData (MinimalBlockRoute60ScalarPushoutPairingData.ofSemantic S)

Project semantic diagonal vanishing to Route60 diagonal vanishing for the same pairing family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockRoute60PolarVanishingOnTData.ofSemantic {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (P : MinimalBlockPreheadCentralPushoutPolarZeroSemanticData S) : MinimalBlockRoute60PolarVanishingOnTData (MinimalBlockRoute60ScalarPushoutPairingData.ofSemantic S)

Project semantic polar vanishing to Route60 polar vanishing for the same pairing family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockRoute60PolarRadicalContainmentData.ofSemantic {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} {S : MinimalBlockPreheadCentralPushoutSemanticData D} (R : MinimalBlockPreheadCentralPushoutRadicalContainmentSemanticData S) : MinimalBlockRoute60PolarRadicalContainmentData (MinimalBlockRoute60ScalarPushoutPairingData.ofSemantic S)

Project semantic radical containment to Route60 radical containment for the same pairing family.

Equations

• ⋯ = ⋯

Coherent Route63 packet and Route60-compatible exports

theorem Q2Presentation.Induction.minimalBlock_route60ScalarPushoutPackets_from_route63 {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (F : MinimalBlockRoute60ScalarPushoutPairingData D), Nonempty (MinimalBlockRoute60PairingNaturalityData F) ∧ Nonempty (MinimalBlockRoute60DiagonalVanishingOnTData F) ∧ Nonempty (MinimalBlockRoute60PolarVanishingOnTData F) ∧ Nonempty (MinimalBlockRoute60PolarRadicalContainmentData F)

Route63 coherent replacement for the five independent Route60 atoms.

The existential keeps the actual scalar pushout family tied to the four determinant facts, which is the surface needed to rebuild MinimalBlockPushoutRoute60Data without using any of the Route60 axioms.

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

Rebuild the Route60 packet from Route63's coherent lower packet.

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

Route60-shaped determinant-packet provider supplied by Route63.

This is intended as a drop-in replacement for minimalBlock_preheadDeterminantPackets_from_route60.

Route63 integrated audit theorem

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

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

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

Acceptance checks / exact residual report