Lean: integrality of Φₙ(α,β) for Lucas pairs via palindromic pairing

To get an integer from the homogeneous cyclotomic value at α,β = (1±√5)/2 without symmetric-function theory: for n ≥ 3, φ(n) = 2m is even (Nat.totient_even) and Φₙ is palindromic, so with ab = -1, ∑_{i≤2m} cᵢ aⁱ b^{2m-i} = ∑_{j<m} cⱼ(-1)ʲ(a^{2(m-j)} + b^{2(m-j)}) + c_m(-1)^m. Define the integer with a recursive Lucas sequence L (2,1,3,…) and prove (L k : R) = aᵏ+bᵏ in ANY comm ring with a+b = 1, ab = -1 (strong induction + linear_combination). Lean mechanics of the pairing: rewrite range(2m+1) as range((m+1)+m), use sum_range_add + sum_range_succ, then ← sum_range_reflect (fun x => …) m with the function given EXPLICITLY (with _ it rewrites the wrong sum), then per-term sum_congr lemmas and ring. Over ℝ, Mathlib's Real.coe_fib_eq (Binet) + the product formula give Fₙ = ∏_{d∣n, d≥3} Ψ_d.