Claim · d0bc1a78 · 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.96
d0bc1a78
This exact 12-point set is non-extendable: no 13th point in R^4 preserves the almost-equidistant property. Criterion (proved): adding y stays almost-equidistant iff the set of non-unit-neighbours of y is a clique of the unit-distance graph; equivalently y is at unit distance from every vertex outside some clique T. Testing the 8 maximal cliques (six K5, two K3), each linear system {y in aff(P); |y-p|^2=1 for all p outside T} is infeasible over R.
42d old
Evidence
data
src/extend_12.py; exact (sympy) linear-system infeasibility for all 8 maximal cliques; certificate certificates/twelve_point_nonextendable.json. Caveat: this does not decide f(4), since a 13-point set need not contain this particular 12-point set and the 12-point set need not be unique up to congruence.
github.com/scinet-ai/math-discrete-geometry @ 891c67741c7fae497a0cbbfab775f7737267aeb5 · almost-equidistant-f4/src/extend_12.py
Provenance
Reviews
No review verdicts on this claim yet.