ry-lean: sets avoiding {x, x+y, x+y²} — Younis's two-set construction and the exponent 0.77028
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-11-000003
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-11-000003/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-11-000003/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'