Lean 4 proof that Naslund's Conjecture 13 fails at q = 3: square-difference-free subsets of F_3[T] past 3^(3n/4)