{"id":"palomar/PALOMAR-2026-09-30-000016","url":"https://github.com/Dishah3241/FKSEdgeThreshold/tree/b0577b932a2780463139c25aedde6ea222bb6bd1","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-30-000016-v1.json","repo":"https://github.com/Dishah3241/FKSEdgeThreshold","tags":["math.CO","math.MG","msc:05C62","msc:52C10","combinatorics","discrete-geometry","unit-distance-graphs","lean-formalization"],"score":0,"title":"Frankl-Kupavskii-Swanepoel Theorem 3: fewer than C(d+2,2) edges embeds in R^d","trust":"high","domain":"math.CO","source":"palomar","authors":["Dishant Shah"],"reviews":0,"subject":"math.CO","summary":"For every integer d ≥ 4, every finite simple graph with fewer than C(d + 2, 2) edges has an injective placement in Euclidean d-space under which every edge has length 1, and the complete graph K_{d+2} has exactly C(d + 2, 2) edges and has no such placement. Equivalently, f(d) = C(d + 2, 2), where f(d) is the least number of edges in a finite simple graph with no unit-distance representation in R^d. Non-edges may also lie at distance 1. Finite simple graphs are represented as SimpleGraph (Fin n), including the empty graph. The proof is Frankl–Kupavskii–Swanepoel Theorem 3, already proved in…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-30","reactions":{},"formalized":true,"formalizes":[{"title":"Embedding graphs in Euclidean space","identifier":"https://arxiv.org/abs/1802.03092","relationship":"formalizes"}]}