Stage G — Quadratic determinant obstructions and the Gauss-sign comparison (manuscript §6)

This file is the comparison core of §6 ("Quadratic determinant obstructions", reference/q2_manuscript.tex, l.2025–3597). The linear interface of §5 (Lifting/) does not determine the scalar central pushouts attached to a self-dual simple module V, because their lifting obstruction is quadratic. §6 constructs a normalized equivariant base class κ_q^0, computes the resulting quadratic form on the candidate and local sides, and proves their Gauss sums agree (prop:localzero, l.3347 — the conclusion this file targets).

The determinant obstruction (l.2034–2049)

For a C-equivariant central extension 1 → R → M̃ → M → 1 of class ≤ 2 with R, M elementary abelian, and λ ∈ (R^∨)^C, pushing out along λ : R → F₂ gives a central double cover of M whose square map q_λ(m) = λ(m̃²) ∈ F₂ is quadratic, with polar form the commutator pairing. On the nontrivial simple head V this is a nonzero nonsingular quadratic form (prop:simpleheaddet).

This is exactly the class-two Heisenberg ledger of Lifting/HeisenbergCup.lean: the square diagonal (u²).z = λ(v) (HeisQ.sq_z) is the square map, and the commutator central coordinate (⁅u,w⁆).z = bcl u w (HeisQ.commutator_z) is the polar form. We package this as QuadF2 (a quadratic form over F₂ with explicit polar form) and exhibit the extraspecial pushout extraspecialForm.

The candidate-side base form (l.2458–2536, prop:wordquadratic, eq:QA)

The complete base second-order word expansion of the wild relator gives

  Q_A^0(c) = q(c) + b_q((P+1)c, U^{-1}c),     U = S^{ω₂}            (eq:QA, l.2470)

with ramified cases (eq:QAcases): Q_A^0 = q when T=1 (unramified), and Q_A^0(c) = q(c) + b_q(c, U^{-1}c) when V^T = 0 (ramified). Its polar form (eq:polaroperator) is

  b_A(c,c') = b_q(c, (1 + U + U^{-1}) c').                          (eq:polaroperator)

The operator 1 + U + U^{-1} is exactly Lifting.pairingOp, already proven a unit in HeisenbergCup.lean (pairingOp_powOmega2_isUnit, because U = S^{ω₂} has 2-power order ⟹ unipotent). So the candidate base form (candidateForm) is a genuinely nonsingular QuadF2, proven here by reusing that infrastructure.

The Gauss sums (l.2731 prop:candidatezero, l.3349 prop:localzero)

A nonsingular quadratic form of dimension d over F₂ has # Q⁻¹(0) = 2^{d-1} + (-1)^{Arf} 2^{d/2-1}. Both sides compute the same count (baseZeroCount):

  # Q⁻¹(0) = 2^{d-1} - 2^{d/2-1}   (V unramified, minus type),
  # Q⁻¹(0) = 2^{d-1} + 2^{d/2-1}   (V ramified,  plus  type).

• Candidate (prop:candidatezero): unramified Arf = 1 by the Hermitian-line classification (lem:unitaryline); ramified Arf = Arf(q) + rank(1+U) = s+s = 0 by Wall doubling (lem:wall) + the ramified Hermitian/fixed-space computation (lem:ramifiedhermitian).
• Local (prop:localzero): unramified Arf = 1 by the same Hermitian line (lem:unitaryline, the norm-one group acts by isometries); ramified the deep half X_+ = Hom_{H_V}(V^∨, U_{e+1}) is totally singular of dimension d/2 (lem:shapirodet), so the form is hyperbolic (Arf = 0), via the dyadic square-class filtration and Hilbert-symbol orthogonality U_i^⊥ = U_{2e-i+1}, -1 ∈ U_e (eq:unitorth) and the deep-unit Evens-norm vanishing (lem:evensvanish).

Decomposition: proven vs. isolated

