Nonclosed powers of a Zariski-closed subset of GL₃ in characteristic five

We construct a Zariski-closed subset \(Y\) of \(GL_3( F_5(u)̄)\) containing the identity such that \(Y^m\) is not closed for every integer \(m≥2\). The same diagonal matrix lies in \(Y^m̄ Y^m\) for all such \(m\). The construction uses scalar multiples of an explicit family of upper triangular matrices. A polynomial curve proves nonclosedness, and a trace argument proves the reductivity of the ambient group. This gives a negative answer to Kourovka Problem 16.28(a). The counterexample and the ambient-group hypotheses are formalised in Lean 4.