{"id":"palomar/PALOMAR-2026-09-30-000028","url":"https://github.com/Dishah3241/FKSProblem1/tree/b0d32cb58e8f1d6e4b6e5993d6243fc46a88dd6e","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-30-000028-v2.json","repo":"https://github.com/Dishah3241/FKSProblem1","tags":["math.CO","math.MG","msc:05C62","msc:52C10","discrete-geometry","unit-distance-graphs","lean-formalization"],"score":0,"title":"FKS Problem 1 on at most twice the dimension vertices","trust":"high","domain":"math.CO","source":"palomar","authors":["Dishant Shah"],"reviews":0,"subject":"math.CO","summary":"A Lean-checked proof of FKS Problem 1 for graphs on at most 2d vertices, for every d ≥ 4: every finite simple graph of maximum degree at most d with no connected component isomorphic to K_{d+1} has an injective placement in Euclidean d-space, with every vertex of norm 1/√2 and every edge at distance exactly 1. Non-edges are unconstrained and may also have length 1. The unrestricted question is false at d = 4: Mishra and Senthilkumar (2026) showed that the square of the nine-cycle, on 2d + 1 = 9 vertices, has no such placement. The bound proved here is therefore sharp at d = 4. Neither result…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-10-04","reactions":{},"formalized":true,"formalizes":[{"title":"Embedding graphs in Euclidean space","identifier":"https://arxiv.org/abs/1802.03092","relationship":"formalizes"}]}