• PROVEN (sorry-free, structural): QuadF2 + polar/nonsingularity calculus; the extraspecial Heisenberg obstruction (extraspecialForm, polar = bcl); the candidate base form candidateForm, its polar = pairingOp = 1+U+U^{-1} and its nonsingularity (reusing pairingOp_isUnit); the abstract Gauss-sign calculus and the comparison candidate_gauss_eq_local_gauss.
• AXIOM-FREE (2026-07-08 repair): the former zero-count axioms (candidate_base_zeroCount, q2_local_base_zeroCount) were refutable at V = 0 and are DELETED; the counts are the finite-field Dickson theorem, proven with the honest [Nontrivial V] guard in DicksonCount.lean (*_proven), where the pinning + §6 comparison now live. The honest local residual of prop:localzero is the SIGN-pinning gaussType Q⁰_loc = ram(V) (future keep, audit/BLOCKR_P6_DESIGN.md).

The §6 follow-up not formalized here (flagged for the designer): the affine correction terms Γ_γ, inf δ (subsec:affinecorrections: transgression lem:transgression, shear lem:shear, Θ_q^0) and the index-two Evens-norm machinery (lem:twopointevans, lem:orbitshapiro) underlying the local realization — these enter only after Fourier expansion (cor:sourceinterface), not in the base Gauss-sum comparison proved here.

Part 0 — Quadratic forms over F₂ with explicit polar form

A QuadF2 V is a function form : V → F₂ together with its polar (commutator) form polar : V → V → F₂ (a genuine bilinear map) satisfying the quadratic law form (x+y) = form x + form y + polar x y. Over F₂ the polar form is automatically alternating (polar_self) and symmetric (polar_comm), both derived below; this is the manuscript's "polar form given by the commutator pairing" (l.2045).

structure Q2Presentation.Quadratic.QuadF2 (V : Type u_2) [AddCommGroup V] [Module (ZMod 2) V] : Type u_2

A quadratic form over F₂ with its bilinear polar (commutator) form.

• form : V → ZMod 2

  the quadratic map q : V → F₂

• polar : V →ₗ[ZMod 2] V →ₗ[ZMod 2] ZMod 2

  the bilinear polar form b_q, i.e. the commutator pairing

• form_zero : self.form 0 = 0

  normalization q(0) = 0

• form_add (x y : V) : self.form (x + y) = self.form x + self.form y + (self.polar x) y

  the quadratic law q(x+y) = q(x) + q(y) + b_q(x,y)

