Route10 actual central-extension pushout closure

This sidecar leaves the integrated route files untouched. It gives route10 a single coherent Section 7 actual central-extension / quadratic pushout provider and projects the seven current P5 packet targets from that same family:

• minimalBlock_preheadActualCentralExtensionPhiData;
• minimalBlock_preheadActualCentralExtensionSquareData;
• minimalBlock_preheadActualCentralExtensionDiagonalData;
• minimalBlock_preheadActualCentralExtensionPolarData;
• minimalBlock_preheadActualCentralExtensionNaturalityData;
• minimalBlock_preheadActualCentralExtensionAnnihilationData;
• minimalBlock_preheadActualCentralExtensionRadicalContainmentData.

The remaining floor is the narrower actual semantic packet from MinimalBlockExtraspecialClosers3: the actual square/polar central-pushout family and the same-family simple-head determinant theorem. Thus the route10 hooks below avoid the seven P5 packet axioms and keep all square, polar, naturality, annihilation, and radical fields tied to one pushout family.

One route10 P5 family

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

The route10 P5 family: one coherent actual central-pushout/extraspecial packet from which all actual central-extension split packets are projected.

• actual : MinimalBlockPreheadCentralPushoutExtraspecialActualData D

def Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionRoute10Data.phiData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadActualCentralExtensionRoute10Data D) : MinimalBlockPreheadActualCentralExtensionPhiData D

The actual phi_lambda packet for the route10 family.

Equations

• P.phiData = P.actual.toActualPhi

def Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionRoute10Data.squareData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadActualCentralExtensionRoute10Data D) : MinimalBlockPreheadActualCentralExtensionSquareData P.phiData

The actual square map packet for the same route10 family.

Equations

• P.squareData = P.actual.toActualSquare

def Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionRoute10Data.diagonalData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadActualCentralExtensionRoute10Data D) : MinimalBlockPreheadActualCentralExtensionDiagonalData P.squareData

The diagonal identity for the same route10 square map.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionRoute10Data.polarData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadActualCentralExtensionRoute10Data D) : MinimalBlockPreheadActualCentralExtensionPolarData P.squareData

The polar identity for the same route10 square map.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionRoute10Data.naturalityData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadActualCentralExtensionRoute10Data D) : MinimalBlockPreheadActualCentralExtensionNaturalityData P.phiData

Naturality for the same route10 phi_lambda family.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionRoute10Data.annihilationData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadActualCentralExtensionRoute10Data D) : MinimalBlockPreheadActualCentralExtensionAnnihilationData P.squareData

Annihilation on T for the same route10 square map.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionRoute10Data.radicalContainmentData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadActualCentralExtensionRoute10Data D) : MinimalBlockPreheadActualCentralExtensionRadicalContainmentData P.squareData

Polar-radical containment for the same route10 square map.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionRoute10Data.pushoutData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadActualCentralExtensionRoute10Data D) : MinimalBlockPreheadActualCentralExtensionPushoutData D

Reassemble the broad actual central-extension pushout packet from the same route10 family.

Equations

• P.pushoutData = P.actual.toActualCentralExtensionPushoutData

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

Route4 data projected from the same route10 actual pushout.

Equations

• P.route4Data = { actualPushout := P.pushoutData }

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

Lower pushout-route packet projected from the same route10 actual pushout.

Equations

• P.toPushoutRouteLower = P.route4Data.toPushoutRouteLower

P5 packet replacements

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

Construct the route10 P5 family from the coherent actual pushout packet.

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

Route10 replacement for the PhiData packet.

theorem Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionSquareData_from_route10Proofs {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadActualCentralExtensionPhiData D) : Nonempty (MinimalBlockPreheadActualCentralExtensionSquareData Phi)

Route10 replacement for the SquareData packet, using the extraspecial square attached to the supplied phi family.

theorem Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionDiagonalData_from_route10Proofs {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadActualCentralExtensionPhiData D) : Nonempty (MinimalBlockPreheadActualCentralExtensionDiagonalData (MinimalBlockPreheadActualCentralExtensionSquareData.ofPhi Phi))

Route10 replacement for the DiagonalData packet for the route square ofPhi Phi.

theorem Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionPolarData_from_route10Proofs {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (Phi : MinimalBlockPreheadActualCentralExtensionPhiData D) : Nonempty (MinimalBlockPreheadActualCentralExtensionPolarData (MinimalBlockPreheadActualCentralExtensionSquareData.ofPhi Phi))

Route10 replacement for the PolarData packet for the route square ofPhi Phi.

theorem Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionNaturalityData_from_route10Proofs {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadActualCentralExtensionRoute10Data D) : Nonempty (MinimalBlockPreheadActualCentralExtensionNaturalityData P.phiData)

Route10 naturality packet for the phi family projected from one actual pushout provider.

theorem Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionAnnihilationData_from_route10Proofs {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadActualCentralExtensionRoute10Data D) : Nonempty (MinimalBlockPreheadActualCentralExtensionAnnihilationData P.squareData)

Route10 annihilation packet for the square projected from one actual pushout provider.

theorem Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionRadicalContainmentData_from_route10Proofs {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadActualCentralExtensionRoute10Data D) : Nonempty (MinimalBlockPreheadActualCentralExtensionRadicalContainmentData P.squareData)

Route10 radical-containment packet for the square projected from one actual pushout provider.

theorem Q2Presentation.Induction.minimalBlock_preheadActualCentralExtensionPackets_from_route10Proofs {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : ∃ (Phi : MinimalBlockPreheadActualCentralExtensionPhiData D) (Q : MinimalBlockPreheadActualCentralExtensionSquareData Phi), Nonempty (MinimalBlockPreheadActualCentralExtensionDiagonalData Q) ∧ Nonempty (MinimalBlockPreheadActualCentralExtensionPolarData Q) ∧ Nonempty (MinimalBlockPreheadActualCentralExtensionNaturalityData Phi) ∧ Nonempty (MinimalBlockPreheadActualCentralExtensionAnnihilationData Q) ∧ Nonempty (MinimalBlockPreheadActualCentralExtensionRadicalContainmentData Q)

All seven P5 packet targets, projected from one route10 actual pushout family.

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

Broad actual central-extension pushout packet through the route10 P5 provider.

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

Route4 actual central-pushout packet through the route10 P5 provider.

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

Route-ready lower pushout packet through the route10 P5 provider.

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

Determinant packet projection through the route10 P5 provider.

Route10 hook with only P5 swapped

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

Route10 nonterminal Fourier branch with the P5 actual central-extension step supplied by this sidecar.

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

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

Route10 finite-surjection equality with the P5 actual central-extension step supplied by this sidecar.

Acceptance checks / exact residual report