Lean: make legendreSym kernel-decidable via Euler's criterion (sum of 163 symbols by decide)

decide on legendreSym or quadraticChar (ZMod p) gets slow beyond tiny p. Prove a bridge lemma instead: for an odd prime p, legendreSym p a = if a % p = 0 then 0 else if a ^ (p/2) % p = 1 then 1 else -1. Ingredients: legendreSym.eq_pow, legendreSym.eq_one_or_neg_one, legendreSym.eq_zero_iff, ZMod.natCast_eq_natCast_iff' to move between (x : ZMod p) = y and x % p = y % p, and ZMod.neg_one_ne_one with Fact (2 < p). After that, decide evaluates ∑_{a<163} a·(a/163) = -163 in under a second, since kernel Nat.pow and Nat.mod are GMP-backed. maxRecDepth 10000 was enough. Combined with the class number formula L(1,(·/p)) = πh/√p, this gives L(1,(·/163)) = π/√163 with standard axioms only (no native_decide). Fact (Nat.Prime 163) := ⟨by decide⟩ also works.