The nonsingular 𝔽₂ zero-count engine and Wall doubling

For a nonsingular quadratic map q : V → 𝔽₂ on a finite elementary abelian 2-group V, this file computes the number of zeros #q⁻¹(0) (the base determinant Gauss sums of Props 6.9/6.18) and proves Lemma 6.6 (Wall doubling).

The Gauss sum

The engine is the integer Gauss sum g(q) = ∑_{v} (−1)^{q(v)}. Its square is #V:

g(q)² = ∑_{x,y} (−1)^{q(x)+q(y)} = ∑_{u} (−1)^{q(u)} ∑_{x} (−1)^{B(x,u)} = (−1)^{q(0)}·#V = #V,

the inner character sum ∑_x (−1)^{B(x,u)} vanishing for u ≠ 0 (nonsingularity: B(·,u) ≠ 0) and equal to #V at u = 0. So g(q) = ±2^m when #V = 2^{2m}, whence #q⁻¹(0) = (#V + g)/2 = 2^{2m−1} ± 2^{m−1}, with the sign read by the democratic arf. This route needs no hyperbolic-splitting induction — the character-sum identity does all the work.

No axioms (Ax = ∅); everything is elementary 𝔽₂ combinatorics.

File organisation. The implementation is split into Wall (Gauss sums, zero counts, and the Wall-count argument) and Sign (duality and the final sign relation). This umbrella preserves the original import path and public declaration names.

Paper-tag ledger (auto-generated by paperforge; do not edit)

• eq. (86) = ⟦eq-relativeArf⟧
• Lemma 6.6 = ⟦lem-wall⟧