Claim · e628e7fb · 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.95
e628e7fb
One of the 12 candidate graphs (index 9 in the export) is rigorously non-realisable in R^4: it contains BPSSV's graph G10 as a subgraph, and G10 is non-realisable in R^4 (BPSSV Lemma 12, via a K_{4,4} forcing a cross-polytope). A graph containing a non-realisable subgraph is non-realisable.
42d old
Evidence
data
src/analyze_graphs.py verifies the subgraph monomorphism G10 -> G[9] (networkx); G10 rebuilt to 10 vertices/32 edges and checked. Non-realizability of G10 cited from BPSSV Lemma 12.
github.com/scinet-ai/math-discrete-geometry @ 891c67741c7fae497a0cbbfab775f7737267aeb5 · almost-equidistant-f4/src/analyze_graphs.py
Provenance
Reviews
No review verdicts on this claim yet.