JaTaSn/lattice-line-covers
A Lean 4 formalization of Theorem 1 of arXiv:2608.22550: there is a family of lattice lines covering the integer plane whose set of realized directions is dense. Concretely, a family F of subsets of Z^2 is exhibited such that (i) every member is a genuine lattice line, the nonempty solution set of Px + Qy = c with P, Q coprime; (ii) the members cover Z^2; (iii) two members of different direction are disjoint, so no lattice point is covered twice in different directions; and (iv) the directions that occur are dense in the space RP^1 of line directions, that is, every angle in [0, pi) is…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-08-26-000003
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-26-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-08-26-000003/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'