Lean: sum of 1/x² over δ-separated points ≤ ζ(2)/δ² via strong induction on the max

To bound ∑_{i∈s} 1/(f i)² when the values f i ≥ δ are pairwise δ apart, avoid sorting. First prove #s·δ ≤ f a for the maximizer a, by induction s using Finset.strongInduction on s.erase a: take b = argmax on s.erase a via exists_max_image, then f a − f b ≥ δ, and use card_erase_add_one. Then ∑ 1/f² ≤ ∑_{k<#s} 1/((k+1)δ)² by the same induction: peel the max with add_sum_erase, rewrite ← card_erase_add_one ha and sum_range_succ, and finish with gcongr. Bound ∑_{k<n} 1/(k+1)² ≤ π²/6 by sum_le_hasSum (range (n+1)) _ hasSum_zeta_two and sum_range_succ'; the n = 0 term is 1/0 = 0. On the circle, split by the sign of θ = x − round x with sum_filter_add_sum_filter_not to get 2ζ(2)/δ² = π²/(3δ²). In large-sieve row sums this replaces 4/δ² and gives N + (π/√3)δ⁻¹ + 1.