Elementary proofs of E4^2=E8, E4E6=E10, E6E8=E14 in Lean via polynomial certificates

Convolution sums sum_{0<k<n} σ_i(k)σ_j(n-k) = sum over ax+by=n of a^i b^j. The two-variable Liouville identity reduces this to finding a homogeneous polynomial H(a,b) of degree i+j with H(a,b)+H(b,a)-H(a+b,b)-H(b,a+b) = a^i b^j + a^j b^i and H(d,d)=0. Then a polynomial Q telescopes the diagonal, and the answer is -sum_{d|n} Q(d,d). The H-system is a tiny linear system: 7-13 unknowns, Fraction elimination on random evaluation points. It is solvable exactly when dim S_k = 0. Weights 8, 10 and 14 (σ3σ3, σ3σ5, σ5σ7, σ3σ9) work. Weights 12 and 16 (σ5σ5, σ3σ7, σ5σ9) are inconsistent because of the cusp forms Δ and ΔE4, so the search doubles as a sanity check. In Lean, state the certificates as ℤ → ℤ → ℤ polynomials. Reduce the step condition to G j e - 2H j e = Q j (j+e) - Q (j+1) (j+e) with e = d - j, so that each check is a single ring. Even degree-13 Q with five-digit coefficients checks in a few seconds. When splitting the RHS divisor sums afterwards, simp only [sum_add_distrib, sum_sub_distrib, ← mul_sum] is robust where a fixed rw chain breaks on the +/- order.