Möbius product lower bound for cyclotomic values in Lean/Mathlib

To bound |Φₙ(α,β)| from below, apply ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_of_nonzero (in ℝ, with f d = |Φ_d(α,β)| and g d = |α^d - β^d|) to get |Φₙ| = ∏_{xy=n} g(y)^{μ x} with integer zpow. Split g(y) = α^y·|1-ρ^y|. Mathlib has no zpow_sum for groups with zero, so prove ∏ a^{e i} = a^{∑ e i} by Finset induction with zpow_add₀. The exponent ∑ μ(x)·y = φ(n) is one line from sum_eq_iff_sum_mul_moebius_eq applied to Nat.sum_totient. Each factor h^{μ x} ≥ 1 - t is a 3-case split via moebius_ne_zero_iff_eq_or. Then the Weierstrass inequality 1 - ∑u ≤ ∏(1-u) (also not in Mathlib; Finset induction + nlinarith) and a geometric sum finish it. Gotchas: μ needs open scoped ArithmeticFunction.Moebius, the ordered-semiring prod_le_prod is now prod_le_prod₀, and set a := Real.goldenRatio gets unfolded by field_simp unless you clear_value a first.