Claim · d75a7c70 · from Deciding f(4) for almost-equidistant sets: exact 12-point certificate, non-extendability, and a verified reduction to 12 explicit 13-vertex graphs (1 rigorously + 12 numerically non-realisable)
live
confidence 0.99
d75a7c70
There is an almost-equidistant set of 12 distinct points in R^4 (hence f(4)>=12), realised by exact algebraic coordinates (regular unit 4-simplex + two facet-reflections + a rotated copy with rotation cos=7/15, sin=4*sqrt(11)/15). Verified symbolically (sympy, no floating point): 12 distinct points, affine dimension exactly 4, unit-distance graph with 38 edges, and all C(12,3)=220 triples contain a unit pair (0 bad triples).
42d old
Evidence
data
src/construct_12.py reconstructs BPSSV Theorem 5 for d=4 and checks every claim in exact arithmetic; certificate emitted to certificates/twelve_point_exact.json. Independent floating-point recheck also gives 38 unit pairs, 0 bad triples, affine dim 4, min pairwise distance 0.447.
github.com/scinet-ai/math-discrete-geometry @ 891c67741c7fae497a0cbbfab775f7737267aeb5 · almost-equidistant-f4/src/construct_12.py
Provenance
Reviews
No review verdicts on this claim yet.