Route18 actual central-extension / pushout sidecar

Route17 replaces the old pushout/determinant leaves by seven actual central-extension packets:

• actual phi_lambda;
• actual square map;
• diagonal and polar identities;
• naturality;
• annihilation on T;
• polar radical containment.

The current API still does not expose the quotient group object K_lambda = K / ker lambda from the manuscript. This sidecar therefore closes the seven Route17 packets for one coherent manuscript-shaped family built from:

• the concrete central-pushout square/polar packet; and
• the actual simple-head determinant packet for the semantic family projected from exactly that square/polar packet.

Thus the route-ready theorem below depends on two sharper pushout residuals, not the seven Route17 actual-central-extension residuals.

Route18 coherent actual packet

theorem Q2Presentation.Induction.MinimalBlockPreheadCentralPushoutSquarePolarData.square_eq_extraspecial {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutSquarePolarData D) (lam : Module.Dual (ZMod 2) D.R) : P.square lam = Quadratic.Extraspecial.extraspecialForm (P.phi lam)

The coherent square/polar packet determines the extraspecial quadratic form attached to the same pairing.

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

Route18 central-pushout data.

The determinant packet is indexed by the semantic family projected from the same square/polar packet, so the naturality, annihilation, and radical statements cannot drift to a different phi_lambda.

• squarePolar : MinimalBlockPreheadCentralPushoutSquarePolarData D
• determinantActual : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData { phi := self.squarePolar.phi }

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

The semantic central-pushout family projected from the Route18 packet.

Equations

• P.semantic = { phi := P.squarePolar.phi }

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

Route17 PhiData projected from the Route18 coherent packet.

Equations

• P.phiPacket = { phi := P.squarePolar.phi }

def Q2Presentation.Induction.MinimalBlockPushoutRoute18ActualDeterminantData.squarePacket {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute18ActualDeterminantData D) : MinimalBlockPreheadActualCentralExtensionSquareData P.phiPacket

Route17 SquareData projected from the same Route18 square/polar packet.

Equations

• P.squarePacket = { square := P.squarePolar.square }

def Q2Presentation.Induction.MinimalBlockPushoutRoute18ActualDeterminantData.diagonalPacket {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute18ActualDeterminantData D) : MinimalBlockPreheadActualCentralExtensionDiagonalData P.squarePacket

Route17 diagonal identity from the coherent square/polar packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute18ActualDeterminantData.polarPacket {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute18ActualDeterminantData D) : MinimalBlockPreheadActualCentralExtensionPolarData P.squarePacket

Route17 polar identity from the coherent square/polar packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute18ActualDeterminantData.naturalityPacket {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute18ActualDeterminantData D) : MinimalBlockPreheadActualCentralExtensionNaturalityData P.phiPacket

Route17 naturality from the same-family actual determinant packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute18ActualDeterminantData.annihilationPacket {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute18ActualDeterminantData D) : MinimalBlockPreheadActualCentralExtensionAnnihilationData P.squarePacket

Route17 annihilation from the same-family actual determinant packet, with the semantic extraspecial square rewritten to the concrete Route18 square.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute18ActualDeterminantData.radicalContainmentPacket {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute18ActualDeterminantData D) : MinimalBlockPreheadActualCentralExtensionRadicalContainmentData P.squarePacket

Route17 radical containment from the same-family actual determinant packet, again rewriting the semantic extraspecial square to the concrete Route18 square.

Equations

• ⋯ = ⋯

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

Reassemble the broad actual central-extension pushout packet from the Route18 coherent packet.

Equations

• P.actualPushout = Q2Presentation.Induction.MinimalBlockPreheadActualCentralExtensionPushoutData.ofSplitPackets P.phiPacket P.squarePacket ⋯ ⋯ ⋯ ⋯ ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute18ActualDeterminantData.actualDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute18ActualDeterminantData D) : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData P.actualPushout.toSemanticData

The actual determinant packet projected from the reassembled actual pushout.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute18ActualDeterminantData.extraspecialSimpleHeadDeterminant {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute18ActualDeterminantData D) : MinimalBlockPreheadExtraspecialSimpleHeadDeterminantData (MinimalBlockPreheadExtraspecialFamilyData.ofCentralPushoutSelfDuality P.actualPushout.toSemanticData.toSelfDuality)

The extraspecial simple-head determinant packet consumed by the lower route.

Equations

• ⋯ = ⋯

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

Convert Route18 data to the lower pushout packet consumed by integrated routes.

Equations

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

Route18 constructors and route hooks

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

Assemble Route18 data from two coherent manuscript-shaped residuals.

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

Same-family Route17 packet bundle supplied by Route18.

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

Broad actual central-extension pushout data from Route18, avoiding the seven Route17 split residual axioms.

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

Route18 replacement for the semantic central-pushout residual.

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

Route18 actual determinant packet for the route-relevant semantic family.

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

Preferred supervisor hook: Route18 lower pushout packet compatible with the Route17 consumption site.

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

Determinant packet projection from the Route18 lower pushout theorem.

Acceptance checks / residual report