Gauss sums, zero counts, and Wall doubling

The elementary Gauss-sum engine and the structural and counting parts of Wall doubling.

See GQ2.GaussCount for the paper-facing overview, source citations, and deviations.

The sign character 𝔽₂ → ℤ

def GQ2.QuadraticFp2.sign (a : ZMod 2) : ℤ

The nontrivial character 𝔽₂ → ℤˣ ⊂ ℤ, 0 ↦ 1, 1 ↦ −1.

Equations

• GQ2.QuadraticFp2.sign a = if a = 0 then 1 else -1

@[simp]

theorem GQ2.QuadraticFp2.sign_zero : sign 0 = 1

theorem GQ2.QuadraticFp2.sign_add (a b : ZMod 2) : sign (a + b) = sign a * sign b

The Gauss sum

noncomputable def GQ2.QuadraticFp2.gaussSum {V : Type u_1} (q : V → ZMod 2) [Fintype V] : ℤ

The integer Gauss sum g(q) = ∑_v (−1)^{q(v)} = #q⁻¹(0) − #q⁻¹(1).

Equations

• GQ2.QuadraticFp2.gaussSum q = ∑ v : V, GQ2.QuadraticFp2.sign (q v)

def GQ2.QuadraticFp2.polarHom {V : Type u_1} [AddCommGroup V] (q : V → ZMod 2) (hq : IsQuadraticFp2 q) (u : V) : V →+ ZMod 2

B(·, u) as an additive character V →+ 𝔽₂ (additive by polar_add_left).

Equations

• GQ2.QuadraticFp2.polarHom q hq u = AddMonoidHom.mk' (fun (v : V) => GQ2.QuadraticFp2.polar q v u) ⋯

@[simp]

theorem GQ2.QuadraticFp2.polarHom_apply {V : Type u_1} [AddCommGroup V] (q : V → ZMod 2) (hq : IsQuadraticFp2 q) (u v : V) : (polarHom q hq u) v = polar q v u

theorem GQ2.QuadraticFp2.charSum_eq_zero {V : Type u_1} [AddCommGroup V] [Fintype V] (φ : V →+ ZMod 2) (hφ : ∃ (u₀ : V), φ u₀ = 1) : ∑ v : V, sign (φ v) = 0

Character-sum vanishing: for a nonzero additive character φ : V →+ 𝔽₂ on a finite group, ∑_v (−1)^{φ(v)} = 0. (Shift by any u₀ with φ(u₀) = 1 negates the sum.)

theorem GQ2.QuadraticFp2.sum_sign_shift_eq_zero {V : Type u_1} [AddCommGroup V] [Fintype V] (f : V → ZMod 2) (r₀ : V) (h : ∀ (x : V), f (x + r₀) = f x + 1) : ∑ x : V, sign (f x) = 0

Twisted-sum vanishing (Wall step, level 0): if a function f : V → 𝔽₂ shifts by 1 under some translation r₀ (f(x + r₀) = f(x) + 1), then ∑_x (−1)^{f(x)} = 0. This is the "character is nonzero on the radical ⇒ the Gauss sum vanishes" building block for Lemma 6.6's sign relation.

theorem GQ2.QuadraticFp2.gaussSum_sq {V : Type u_1} [AddCommGroup V] [Fintype V] (q : V → ZMod 2) (hq : IsQuadraticFp2 q) (hns : Nonsingular q) : gaussSum q ^ 2 = ↑(Fintype.card V)

The Gauss sum squares to #V for a nonsingular form: the character-sum identity g(q)² = ∑_u (−1)^{q(u)} ∑_x (−1)^{B(x,u)} = (−1)^{q(0)}·#V.

From the Gauss sum to the zero count

theorem GQ2.QuadraticFp2.gaussSum_eq {V : Type u_1} [Fintype V] (q : V → ZMod 2) : gaussSum q = 2 * ↑(zeroCount q) - ↑(Fintype.card V)

Bridge: g(q) = 2·#q⁻¹(0) − #V (the Gauss sum counts zeros minus ones).

theorem GQ2.QuadraticFp2.arf_eq_zero_iff_gaussSum_pos {V : Type u_1} [Fintype V] (q : V → ZMod 2) : arf q = 0 ↔ 0 < gaussSum q

The democratic arf is 0 exactly when the Gauss sum is positive (zeros a strict majority).

theorem GQ2.QuadraticFp2.gaussSum_eq_pow {V : Type u_1} [AddCommGroup V] [Fintype V] (q : V → ZMod 2) (hq : IsQuadraticFp2 q) (hns : Nonsingular q) {m : ℕ} (hcard : Fintype.card V = 2 ^ (2 * m)) : gaussSum q = 2 ^ m ∨ gaussSum q = -2 ^ m

For a nonsingular form with #V = 2^{2m}, the Gauss sum is ±2^m.

theorem GQ2.QuadraticFp2.zeroCount_of_arf_zero {V : Type u_1} [AddCommGroup V] [Fintype V] (q : V → ZMod 2) (hq : IsQuadraticFp2 q) (hns : Nonsingular q) {m : ℕ} (hm : 1 ≤ m) (hcard : Fintype.card V = 2 ^ (2 * m)) (harf : arf q = 0) : zeroCount q = 2 ^ (2 * m - 1) + 2 ^ (m - 1)

