recognitionThetaTerm_zero

formal source

 193  simp [costSpectrumValue_one]
 194
 195/-- At `n = 0` the term vanishes because `χ₈(0) = 0`. -/
 196@[simp] theorem recognitionThetaTerm_zero (t : ℝ) :
 197    recognitionThetaTerm t 0 = 0 := by
 198  unfold recognitionThetaTerm
 199  simp
 200
 201/-- The term at `n = 2` vanishes because `χ₈(2) = 0`. -/
 202theorem recognitionThetaTerm_two (t : ℝ) :
 203    recognitionThetaTerm t 2 = 0 := by
 204  unfold recognitionThetaTerm
 205  rw [chi8_two]
 206  ring
 207
 208/-- Even-residue terms vanish.  Equivalently, only odd integers
 209    coprime to 2 (and indeed coprime to 8) contribute non-zero
 210    terms. -/
 211theorem recognitionThetaTerm_even {n : ℕ} (t : ℝ) (h : n % 2 = 0) :
 212    recognitionThetaTerm t n = 0 := by
 213  unfold recognitionThetaTerm
 214  have h_chi : chi8 n = 0 := by
 215    unfold chi8
 216    have h_lt : n % 8 < 8 := Nat.mod_lt _ (by norm_num)
 217    have h_mod2 : n % 8 % 2 = 0 := by omega
 218    -- The cases where n%8 is even (0,2,4,6) all give chi8 = 0 by def;
 219    -- the odd cases (1,3,5,7) contradict h_mod2.
 220    interval_cases (n % 8) <;> first | rfl | omega
 221  rw [h_chi]
 222  ring
 223
 224/-- The Recognition Theta function as a tsum.  Convergence is part of
 225    Sub-conjecture A.1 (the analytic content); the tsum is well-defined
 226    in any case (defaults to 0 if not summable). -/