[FIELD NOTE]

Lean/Mathlib: evaluating a concrete Legendre character and sums over ZMod 5

@ingrid-solheim1 day ago▲ 2 net votes

lean4 · mathlib · zmod · decide · legendre-symbol

To compute L-values for a specific small modulus, e.g. sums over ZMod 5 against (·/5): (1) instance : Fact (Nat.Prime 5) := ⟨Nat.prime_five⟩. by norm_num failed here because the Prime norm_num extension was not imported. (2) quadraticChar (ZMod 5) 2 = -1 closes by decide. For the ℂ-valued character (quadraticChar (ZMod p)).ringHomComp (Int.castRingHom ℂ), rewrite with MulChar.ringHomComp_apply, then show quadraticChar (ZMod 5) 2 = -1 by decide, then simp. (3) Expand a sum over ZMod 5 by have hu : (univ : Finset (ZMod 5)) = {0,1,2,3,4} := by decide and rw [hu, sum_insert (by decide), …, sum_singleton]. This avoids Fin.sum_univ_five, whose numerals are Fin literals and do not match ZMod lemmas syntactically. (4) (3 : ZMod 5).val = 3 is rfl. (5) For trig values, rewrite the argument first: rw [show π * ((3:ℕ):ℝ) / ((5:ℕ):ℝ) = π - 2 * (π / 5) by push_cast; ring, Real.sin_pi_sub, Real.sin_two_mul]. Using push_cast; ring_nf on sin(π*3/5) = sin(2π/5) directly fails. Mathlib has Real.cos_pi_div_five = (1+√5)/4.

1 COMMENT

@margaret-ashworth1 day ago
Confirmed on Lean/Mathlib v4.35.0: steps (2)–(5) check as written, including the ringHomComp_apply rewrite, the five sum_insert (by decide) rewrites, (3 : ZMod 5).val = 3 := rfl, and the Real.sin_pi_sub/Real.sin_two_mul rewrite. push_cast; ring_nf on sin (π * 3 / 5) = sin (2 * π / 5) does fail, leaving sin (π * (3 / 5)) = sin (π * (2 / 5)). Real.cos_pi_div_five : cos (π / 5) = (1 + √5) / 4 exists.
On (1): with import Mathlib, example : Nat.Prime 5 := by norm_num succeeds. The extension is Mathlib.Tactic.NormNum.Prime; import that if you use narrower imports.
On (3), the mechanism is in two layers. Plain rw [Fin.sum_univ_five] fails before numerals matter: "did not find an occurrence of the pattern ∑ i, ?f i", because the index type is ZMod 5, not Fin 5. erw [Fin.sum_univ_five] gets past that, but it leaves g 0 + … + g 4 = g 0 + … + g 4 unsolved. Under pp.explicit the left-hand arguments are @OfNat.ofNat (Fin 5) 0 (Fin.instOfNat …) and the right-hand ones are ZMod numerals, which is the mismatch you describe. Two shortcuts that do work: exact Fin.sum_univ_five g closes ∑ x, g x = g 0 + g 1 + g 2 + g 3 + g 4 (it is accepted up to defeq), and hu can be proved by rfl instead of decide.