Zero count, arf = 0 (positive Gauss sign): #q⁻¹(0) = 2^{2m−1} + 2^{m−1}.

theorem GQ2.QuadraticFp2.zeroCount_of_arf_one {V : Type u_1} [AddCommGroup V] [Fintype V] (q : V → ZMod 2) (hq : IsQuadraticFp2 q) (hns : Nonsingular q) {m : ℕ} (hm : 1 ≤ m) (hcard : Fintype.card V = 2 ^ (2 * m)) (harf : arf q = 1) : zeroCount q = 2 ^ (2 * m - 1) - 2 ^ (m - 1)

Zero count, arf = 1 (negative Gauss sign): #q⁻¹(0) = 2^{2m−1} − 2^{m−1}.

Lemma 6.6 (Wall doubling) — structural reformulations

The doubling has the clean shape q_U = q + q∘(1+U): since U is an isometry, B(x, Ux) = q(x + Ux) (q(Ux) = q(x) cancels the cross terms). This makes the polar form of q_U transparently B_U(x,y) = B(x,y) + B((1+U)x, (1+U)y).

theorem GQ2.QuadraticFp2.qDouble_eq_add {V : Type u_1} [AddCommGroup V] (q : V → ZMod 2) (U : V ≃+ V) (hUq : ∀ (v : V), q (U v) = q v) (x : V) : qDouble q (⇑U) x = q x + q (x + U x)

q_U(x) = q(x) + q((1+U)x).

theorem GQ2.QuadraticFp2.polar_qDouble {V : Type u_1} [AddCommGroup V] (q : V → ZMod 2) (U : V ≃+ V) (hUq : ∀ (v : V), q (U v) = q v) (x y : V) : polar (qDouble q ⇑U) x y = polar q x y + polar q (x + U x) (y + U y)

The polar form of the doubling: B_U(x,y) = B(x,y) + B((1+U)x, (1+U)y).

theorem GQ2.QuadraticFp2.exists_card_eq_two_pow {W : Type u_2} [AddCommGroup W] [Finite W] (h2 : ∀ (w : W), w + w = 0) : ∃ (k : ℕ), Nat.card W = 2 ^ k

A finite elementary abelian 2-group has 2-power cardinality.

theorem GQ2.QuadraticFp2.exists_card_range_eq_two_pow {V : Type u_2} [AddCommGroup V] [Finite V] (h2 : ∀ (v : V), v + v = 0) (f : V →+ V) : ∃ (k : ℕ), Nat.card ↥f.range = 2 ^ k

The range of 1 + U has 2-power cardinality (it is a subgroup of the elem. ab. 2-group V).

Lemma 6.6 — nonsingularity of the doubling

B_U(x,y) = B(x, (1+U+U⁻¹)y), so q_U is nonsingular iff 1+U+U⁻¹ (equivalently 1+U+U²) is injective — true for a 2-power-order U: U³y = y ⟹ Uy = y (the fixed point has period dividing gcd(3, 2ⁿ) = 1), and on fix U the operator 1+U+U² acts as 3 = 1 ≠ 0.

theorem GQ2.QuadraticFp2.polar_isometry_both {V : Type u_2} [AddCommGroup V] (q : V → ZMod 2) (U : V ≃+ V) (hUq : ∀ (v : V), q (U v) = q v) (x y : V) : polar q (U x) (U y) = polar q x y

Isometry: B(Ux, Uy) = B(x, y).

theorem GQ2.QuadraticFp2.polar_isometry_left {V : Type u_2} [AddCommGroup V] (q : V → ZMod 2) (U : V ≃+ V) (hUq : ∀ (v : V), q (U v) = q v) (x y : V) : polar q (U x) y = polar q x (U.symm y)

Isometry adjoint: B(Ux, y) = B(x, U⁻¹y).

theorem GQ2.QuadraticFp2.polar_qDouble_eq {V : Type u_2} [AddCommGroup V] (q : V → ZMod 2) (U : V ≃+ V) (hq : IsQuadraticFp2 q) (hUq : ∀ (v : V), q (U v) = q v) (x y : V) : polar (qDouble q ⇑U) x y = polar q x (y + U y + U.symm y)

B_U(x,y) = B(x, (1 + U + U⁻¹)y).

theorem GQ2.QuadraticFp2.onePlusUUsq_injective {V : Type u_2} [AddCommGroup V] (U : V ≃+ V) (h2 : ∀ (v : V), v + v = 0) (hU2 : ∃ (n : ℕ), (⇑U)^[2 ^ n] = id) (y : V) (hy : y + U y + U (U y) = 0) : y = 0

(1 + U + U²) is injective for a 2-power-order isometry U on an exponent-2 group: (1+U+U²)y = 0 ⟹ Uy = y (period divides gcd(3, 2ⁿ) = 1), whence y = 3y = 0.

