Actual scalar central-pushout proof boundary

This sidecar narrows the current Section 7 semantic residual minimalBlock_preheadCentralPushoutSemanticData.

The manuscript construction on pages 41--42 starts with scalar central pushouts K_lambda = K / ker lambda for nonzero invariant characters lambda : R^vee. The current semantic packet only records the resulting self-duality family phi_lambda. The residual introduced here is narrower: it records the scalar quotient condition for every nonzero lambda, the square map of the same scalar pushout family, and the fact that this square is the extraspecial form attached to the same phi_lambda.

No routed file imports this sidecar yet. A coordinator can route through minimalBlock_preheadCentralPushoutSemanticData_proven to replace the broad semantic residual by minimalBlock_preheadActualScalarCentralPushoutData.

Actual scalar pushout family

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

Actual scalar central-pushout data over a pre-head Section 7 tower.

Manuscript anchor: for each 0 != lambda in the determinant character space, the scalar quotient lambda : R -> F_2 forms K_lambda = K / ker lambda. Its square map on M = K/R is the extraspecial quadratic form determined by the same self-duality pairing phi_lambda.

The current API has no quotient group object for K_lambda; this packet is the closest available Lean boundary to the manuscript construction without inventing dummy pushouts.

• phi : Module.Dual (ZMod 2) D.R → D.M →ₗ[ZMod 2] Module.Dual (ZMod 2) D.M

  The self-duality pairing induced by the scalar central pushouts.

• square : Module.Dual (ZMod 2) D.R → Quadratic.QuadF2 D.M

  The square map of the same scalar central pushout family.

• scalar_quotient_surjective (lam : Module.Dual (ZMod 2) D.R) : lam ≠ 0 → Function.Surjective ⇑lam

  Nonzero characters really are scalar quotients R -> F_2, excluding a vacuous one-point pushout interpretation.

• square_is_extraspecial (lam : Module.Dual (ZMod 2) D.R) : self.square lam = Quadratic.Extraspecial.extraspecialForm (self.phi lam)

  The square map is the extraspecial square attached to the same phi_lambda.

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

Forget to the split quadratic-family packet.

Equations

• P.toQuadraticFamily = { phi := P.phi, square := P.square }

def Q2Presentation.Induction.MinimalBlockPreheadActualScalarCentralPushoutData.squareDiagonalData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadActualScalarCentralPushoutData D) : MinimalBlockPreheadCentralPushoutSquareDiagonalData P.toQuadraticFamily

The square diagonal is definitional after identifying the actual square with the extraspecial square of phi_lambda.

Equations

• ⋯ = ⋯

def Q2Presentation.Induction.MinimalBlockPreheadActualScalarCentralPushoutData.polarSymmData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadActualScalarCentralPushoutData D) : MinimalBlockPreheadCentralPushoutPolarSymmData P.toQuadraticFamily

The polar form is the symmetrized phi_lambda pairing for the same actual scalar pushout square.

Equations

• ⋯ = ⋯

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

Package the actual scalar pushout family as the existing standard square/polar data.

Equations

• P.toStandardData = { quadraticFamily := P.toQuadraticFamily, squareDiagonal := ⋯, polarSymm := ⋯ }

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

Forget the actual square and scalar-quotient witnesses to the current semantic central-pushout packet.

Equations

• P.toSemanticData = { phi := P.phi }

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

Forget further to the old self-duality-only packet.

Equations

• P.toSelfDualityData = { phi := P.phi }

Residual and projections

axiom Q2Presentation.Induction.minimalBlock_preheadActualScalarCentralPushoutData {p : FramedPair} {chief : NonScalarChiefFactor p} (D : MinimalBlockPreheadTowerData p chief) : Nonempty (MinimalBlockPreheadActualScalarCentralPushoutData D)

Narrow Section 7 residual: actual scalar central-pushout construction.

This is the intended replacement for the broad semantic-family axiom minimalBlock_preheadCentralPushoutSemanticData.

theorem Q2Presentation.Induction.minimalBlock_preheadCentralPushoutStandardData_from_actualScalarCentralPushout {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadActualScalarCentralPushoutData D) : Nonempty (MinimalBlockPreheadCentralPushoutStandardData D)

Reconstruct the standard square/polar packet from the actual scalar pushout construction.

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

Project an actual scalar central-pushout construction to the current semantic central-pushout packet.

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

Closure of the current semantic central-pushout packet from the narrower actual scalar-pushout residual.

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

Self-duality closure from the actual scalar pushout residual, bypassing the broad semantic-family axiom.

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

Route-level lower packet with the central self-duality field supplied from the actual scalar pushout residual.

The determinant side still uses the existing extraspecial packet projections; the point of this theorem is only to remove minimalBlock_preheadCentralPushoutSemanticData from the central-pushout part of the route.