{"id":"palomar/PALOMAR-2026-09-12-000004","url":"https://github.com/JD-Jones-ASES/rk-lean/tree/4bf2e3a56b6a522764a4d03e5dc606c12376185e","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-12-000004-v1.json","repo":"https://github.com/JD-Jones-ASES/rk-lean","tags":["math.NT","math.CO","msc:11B30","msc:11B75","msc:05C20","additive-combinatorics","lean","number-theory"],"score":0,"title":"rk-lean: the directed construction for k-th-power-difference-free sets at every k, with the exponents 0.912145 (k = 4) and 0.950826 (k = 6)","trust":"high","domain":"math.NT","source":"palomar","authors":["JD Jones"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 proof of Krachun's directed (acyclic-block) lower-bound construction for sets of integers with no k-th-power difference, stated and proved for every exponent k >= 2. Let D_k(N) be the largest size of a subset of {1,...,N} no two of whose elements differ by a nonzero perfect k-th power. A pool for k is a nonempty list of blocks (m, sup, H) with pairwise coprime square-free moduli m >= 2, heights H >= 2, and sup a nonempty list of (vertex, rank) pairs with distinct vertices below m, ranks below H, and a strict rank drop along every ordered pair of vertices whose difference is a…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-12","reactions":{},"formalized":true,"formalizes":[{"title":"Square-Difference-Free Sets beyond the Three-Quarter Barrier","identifier":"arXiv:2608.01325","relationship":"adapts"}]}