Actual scalar central-pushout proof split

This sidecar strictly narrows the current Section 7 residual minimalBlock_preheadActualScalarCentralPushoutData.

Manuscript anchor: Section 7, pages 41--42. For every nonzero invariant character lambda : R -> F_2, the scalar pushout K_lambda = K / ker lambda is a central double cover of M = K/R; its square map is the extraspecial square attached to the same phi_lambda.

The current Lean API already has a standard same-family square/polar packet MinimalBlockPreheadCentralPushoutStandardData. The only remaining pushout-specific content needed to recover the actual-scalar packet is the comparison that this standard square is the extraspecial square. Surjectivity of every nonzero lambda : R -> F_2 is closed below as an elementary ZMod 2 fact.

No routed file imports this sidecar yet.

Nonzero scalar characters over F_2 are surjective

theorem Q2Presentation.Induction.minimalBlock_actualScalar_dual_zmod2_surjective_of_ne_zero {R : Type} [AddCommGroup R] [Module (ZMod 2) R] (lam : Module.Dual (ZMod 2) R) (hlam : lam ≠ 0) : Function.Surjective ⇑lam

A nonzero F_2-linear functional onto ZMod 2 is surjective.

Smaller actual-scalar comparison residual

structure Q2Presentation.Induction.MinimalBlockPreheadActualScalarCentralPushoutComparisonData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutStandardData D) : Prop

The remaining actual scalar-pushout comparison after the standard square and polar packets have already supplied the same-family phi_lambda and square map.

This is strictly smaller than MinimalBlockPreheadActualScalarCentralPushoutData: it records only that the standard square is the extraspecial square. The square map itself comes from P.quadraticFamily, and surjectivity of nonzero scalar characters is proved above.

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

axiom Q2Presentation.Induction.minimalBlock_preheadActualScalarCentralPushoutComparisonData {p : FramedPair} {chief : NonScalarChiefFactor p} {D : MinimalBlockPreheadTowerData p chief} (P : MinimalBlockPreheadCentralPushoutStandardData D) : Nonempty (MinimalBlockPreheadActualScalarCentralPushoutComparisonData P)

Narrow residual: compare the standard Section 7 square/polar packet with the actual extraspecial scalar pushout square.

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

Assemble the current actual-scalar packet from the standard square/polar packet plus the smaller extraspecial-square comparison residual.

Equations

• One or more equations did not get rendered due to their size.

Replacement theorem for the current residual

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

Closure of the current actual scalar central-pushout packet from the smaller comparison residual plus the already-existing standard square/polar packet.

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

Semantic central-pushout closure through the new actual-scalar proof split, avoiding the old minimalBlock_preheadActualScalarCentralPushoutData axiom.

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

Route-level lower packet through the new actual-scalar proof split.