Actual semantic central-pushout closers

This sidecar is the narrow bridge below minimalBlock_preheadCentralPushoutExtraspecialActualData.

The current route-facing packet combines two different manuscript steps:

• the actual scalar central-pushout family K_lambda = K / ker lambda, recorded in Lean as one coherent square/polar family with the same phi_lambda;
• the simple-head determinant theorem for that actual family, namely naturality, q_lambda|T = 0, b_lambda(T,M) = 0, and polar-radical containment.

This file keeps those steps separate. It does not introduce a new axiom: the assembler below uses the existing concrete square/polar central-pushout packet and the existing actual simple-head determinant packet for the semantic family projected from that same square/polar data.

Same-family actual semantic packet

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

Actual semantic data for the Section 7 extraspecial pushout, split into the actual scalar central-pushout construction and the determinant theorem for the same projected semantic family.

• squarePolar : MinimalBlockPreheadCentralPushoutSquarePolarData D

  The actual scalar central-pushout square/polar family.

• determinant : MinimalBlockPreheadCentralPushoutSimpleHeadDeterminantActualData (MinimalBlockPreheadActualScalarCentralPushoutData.ofSquarePolar self.squarePolar).toSemanticData

  The prop:simpleheaddet theorem for the semantic family projected from squarePolar.

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

The actual scalar central-pushout packet induced by the square/polar data.

Equations

• P.actualScalar = Q2Presentation.Induction.MinimalBlockPreheadActualScalarCentralPushoutData.ofSquarePolar P.squarePolar

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

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

Equations

• P.semanticData = P.actualScalar.toSemanticData

Constructor from lower Section 7 packets

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

Assemble the actual semantic split from the concrete square/polar pushout family and the actual simple-head determinant packet for the same projected semantic family.

Its nonstandard closure is strictly below minimalBlock_preheadCentralPushoutExtraspecialActualData: it exposes the actual central-pushout square/polar construction and the actual determinant theorem as separate obligations.