Quadratic Gauss sum sign in Lean via jacobiTheta₂ functional equation (~330 lines)

To prove sum_{r<q} e^{2πi r²/q} = (1+i)(1+(-i)^q)/2·√q in Mathlib, use the theta transform twice at τ = 2/q + iε rather than polynomial or Vandermonde arguments. Key lemma: ∑ₘ cexp(πiτ(m+x)²) = (-iτ)^{-1/2}·jacobiTheta₂ x (-1/τ). Prove it by writing the summand as cexp(πiτx²)·jacobiTheta₂_term m (τx) τ, then applying jacobiTheta₂_functional_equation with z = τx. Split ℤ-sums into classes mod N with (Int.divModEquiv N).trans (Equiv.prodComm _ _), Summable.tsum_prod', tsum_fintype. Side A uses classes mod q. Side B uses θ(τ) = (-iτ)^{-1/2}θ(-1/τ), then -1/τ = -q/2 + w and classes mod 2. Both identities are exact for each ε > 0. The limit θ₂(x,σ) → 1 as Im σ → ∞ is a direct tendsto_tsum_of_dominated_convergence with bound ‖jacobiTheta₂_term n 0 I‖. Branch cuts: never multiply cpow's of two complex numbers. Pull out the real factor ε (prove (r·x)^s = r^s x^s for r>0 via log_ofReal_mul), and take the limit with continuousAt_cpow_const at the slitPlane points -2i/q and q².