theorem Q2Presentation.Quadratic.QuadF2.polar_comm {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (q : QuadF2 V) (x y : V) : (q.polar x) y = (q.polar y) x

The polar form is symmetric (derived from the quadratic law).

@[simp]

theorem Q2Presentation.Quadratic.QuadF2.polar_self {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (q : QuadF2 V) (x : V) : (q.polar x) x = 0

The polar form is alternating: b_q(x,x) = 0 (char 2).

@[simp]

theorem Q2Presentation.Quadratic.QuadF2.form_zero' {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (q : QuadF2 V) : q.form 0 = 0

The square value at 0 (restating form_zero for simp).

def Q2Presentation.Quadratic.QuadF2.Nonsingular {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (q : QuadF2 V) : Prop

Nonsingularity (the polar form is nondegenerate / perfect): the only vector pairing to 0 with everything is 0. For a nonzero invariant form on a simple self-dual V this is automatic (lem:zeropolar, l.3452).

Equations

• q.Nonsingular = ∀ (x : V), (∀ (y : V), (q.polar x) y = 0) → x = 0

Part 1 — The extraspecial / Heisenberg quadratic obstruction κ_q^0

The scalar central (extraspecial) pushout of a self-dual simple module produces a quadratic form whose polar form is the commutator pairing (l.2034–2049). In the class-two Heisenberg coefficient group HeisQ V of Lifting/HeisenbergCup.lean, for a symmetric self-duality φ : V → V^∨ the square map is c ↦ ((⟨c,φc,0⟩)²).z = (φ c) c (HeisQ.sq_z) and the polar form is the commutator central coordinate bcl (HeisQ.commutator_z). This is proven structurally from HeisenbergCup.

def Q2Presentation.Quadratic.Extraspecial.polarφ {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (φ : V →ₗ[ZMod 2] Module.Dual (ZMod 2) V) : V →ₗ[ZMod 2] V →ₗ[ZMod 2] ZMod 2

The symmetrized polar form b_φ(c,c') = φ(c)(c') + φ(c')(c) of the extraspecial pushout — the bilinear commutator pairing bcl of HeisQ V.

Equations

• Q2Presentation.Quadratic.Extraspecial.polarφ φ = LinearMap.mk₂ (ZMod 2) (fun (c c' : V) => (φ c) c' + (φ c') c) ⋯ ⋯ ⋯ ⋯

@[simp]

theorem Q2Presentation.Quadratic.Extraspecial.polarφ_apply {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (φ : V →ₗ[ZMod 2] Module.Dual (ZMod 2) V) (c c' : V) : ((polarφ φ) c) c' = (φ c) c' + (φ c') c

def Q2Presentation.Quadratic.Extraspecial.extraspecialForm {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (φ : V →ₗ[ZMod 2] Module.Dual (ZMod 2) V) : QuadF2 V

The extraspecial pushout quadratic obstruction κ_q^0 as a QuadF2: form c = φ(c)(c), polar form bcl. This is the fibre square map of the central double cover (l.2043), proven quadratic with the commutator polar form.

Equations

• Q2Presentation.Quadratic.Extraspecial.extraspecialForm φ = { form := fun (c : V) => (φ c) c, polar := Q2Presentation.Quadratic.Extraspecial.polarφ φ, form_zero := ⋯, form_add := ⋯ }

theorem Q2Presentation.Quadratic.Extraspecial.extraspecialForm_eq_heisSquare {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (φ : V →ₗ[ZMod 2] Module.Dual (ZMod 2) V) (c : V) : (extraspecialForm φ).form c = ({ v := c, dl := φ c, z := 0 } ^ 2).z

The extraspecial square map is the Heisenberg square diagonal (u²).z = λ(v) of lem:h0shadow (HeisQ.sq_z): form c = ((⟨c, φc, 0⟩)²).z.

theorem Q2Presentation.Quadratic.Extraspecial.extraspecialForm_polar_eq_bcl {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (φ : V →ₗ[ZMod 2] Module.Dual (ZMod 2) V) (c c' : V) : ((extraspecialForm φ).polar c) c' = { v := c, dl := φ c, z := 0 }.bcl { v := c', dl := φ c', z := 0 }

The extraspecial polar form is the commutator pairing bcl (HeisQ.commutator_z): b_φ(c,c') = bcl ⟨c,φc,0⟩ ⟨c',φc',0⟩. This is the manuscript's "polar form given by the commutator pairing" (l.2045).

Part 2 — The candidate-side base form Q_A^0 (prop:wordquadratic, eq:QA)

The complete base second-order word expansion (eq:QA) is Q_A^0(c) = q(c) + b_q((P+1)c, U^{-1}c); in the ramified normal form (eq:QAcases, V^T = 0, where P = 0 on the relevant piece) this is q(c) + b_q(c, U^{-1}c). We formalize this ramified form and prove its polar form is the mixed-Hessian pairing operator b_q(·, (1 + U + U^{-1})·) (eq:polaroperator) — i.e. Lifting.pairingOp — hence its nonsingularity by reusing pairingOp_isUnit.

def Q2Presentation.Quadratic.Candidate.pairOp {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (U : (Module.End (ZMod 2) V)ˣ) : Module.End (ZMod 2) V

The mixed-Hessian pairing operator M = 1 + U + U⁻¹ on V (pairingOp, eq:pairingoperator).

Equations

• Q2Presentation.Quadratic.Candidate.pairOp U = 1 + ↑U + ↑U⁻¹

@[simp]

theorem Q2Presentation.Quadratic.Candidate.pairOp_apply {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (U : (Module.End (ZMod 2) V)ˣ) (x : V) : (pairOp U) x = x + ↑U x + ↑U⁻¹ x

def Q2Presentation.Quadratic.Candidate.candidateForm {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (q : QuadF2 V) (U : (Module.End (ZMod 2) V)ˣ) (hisom : ∀ (x y : V), (q.polar (↑U x)) (↑U y) = (q.polar x) y) : QuadF2 V

The candidate base determinant form Q_A^0 in the ramified normal form (eq:QAcases): form c = q(c) + b_q(c, U^{-1}c), with polar form the mixed-Hessian operator b_q(c, (1 + U + U^{-1}) c') (eq:polaroperator).

Equations

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

@[simp]

theorem Q2Presentation.Quadratic.Candidate.candidateForm_form {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (q : QuadF2 V) (U : (Module.End (ZMod 2) V)ˣ) (hisom : ∀ (x y : V), (q.polar (↑U x)) (↑U y) = (q.polar x) y) (c : V) : (candidateForm q U hisom).form c = q.form c + (q.polar c) (↑U⁻¹ c)

@[simp]

theorem Q2Presentation.Quadratic.Candidate.candidateForm_polar {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (q : QuadF2 V) (U : (Module.End (ZMod 2) V)ˣ) (hisom : ∀ (x y : V), (q.polar (↑U x)) (↑U y) = (q.polar x) y) (c c' : V) : ((candidateForm q U hisom).polar c) c' = (q.polar c) ((pairOp U) c')

theorem Q2Presentation.Quadratic.Candidate.candidateForm_polar_eq {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (q : QuadF2 V) (U : (Module.End (ZMod 2) V)ˣ) (hisom : ∀ (x y : V), (q.polar (↑U x)) (↑U y) = (q.polar x) y) (c c' : V) : ((candidateForm q U hisom).polar c) c' = (q.polar c) ((1 + ↑U + ↑U⁻¹) c')

eq:polaroperator (prop:wordquadratic): the candidate base polar form is b_A(c,c') = b_q(c, (1 + U + U^{-1}) c'), the mixed-Hessian pairing operator.

theorem Q2Presentation.Quadratic.Candidate.candidateForm_nonsingular {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (q : QuadF2 V) (U : (Module.End (ZMod 2) V)ˣ) (hisom : ∀ (x y : V), (q.polar (↑U x)) (↑U y) = (q.polar x) y) (hq : q.Nonsingular) (hM : IsUnit (pairOp U)) : (candidateForm q U hisom).Nonsingular

The candidate base form is nonsingular (prop:wordquadratic: "the operator is invertible by the same polynomial argument used in prop:defduality"). Proven by reusing pairingOp invertibility: if b_q(c, M c') = 0 for all c' and M = 1+U+U⁻¹ is a unit (surjective), then b_q(c, ·) = 0, so c = 0 by nonsingularity of q.

theorem Q2Presentation.Quadratic.Candidate.candidateForm_one {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (q : QuadF2 V) (hisom1 : ∀ (x y : V), (q.polar (↑1 x)) (↑1 y) = (q.polar x) y) (c : V) : (candidateForm q 1 hisom1).form c = q.form c

Unramified normal form (eq:QAcases, T = 1): when U = 1 the candidate base form is q itself (Q_A^0 = q), since b_q(c, c) = 0.

theorem Q2Presentation.Quadratic.Candidate.instFiniteEnd' {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] [Finite V] : Finite (Module.End (ZMod 2) V)

theorem Q2Presentation.Quadratic.Candidate.instFiniteEndUnits' {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] [Finite V] : Finite (Module.End (ZMod 2) V)ˣ

theorem Q2Presentation.Quadratic.Candidate.pairOp_isUnit_powOmega2 {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] [Finite V] (S : (Module.End (ZMod 2) V)ˣ) : IsUnit (pairOp (powOmega2 S))

The candidate polar operator is a unit when U = S^{ω₂} (U of 2-power order): this is exactly Lifting.pairingOp_powOmega2_isUnit. So the ramified candidate base form is genuinely nonsingular without any further hypothesis.

Part 3 — The Gauss sign of a finite nonsingular F₂ quadratic space

Over F₂ a nonsingular quadratic form of dimension d has # Q⁻¹(0) = 2^{d-1} + ε · 2^{d/2-1} with the Gauss sign ε = (-1)^{Arf} ∈ {±1} (the standard quadric point count). baseGaussSign is +1 (plus type / ramified) or -1 (minus type / unramified); baseZeroCount is the resulting count.

def Q2Presentation.Quadratic.numZeros {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (q : QuadF2 V) : ℕ

The number of zeros # Q⁻¹(0) of a quadratic form.

Equations

• Q2Presentation.Quadratic.numZeros q = Nat.card { v : V // q.form v = 0 }

def Q2Presentation.Quadratic.baseGaussSign (ramified : Bool) : ℤ

The base Gauss sign (prop:candidatezero/prop:localzero): +1 (plus type) in the ramified case, -1 (minus type) in the unramified case.

Equations

• Q2Presentation.Quadratic.baseGaussSign ramified = if ramified = true then 1 else -1

def Q2Presentation.Quadratic.baseZeroCount (ramified : Bool) (d : ℕ) : ℤ

The base determinant zero count 2^{d-1} + ε·2^{d/2-1} (eq:candidatezeros / eq:localzeros).

Equations

• Q2Presentation.Quadratic.baseZeroCount ramified d = 2 ^ (d - 1) + Q2Presentation.Quadratic.baseGaussSign ramified * 2 ^ (d / 2 - 1)

@[simp]

theorem Q2Presentation.Quadratic.baseZeroCount_true (d : ℕ) : baseZeroCount true d = 2 ^ (d - 1) + 2 ^ (d / 2 - 1)

@[simp]

theorem Q2Presentation.Quadratic.baseZeroCount_false (d : ℕ) : baseZeroCount false d = 2 ^ (d - 1) - 2 ^ (d / 2 - 1)

theorem Q2Presentation.Quadratic.baseZeroCount_ne (d : ℕ) : baseZeroCount false d ≠ baseZeroCount true d

The plus-type and minus-type counts are distinct (the 2^{d/2-1} gap is nonzero) — this is what lets the zero count determine the Gauss sign.

def Q2Presentation.Quadratic.gaussSign {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (q : QuadF2 V) : ℤ

The Gauss sign of a quadratic form, read off from its zero count: +1 iff the count is plus-type, else -1. For a nonsingular form this is the genuine (-1)^{Arf} (the count is always one of the two values).

Equations

• Q2Presentation.Quadratic.gaussSign q = if ↑(Q2Presentation.Quadratic.numZeros q) = 2 ^ (Module.finrank (ZMod 2) V - 1) + 2 ^ (Module.finrank (ZMod 2) V / 2 - 1) then 1 else -1

def Q2Presentation.Quadratic.gaussType {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (q : QuadF2 V) : Bool

The Gauss type of a quadratic form: the Bool-valued ramification flag read off from its zero count — true (plus type / ramified) iff the count is the plus value baseZeroCount true d, else false (minus type / unramified). This is the form's own Arf type made into the unique ram for which # Q⁻¹(0) = baseZeroCount ram d (uniqueness is baseZeroCount_ne; that this ram is realized is the Dickson zero count, candidate_numZeros_eq_gaussType / q2_local_numZeros_eq_gaussType in DicksonCount.lean). Tying the flag to the form this way is exactly the de-bugging of the old free ram argument.

Equations

• Q2Presentation.Quadratic.gaussType q = if ↑(Q2Presentation.Quadratic.numZeros q) = Q2Presentation.Quadratic.baseZeroCount true (Module.finrank (ZMod 2) V) then true else false

theorem Q2Presentation.Quadratic.gaussSign_eq_baseGaussSign_gaussType {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (q : QuadF2 V) : gaussSign q = baseGaussSign (gaussType q)

gaussSign is baseGaussSign of the form's gaussType: the integer Gauss sign and the Bool Gauss type are the same datum (+1 ↔ true, -1 ↔ false).

theorem Q2Presentation.Quadratic.gaussSign_eq_of_zeroCount {V : Type u_1} [AddCommGroup V] [Module (ZMod 2) V] (q : QuadF2 V) (ram : Bool) (h : ↑(numZeros q) = baseZeroCount ram (Module.finrank (ZMod 2) V)) : gaussSign q = baseGaussSign ram

If the zero count matches baseZeroCount ram d, the Gauss sign is baseGaussSign ram. (Uses that the plus/minus counts are distinct.)

Parts 4–6 — RE-HOMED to Quadratic/DicksonCount.lean

The former Part-4/5 zero-count AXIOMS (candidate_base_zeroCount, q2_local_base_zeroCount) were REFUTABLE at V = 0 (the ∃ ram statement fails for the singleton module: the count is 1, the two base values are not). The counts are finite-field Dickson algebra — NOT an irreducible local input — and are proven (with the honest [Nontrivial V] guard) in DicksonCount.lean (candidate_base_zeroCount_proven / q2_local_base_zeroCount_proven), where the Gauss-type pinning and the §6 comparison now live as theorems. The honest remaining LOCAL content of prop:localzero is the sign-pinning gaussType Q⁰_loc = ram(V) (future q2_local_base_gaussType keep, see audit/BLOCKR_P6_DESIGN.md).