Dependencies

A graph has a unit-distance representation in \(\mathbb {R}^d\) when its vertices admit an injective placement in \(\mathbb {R}^d\) under which every edge has length one. Non-adjacent vertices are unconstrained and may also land one unit apart: this is the Erdős–Harary–Tutte notion, and the source tracks the faithful variant, which also forbids unit non-edges, separately as \(f_{FD}\). The frozen statement’s predicate and the shared library’s predicate agree definitionally (Lemma 27).

Five explicit graphs on \(\texttt{Fin 7}\) or \(\texttt{Fin 6}\), with their label conventions: the subdivision of \(K_{3,3}\) has parts \(0, 1, 2\) and \(3, 4, 5\), with the edge \(03\) replaced by \(06\) and \(63\) through the new vertex \(6\); the wheel has rim \(0, 1, 2, 3, 4\) and hub \(5\); the octahedron \(K_{2,2,2}\) has opposite pairs \(01, 23, 45\); \(K_{1,1,5}\) has singleton parts \(0\) and \(1\) and remaining part \(2, \dots , 6\); the cone over two triangles \(K_1 \vee (K_3 \sqcup K_3)\) has triangles \(012\) and \(345\) with universal hub \(6\). Each definition carries a characteristic adjacency lemma and a nondegenerate separating example in the library.

A graph on six vertices with ten edges and minimum degree at least three has a complement isomorphic to one of the four forms \(C_5 \sqcup K_1\), \(P_6\), \(C_4 \sqcup P_2\), or \(C_3 \sqcup P_3\).

If a graph \(G\) on seven vertices contains \(K_{3,3}\), then \(\overline G\) is contained in the cone \(K_1 \vee (K_3 \sqcup K_3)\).

If a graph \(G\) on seven vertices contains \(K_5\), then \(\overline G\) is contained in \(K_{1,1,5}\).

Let \(G\) have at most seven vertices and ten edges, contain no \(K_{3,3}\), and let \(v\) have precisely the two neighbours \(a \ne b\). If \(G - v + ab\) contains \(K_{3,3}\), then \(G\) is isomorphic to the graph obtained by subdividing one edge of \(K_{3,3}\).

The graph \(K_1 \vee (K_3 \sqcup K_3)\) is representable in \(\mathbb {R}^3\).

A graph on at most seven vertices and ten edges, containing no \(K_{3,3}\) and having a degree-two vertex, is representable in \(\mathbb {R}^3\).

For every graph on seven vertices, \(|E(G)| + |E(\overline G)| = \binom 72 = 21\): the two edge sets partition the pairs of distinct vertices.

Every finite graph with at most eight edges has a representation in \(\mathbb {R}^3\). Chaffee–Noble, Theorem 6.

Every graph on at most five vertices that contains no \(K_5\) is contained in the fixed graph \(K_5 - e\).

The graph \(K_{1,1,5}\) is representable in \(\mathbb {R}^3\).

The graph \(K_5 - e\), with the deleted edge joining \(3\) and \(4\), has a representation in \(\mathbb {R}^3\): vertices \(0, 1, 2\) form a unit equilateral triangle and \(3, 4\) are the apexes of the two regular tetrahedra on it, which are \(2\sqrt{2/3}\) apart.

A finite graph with at most nine edges and no representation in \(\mathbb {R}^3\) contains an ordinary copy of \(K_{3,3}\). With Lemma 7 this says \(K_{3,3}\), with nine edges, is the smallest graph without a representation in \(\mathbb {R}^3\).

The octahedron on the opposite pairs \(01, 23, 45\) is representable in \(\mathbb {R}^3\).

The complement of \(P_6\) is representable in \(\mathbb {R}^3\).

The complement of \(C_6\) is representable in \(\mathbb {R}^2\): the triangular prism is planar.

A vertex of degree at most two can be restored in \(\mathbb {R}^3\) to a representation of its deletion, provided that when it has two neighbours they have been placed one unit apart: with one neighbour the new point lies on the unit sphere about it, and with two the unit spheres about the neighbours meet in a circle, which avoids the finitely many points already used.

A graph on six vertices with at most ten edges, minimum degree at least three, and no \(K_{3,3}\) is representable in \(\mathbb {R}^3\).

The frozen statement’s representation predicate is equivalent to the shared library’s UnitDistEmbeddable: both quantify an injective placement of the vertices in the \(d\)-dimensional Euclidean space \(\mathbb {R}^d\) sending every edge to distance one, leaving non-edges unconstrained. The equivalence holds by Iff.rfl.

Subdividing one edge of \(K_{3,3}\) gives a graph representable in \(\mathbb {R}^3\).

Representations pull back along injective graph homomorphisms, so a subgraph of a graph with a representation has one, representations transport along isomorphisms, and a representation in \(\mathbb {R}^n\) gives one in \(\mathbb {R}^m\) for \(n \le m\) by appending zero coordinates.

A two-regular graph on six vertices is isomorphic to the six-cycle \(C_6\) or to the disjoint union of two triangles \(K_3 \sqcup K_3\).

The wheel with five rim vertices is representable in \(\mathbb {R}^3\).

The frozen instance \(d = 3\) of Conjecture 2 holds: every simple graph on seven vertices, or its complement, has a unit-distance representation in \(\mathbb {R}^3\). This is \(f_D(7) \le 3\). With the lower bound \(f_D(7) \ge 3\) of Frankl, Kupavskii and Swanepoel (2020, Theorem 4), which is not formalized here, it gives \(f_D(7) = 3\).

Every graph on seven vertices, or its complement, has a unit-distance representation in \(\mathbb {R}^3\).

Every finite graph on at most seven vertices and at most ten edges that contains neither \(K_5\) nor \(K_{3,3}\) is representable in \(\mathbb {R}^3\).