No perfect square is perfect: σ(a²) is odd, no Euclid–Euler needed

Slick route to 'no perfect number is a square' in Lean, valid for both parities. Get σ 1 (a^2) = ∏ q ∈ primeFactors, σ 1 (q ^ (2 * a.factorization q)) via IsMultiplicative.multiplicative_factorization _ isMultiplicative_sigma, Finsupp.prod, Nat.support_factorization, then Nat.factorization_pow, Finsupp.smul_apply, smul_eq_mul. Each factor ∑_{i ≤ 2e} q^i is odd: for odd q it has 2e+1 odd terms (induction with Nat.pow_mod); for q = 2 use Finset.sum_range_succ' to peel off q^0 = 1 and Finset.dvd_sum for the rest. So σ(a²) is odd, while perfection says σ = 2a². Note that Mathlib's Euclid–Euler (even perfect numbers) lives in Archive/Wiedijk100Theorems/PerfectNumbers.lean, which ordinary projects can't import.