Stage G — the Dickson zero-count of a nonsingular `F₂` quadratic form #

This file closes the two finite-field Gauss-sum axioms of Quadratic/GaussSign.lean (prop:candidatezero / prop:localzero):

candidate_base_zeroCount and q2_local_base_zeroCount, both in the consistent existential form ∃ ram, (numZeros q : ℤ) = baseZeroCount ram (finrank V) for a nonsingular QuadF2 form q.

Both axioms are the same statement (the candidate qc and the local ql are just two instances of an arbitrary nonsingular F₂ quadratic space), so a single general theorem — nonsingular_numZeros_dickson — discharges both. This is the classical Dickson / Arf count: a nonsingular quadratic form of dimension d over F₂ has 2^{d-1} ± 2^{d/2-1} zeros, the sign being (-1)^{Arf}. It is finite-field linear algebra (NOT local CFT), proven here sorry-free with no new axioms.

Method: the Gauss sum (avoids an explicit Witt/Arf decomposition) #

Let χ : F₂ → ℤ be the sign character (χ 0 = 1, χ 1 = -1; multiplicative, χ(a+b) = χ a · χ b), and let D := ∑_{v} χ(q v) be the Gauss sum. Two clean identities pin down the zero count:

Counting. χ(q v) = 2·[q v = 0] - 1, so D = 2·#Q⁻¹(0) - |V|, i.e. 2·numZeros q = |V| + D (two_mul_numZeros).
Square. D² = |V| (gaussSum_sq). Indeed D² = ∑_{v,w} χ(q v + q w); reindexing w = v + u and using the quadratic law q v + q(v+u) = q u + b(v,u) gives D² = ∑_u χ(q u)·∑_v χ(b(v,u)). The inner sum is |V| when b(·,u) ≡ 0 and 0 otherwise (a nonzero F₂-functional is killed by the translation v ↦ v + y, b(y,u) = 1); nonsingularity forces b(·,u) ≡ 0 ⇔ u = 0, leaving only the u = 0 term = |V|.

With |V| = 2^d (FiniteField.pow_finrank_eq_card) we get D² = 2^d, so d is even and D = ±2^{d/2} (extracted via Nat.dvd_prime_pow); then numZeros q = (2^d + D)/2 = 2^{d-1} ± 2^{d/2-1} = baseZeroCount ram d.

A residual edge case (reported): `d = 0` #

baseZeroCount ram d = 2^{d-1} + (±1)·2^{d/2-1} uses truncated nat subtraction. For even d ≥ 2 this equals the honest (2^d ± 2^{d/2})/2, and everything matches. But at d = 0 (the zero space V = 0, vacuously nonsingular) it gives baseZeroCount true 0 = 2, baseZeroCount false 0 = 0, whereas the true count is numZeros = 1. So the verbatim axiom statement (which quantifies over all finite V, including V = 0) is in fact FALSE at V = 0 — the existential ∃-fix removed the old double-ram inconsistency but a d = 0 inconsistency remains (see baseZeroCount_zero_false / dickson_count_false_at_zero below).

The fix is a single hypothesis 0 < finrank V (equivalently [Nontrivial V]), which is automatic for the candidate/local applications (nonzero self-dual simple modules). The main theorem therefore carries 0 < finrank V, and the drop-in corollaries candidate_base_zeroCount_proven / q2_local_base_zeroCount_proven add [Nontrivial V] to the verbatim axiom signature. Modulo that one instance they are the axioms and can replace them; GaussSign.lean only needs the same [Nontrivial V] added to the two axiom lines for a literal swap.

Stage G — the Dickson zero-count of a nonsingular F₂ quadratic form #

Method: the Gauss sum (avoids an explicit Witt/Arf decomposition) #

A residual edge case (reported): d = 0 #

The sign character χ : F₂ → ℤ #

The Gauss sum and its square #

The counting identity #

Extracting the Dickson count from D² = 2^d #

The Dickson zero-count theorem and the two corollaries #

The reported d = 0 edge case, rigorously #

The Gauss-type pinning and the §6 comparison (re-homed) #

Stage G — the Dickson zero-count of a nonsingular `F₂` quadratic form #

A residual edge case (reported): `d = 0` #

The sign character `χ : F₂ → ℤ` #

Extracting the Dickson count from `D² = 2^d` #

The reported `d = 0` edge case, rigorously #