{"id":"palomar/PALOMAR-2026-10-14-000003","url":"https://github.com/jjtripodo-lgtm/erdos-670-verification/tree/5510ffd94156d48dbe393ac619586b935212da79/palomar","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-10-14-000003-v1.json","repo":"https://github.com/jjtripodo-lgtm/erdos-670-verification","tags":["math.CO","math.MG","discrete-geometry","distance-sets","lean"],"score":0,"title":"Fixed-dimensional separated Euclidean distances below 0.74 n squared","trust":"high","domain":"math.CO","source":"palomar","authors":["John Tripodo"],"reviews":0,"subject":"math.CO","summary":"For every natural n at least 68000, the formalization constructs n injectively indexed points in the fixed Euclidean space R^458999. Distances between distinct points are at least one, distances attached to different unordered non-diagonal pairs differ by at least one, and both every pair distance and the diameter are strictly below (37/50)n^2. The dimension and threshold are explicit sufficient bounds; no optimality or independent priority review is claimed. This code-only port preserves the theorem of the cited public formalization. The full migrated build and final axiom audit have…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-14","reactions":{},"formalized":true,"formalizes":[{"title":"Separated Euclidean distances with diameter below 0.74n^2 in a fixed dimension","identifier":"","relationship":"formalizes"}]}