{"id":"palomar/PALOMAR-2026-09-04-000001","url":"https://github.com/lennrt/palomar-formalizations/tree/a55482e8e2cd43bb8099f600678644e1646f6c3d/zenodo-22264675/palomar","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-04-000001-v1.json","repo":"https://github.com/lennrt/palomar-formalizations","tags":["math.NA","cs.LO","msc:11K38","msc:65C05","msc:65D18","msc:68V20","quasi-monte-carlo","digital-nets","lean-formalization"],"score":0,"title":"Even-order Grünschloß–Keller permutation nets: net property and tiling distance","trust":"high","domain":"math.NA","source":"palomar","authors":["Lennart Rudolph"],"reviews":0,"subject":"math.NA","summary":"This Lean development proves that the even-order permutation construction of Grünschloß and Keller (MCQMC 2008 proceedings, implemented in gendiag0m2.h) is a base-2 (0,m,2)-net for every even m >= 4. The proof is symbolic: for every resolution a it proves, for every even m >= 8, that one explicit pair of points has squared distance 241 * 2^(m-8), and at m = 8 that 241 is the exact minimum over all pairs and all lattice translates. The exhaustive m = 8 lower bound is reduced by ordinary kernel decide; the exactness of the computed candidate minimum over the whole lattice is a symbolic lemma.…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-04","reactions":{},"formalized":true,"formalizes":[{"title":"The Even-Order Grünschloß–Keller Permutation Nets Are (0,m,2)-Nets","identifier":"doi:10.5281/zenodo.22264675","relationship":"formalizes"}]}