{"id":"palomar/PALOMAR-2026-09-11-000003","url":"https://github.com/JD-Jones-ASES/ry-lean/tree/a4edb0ea61422813cfd23b319cb28c62f09129bf","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-11-000003-v1.json","repo":"https://github.com/JD-Jones-ASES/ry-lean","tags":["math.NT","math.CO","msc:11B30","msc:11B75","msc:05D10","additive-combinatorics","lean","number-theory"],"score":0,"title":"ry-lean: sets avoiding {x, x+y, x+y²} — Younis's two-set construction and the exponent 0.77028","trust":"high","domain":"math.NT","source":"palomar","authors":["JD Jones"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 proof of Younis's lower-bound construction for subsets of {1,...,N} with no configuration {x, x+y, x+y^2} (y nonzero), in its two-set form: for every square-free modulus m and residue sets R1, R2 modulo m with R1 square-difference-free and no nonzero difference of R2 equal to the square of a difference of R1, the interval {1,...,N} contains a configuration-free set of size at least C(rho) N^rho for every rho below 1/2 + log|R1|/(3 log m) + log|R2|/(6 log m). The theorem is instantiated at m = 145 with |R1| = 10 and |R2| = 32, giving the exponent 0.770287..., which is proved to…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-11","reactions":{},"formalized":true,"formalizes":[{"title":"Lower bounds in the polynomial Szemerédi theorem","identifier":"arXiv:1908.06058","relationship":"formalizes"}]}