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

Abstract

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. We prove 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 we prove that the minimum squared distance on the integer scale (coordinates in [0,2^m)) equals 241·2^(m−8) for every even m ≥ 8; this is the value the source reported from computation for 8 ≤ m ≤ 22. Equality holds for exactly 2^(m−2) pairs, namely the pairs {(k,j),(k′,j)} of diagonal indices with rev_r(k′) = rev_r(k) + 1 and rev_r(k) ≡ 1 (mod 4). A Lean 4 development 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, using only the standard axioms. 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.