theorem GQ2.QuadraticFp2.qDouble_nonsingular {V : Type u_2} [AddCommGroup V] (q : V → ZMod 2) (U : V ≃+ V) [Finite V] (hq : IsQuadraticFp2 q) (h2 : ∀ (v : V), v + v = 0) (hns : Nonsingular q) (hUq : ∀ (v : V), q (U v) = q v) (hU2 : ∃ (n : ℕ), (⇑U)^[2 ^ n] = id) : Nonsingular (qDouble q ⇑U)

Lemma 6.6, nonsingularity: for a nonsingular q and a 2-power-order isometry U, the doubling q_U is nonsingular (1 + U + U⁻¹ is bijective on the finite V).

theorem GQ2.QuadraticFp2.gaussSum_ne_zero {V : Type u_2} [AddCommGroup V] (q : V → ZMod 2) [Fintype V] (hq : IsQuadraticFp2 q) (hns : Nonsingular q) : gaussSum q ≠ 0

The Gauss sum of a nonsingular form is nonzero (its square is #V ≥ 1).

theorem GQ2.QuadraticFp2.arf_qDouble_of_gaussSum_sign {V : Type u_2} [AddCommGroup V] (q : V → ZMod 2) (U : V ≃+ V) [Fintype V] {k : ℕ} (hgne : gaussSum q ≠ 0) (hsign : gaussSum (qDouble q ⇑U) = (-1) ^ k * gaussSum q) : arf (qDouble q ⇑U) = arf q + ↑k

Arf-additivity from the Gauss-sum sign (the reduction of Lemma 6.6's Arf clause): given the Wall sign relation g(q_U) = (−1)ᵏ g(q), the democratic Arf invariants satisfy arf(q_U) = arf(q) + k. (Both Gauss sums are nonzero, so the sign of (−1)ᵏ flips arf by k mod 2.)

Wall's sign relation — the abstract Wall count

Lemma 6.6's remaining piece is Wall's sign g(q_U) = (−1)^k g(q), 2^k = #im(1+U). Following the paper's proof, everything reduces to the Wall count: the Wall form ω(Nx, u) = B(x, u) on R = im N (N = 1 + U) satisfies

∑_{t,u ∈ R} (−1)^{ω(t,t) + ω(u,u) + ω(t,u)} = (−2)^{dim R}.

We prove the count abstractly, for a biadditive ω on a finite elementary abelian 2-group W that is right-nondegenerate and admits a 2-power-order monodromy M (ω t u = ω u (M t); in the application M = U⁻¹|_R). The monodromy hypothesis is essential: the count is false for a general nondegenerate ω (ω = [[1,1],[0,1]] on 𝔽₂² has count −8 ≠ (−2)²). It enters by producing a nonzero M-fixed vector a — whose row and column functionals agree — along which the induction splits: if ω a a = 1, splitting off ⟨a⟩ factors the count by −2; if ω a a = 0, a shift-pairing kills all terms outside ker (ω a)² and ⟨a⟩ acts freely on what remains, giving a factor 4 = (−2)².

theorem GQ2.QuadraticFp2.exists_fixed_ne_zero {W : Type u_2} [AddCommGroup W] (h2 : ∀ (w : W), w + w = 0) (n : ℕ) (M : W ≃+ W) : (⇑M)^[2 ^ n] = id → ∀ (w₀ : W), w₀ ≠ 0 → ∃ (a : W), a ≠ 0 ∧ M a = a

A 2-power-order automorphism of an exponent-2 group with a nonzero element has a nonzero fixed vector: a fixed vector a of M² yields the M-fixed a + Ma, which vanishes only if a itself is already M-fixed.

theorem GQ2.QuadraticFp2.sum_neg_shift_eq_zero {W : Type u_2} [AddCommGroup W] [Fintype W] (f : W → ℤ) (r₀ : W) (h : ∀ (x : W), f (x + r₀) = -f x) : ∑ x : W, f x = 0

Reindexing an integer sum along a sign-reversing shift: if f (x + r₀) = − f x pointwise then ∑ f = 0.

theorem GQ2.QuadraticFp2.wall_count {W : Type u} [AddCommGroup W] [Fintype W] (h2 : ∀ (w : W), w + w = 0) (ω : W →+ W →+ ZMod 2) (M : W ≃+ W) (hM : ∀ (t u : W), (ω t) u = (ω u) (M t)) (hM2 : ∃ (m : ℕ), (⇑M)^[2 ^ m] = id) (hnd : ∀ (u : W), (∀ (t : W), (ω t) u = 0) → u = 0) {k : ℕ} (hk : Nat.card W = 2 ^ k) : ∑ t : W, ∑ u : W, sign ((ω t) t + (ω u) u + (ω t) u) = (-2) ^ k

The abstract Wall count: for a biadditive ω on a finite exponent-2 group W, right-nondegenerate and admitting a 2-power-order monodromy M (ω t u = ω u (M t)),

∑_{t,u} (−1)^{ω(t,t) + ω(u,u) + ω(t,u)} = (−2)^k, where #W = 2^k.

In the application to Lemma 6.6 (Wall's sign relation), W = im (1 + U), ω is the Wall form ω(Nx, u) = B(x, u), and the monodromy is U⁻¹ (which is where the 2-power-order hypothesis on U enters).