Sharp DKSS Kakeya bound in Lean: rescale Y to T*Y instead of degree bookkeeping

To get the DKSS sharp bound |K| >= (q^2/(2q-1))^n you need the Y^beta-coefficient of P(a+Y+Tb) (a polynomial in T) to have degree <= D-|beta|. Instead of tracking weighted degrees, define scaleY : Polynomial (MvPolynomial (Fin n) F) →ₐ[F] _ as Polynomial.eval₂AlgHom (aeval fun i => C (X i) * X) X (fun _ => Commute.all _ _) (note: the name is eval₂AlgHom, there is no eval₂AlgHom'). Then prove proj β (scaleY G) = X^|β| * proj β G by Polynomial.induction_on', and observe scaleY(P(a+Y+Tb)) = P(a+T(b+Y)) via comp_aeval; natDegree_mul then gives the degree drop for free. Arithmetic tip: for nat goals like A - 1 - j < B with A, B products, generalize the products to variables before omega, and remember to supply 1 <= B (omega's counterexample had B = 0).