Route27 minimal-block pushout/determinant refinement

Route26 constructs the lower pushout provider from an actual scalar central pushout family plus the same-family actual determinant packet. Its scalar side still bottoms out in the three split square/polar leaves

• minimalBlock_preheadCentralPushoutQuadraticFamilyData;
• minimalBlock_preheadCentralPushoutSquareDiagonalData;
• minimalBlock_preheadCentralPushoutPolarSymmData.

This sidecar keeps route26's output shape but chooses the semantic central-pushout family as the scalar square source. The square is the extraspecial form of the same phi_lambda by definition, so the three split square/polar leaves are projected theorem-level from the single semantic family.

The determinant side remains the route26 same-family actual determinant packet minimalBlock_preheadCentralPushoutSimpleHeadDeterminantActualData for that same semantic family.

Route27 semantic square plus actual determinant packet

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

Route27 actual determinant data.

The scalar square/polar side is the semantic central-pushout family, whose square is definitionally Extraspecial.extraspecialForm. The determinant side is the actual simple-head determinant packet for the same semantic family.

• semantic : MinimalBlockPreheadCentralPushoutSemanticData D
• actualDeterminant : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData self.semantic

def Q2Presentation.Induction.MinimalBlockPushoutRoute27SemanticActualDeterminantData.actualScalar {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute27SemanticActualDeterminantData D) : MinimalBlockPreheadActualScalarCentralPushoutData D

The actual scalar packet induced by the semantic central-pushout family.

This closes the three route26 split square/polar leaves for this provider: semantic.toQuadraticFamily, semantic.squareDiagonalData, and semantic.polarSymmData provide the same-family square and polar identities.

Equations

• P.actualScalar = { phi := P.semantic.phi, square := P.semantic.toQuadraticFamily.square, scalar_quotient_surjective := ⋯, square_is_extraspecial := ⋯ }

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

Project semantic naturality from the same-family actual determinant packet.

Equations

• ⋯ = ⋯

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

Project diagonal vanishing on T from the same-family actual determinant annihilation packet.

Equations

• ⋯ = ⋯

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

Project polar vanishing on T x M from the same-family actual determinant annihilation packet.

Equations

• ⋯ = ⋯

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

Project polar-radical containment from the same-family actual determinant packet.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute27SemanticActualDeterminantData.determinantSplit {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute27SemanticActualDeterminantData D) : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualSplitData P.semantic

Route25's split determinant packet, projected from route27's actual determinant packet without using the four route25 semantic determinant axioms.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPushoutRoute27SemanticActualDeterminantData.toRoute25Data {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPushoutRoute27SemanticActualDeterminantData D) : MinimalBlockPushoutRoute25ActualCentralExtensionData D

Route27 data repackaged in route25's provider structure.

Equations

• P.toRoute25Data = { actualScalar := P.actualScalar, determinantPieces := ⋯ }

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

Broad actual central-extension pushout data recovered theorem-level through route25's projection chain.

Equations

• P.toActualPushout = P.toRoute25Data.toActualPushout

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

Route27 data projected to the lower pushout route in route26's output shape.

Equations

• P.toPushoutRouteLower = P.toRoute25Data.toPushoutRouteLower

Route-compatible hooks

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

Construct route27 semantic/actual determinant data.

This replaces route26's three split square/polar residuals by the coherent semantic central-pushout family. The determinant residual remains the same route26 actual simple-head determinant packet, indexed by that semantic family.

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

Route25-compatible packet, constructed through route27's semantic actual determinant packet.

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

Broad actual central-extension packet recovered through route27.

This theorem is compatibility glue only; the proof does not call the broad actual central-extension pushout axiom.

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

Supervisor hook: route26-shaped lower pushout provider from route27 semantic actual determinant data.

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

Determinant packet projection through the route27 lower pushout theorem.

Acceptance checks / exact residual report