The Even-Order Grünschloß–Keller Permutation Nets Are (0,m,2)-Nets

Grünschloß and Keller (2009) constructed two-dimensional base-2 point sets with large minimum toroidal distance by a nonlinear permutation rule. For odd m they proved that the 2^m points form a (0,m,2)-net; for even m they verified the net property by computer through m = 22 and left a proof open. This note proves that the even-order construction is a (0,m,2)-net for every even m ≥ 4. The proof writes the first coordinate as an exact concatenation of ⌊k/4⌋ and a bit-reversal term and inverts every dyadic prefix map explicitly. For the row-shifted tiling metric of the source, the minimum squared distance on the integer scale 2^m equals 241·2^(m−8) for every even m ≥ 8, the value the source reported from computation for 8 ≤ m ≤ 22; equality holds for exactly 2^(m−2) pairs. A Lean 4 development (Lean 4.30.0, Mathlib v4.30.0, standard axioms only, kernel reduction only) checks the net theorem for every even m ≥ 4, the upper bound for every even m ≥ 8, and the exact minimum at m = 8 over all pairs and lattice translates. Three independent exact generators reproduce the point sets and the distances, with all pairs through m = 16 and the reduced cases of the proof through m = 30. Included materials. This record contains the preprint, its source archive, three exact checkers with captured logs, the published MIT-licensed generator header, the identical m = 8 point lists, the pinned Lean 4 project in Palomar layout with its build records, and the provenance and validation records. Licensing. The manuscript, documentation, and author-generated data are licensed under Creative Commons Attribution 4.0 International. Original Go, Python, and Lean source code is licensed under the MIT License. The included generator header retains its author's MIT license; the included BibTeX style is LPPL; see LICENSE-MAP.md.