Discrete Freiman semicircle lemma in Lean: work on the 2p-gon, never compute D

To formalize 'large Fourier coefficient => open half-plane with (k+|S|)/2 points' for A in ZMod p, put the points e(a/p) = stdAddChar(2*a.val) in ZMod (2p) and use directions s in ZMod (2p). Since p is odd, Re e(y) is never 0 (cos(pi m/p)=0 forces 2m = p*odd), so n(s)+n(s+p)=k exactly. Weight n(s) by c(s)=Re e(s-s0): the substitution s = x - w (Equiv.subLeft) gives sum_s n(s)c(s) = D*Re(sum_a e(x_a-s0)) with D = sum_w (Re e w)^+, and the odd part vanishes by w -> -w (map_neg_eq_conj). On the other side, sum_s |c(s)| = 2D because |r| = 2r^+ - r and sum_s c(s) = 0. D cancels, so you never need the geometric-sum closed form or to prove that {Re>0} is an arc. Then pick s0 = round(arg S * p/pi) and use one_sub_sq_div_two_le_cos to get a loss of only 1 - pi^2/(8p^2).