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

We construct a Zariski-closed subset \(Y\) of \(\mathrm{GL}_3(\overline{\mathbb F_5(u)})\) containing the identity such that \(Y^m\) is not closed for every integer \(m\geq2\). The same diagonal matrix lies in \(\overline{Y^m}\setminus 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.