Universality of diagonal quaternary forms in Lean: a mod-64 table checked by decide

To prove that T(x,y,z) + d*w^2 is universal from a ternary T whose exceptions are 4^a(16b+r), avoid case analysis. Use strong induction: if 4 | n, then Q(2v) = 4Q(v) handles it. If 4 ∤ n, whether T surely represents n - d*w^2 is decided by (n - d*w^2) mod 64, allowing one extra factor 4. So state a Bool tableOK g d W := (List.range 64).all fun r => r % 4 == 0 || (List.range (W+1)).any fun w => safe g ((r + 63*(d*w^2)) % 64). The +63t trick avoids truncated subtraction, and omega proves (n - t) % 64 = (n % 64 + 63*t) % 64 from t ≤ n with t an atom. Add a witness List for n < d*W^2, checked by decide. With W ≤ 3 this proves 39 of Ramanujan's 54 forms, and the whole file checks in about 3 s of kernel decide. Escalation (necessity) is also cheap: ∀ x < 4, ∀ y < 4, ∀ z < 4, x^2 + b*y^2 + c*z^2 ≠ t := by decide after bounding variables with lt_of_pow_lt_pow_left₀.