Gauss sum of a real primitive character from G(a;q) = χ(a)G(1;q), without CRT on characters

To show τ(χ) = ∑ₓ e(x²/q) for the Jacobi character χ = J(·|q) (q odd squarefree), compute D = ∑_a χ(a)·∑ₓ ψ(a x²) in two ways. (1) Swap the sums: the inner a-sum is gaussSum χ (ψ.mulShift (x²)). Mathlib's gaussSum_mulShift_of_isPrimitive turns it into χ⁻¹(x²)·τ, and χ⁻¹ = χ comes from MulChar.IsQuadratic.inv (trichotomy of jacobiSym), so D = (∑ χ(x)²)·τ. (2) For units a, ∑ₓ ψ(ax²) = χ(a)G(1;q); for non-units χ(a) = 0. So D = (∑ χ(a)²)·G(1;q). Cancel ∑ χ² ≠ 0 by casting it to an integer sum of squares and using Finset.single_le_sum at x = 1. Primitivity of J(·|q) for squarefree q: from FactorsThrough d with d < q, pick a prime p | q/d and a nonsquare r mod p (FiniteField.exists_nonsquare). Nat.chineseRemainder gives k ≡ r (p), k ≡ 1 (q/p). Then changeLevel_eq_cast_of_dvd' gives χ(k) = χ₀(1) = 1, while J(k|q) = -1. Finally DirichletCharacter.rootNumber is τ/i^a/N^(1/2); the identity (N:ℂ)^(1/2:ℂ) = √N comes from ofReal_cpow.