1 FKS Problem 2 in dimension three
1.1 Notation
“Contains” and “avoids” always refer to ordinary subgraphs, not induced ones. \(K_5 - e\) is the complete graph on five vertices with the edge \(34\) deleted (Lean: \(\texttt{deleteEdges \{ s(3, 4)\} }\)). \(\overline G\) is the complement of \(G\) on the same vertex set. \(f_D(s)\) is the least \(d\) such that every graph on \(s\) vertices, or its complement, has a unit-distance representation in \(\mathbb {R}^d\) (Frankl–Kupavskii–Swanepoel, introduction).
1.2 The question
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).
Every simple graph on \(2d + 1\) vertices, or its complement, has a unit-distance representation in \(\mathbb {R}^d\) — in the source’s wording, has dimension at most \(d\), since \(\mathbb {R}^{d'}\) sits in \(\mathbb {R}^d\) for \(d' \le d\). This is open: Problem 2 of Frankl–Kupavskii–Swanepoel (l. 441), asking whether their lower bound \(\lceil (s - 1)/2 \rceil \le f_D(s)\) is sharp at the odd values \(s = 2d + 1\). The instances \(d = 0\) and \(d = 1\) are elementary and are proved in this repository.
1.3 Existing library dependencies
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 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.
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 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\).
1.4 The eight- and nine-edge theorems
Every finite graph with at most eight edges has a representation in \(\mathbb {R}^3\). Chaffee–Noble, Theorem 6.
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\).
1.5 Concrete graphs and their placements
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.
Subdividing one edge of \(K_{3,3}\) gives a graph representable in \(\mathbb {R}^3\).
With \(s = \sqrt3\), send \(0, 1, 2, 3, 4, 5, 6\) to
The nine cross edges and the two subdivision edges \(06\) and \(36\) have squared length one by direct computation, and the seven points are distinct.
The wheel with five rim vertices is representable in \(\mathbb {R}^3\).
Put the rim on the integer points \((1, 1, 0)\), \((0, 1, 1)\), \((1, 0, 1)\), \((1, -1, 0)\), \((1, 0, -1)\) of the cuboctahedron and the hub at their centre \((0, 0, 0)\), all scaled by \(1/\sqrt2\): every rim edge and every spoke has integer squared distance \(2\), so each scaled edge has length one.
The complement of \(P_6\) is representable in \(\mathbb {R}^3\).
In path order, divide the integer vectors
by \(18\sqrt2\). The six vectors are distinct, and every complement edge has integer squared distance \(648 = (18\sqrt2)^2\), so each scaled edge has length one.
The octahedron on the opposite pairs \(01, 23, 45\) is representable in \(\mathbb {R}^3\).
Put vertex \(2i\) at \(e_i/\sqrt2\) and vertex \(2i + 1\) at \(-e_i/\sqrt2\) on the coordinate axes. Two vertices of different opposite pairs have squared distance \(2/2 = 1\), and each opposite pair is antipodal, so exactly the edges are placed at length one.
The graph \(K_{1,1,5}\) is representable in \(\mathbb {R}^3\).
Put the singleton parts at the poles \((0, 0, \pm \tfrac 12)\), one unit apart, and the five remaining vertices on the equator circle of radius \(\sqrt3/2\) at the rational parameters \(t = 0, \dots , 4\) of the circle \(((1 - t^2)/(1 + t^2),\, 2t/(1 + t^2))\). Each equator point has squared distance \(3/4 + 1/4 = 1\) from both poles, and the five points are distinct. This is the placement required in Lemma 23.
The graph \(K_1 \vee (K_3 \sqcup K_3)\) is representable in \(\mathbb {R}^3\).
Put the hub at the origin and the two triangles on opposite triangle faces of the cuboctahedron — the integer points \((1, 1, 0)\), \((0, 1, 1)\), \((1, 0, 1)\) and their negatives, in planes at heights \(\pm \sqrt{2/3}\) with circumradius \(1/\sqrt3\) — all scaled by \(1/\sqrt2\). Every triangle edge and every spoke to the hub has length one, and the two triangles are placed at different heights. This is the placement required in Lemma 24.
The complement of \(C_6\) is representable in \(\mathbb {R}^2\): the triangular prism is planar.
A unit equilateral triangle and its translate by one unit perpendicular to the triangle give six points whose unit distances are exactly the nine prism edges, the three vertical matching edges included. Chaffee–Noble, Theorem 7.
1.6 Combinatorial reductions
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\).
The complement has five edges and maximum degree at most two, so its components are paths and cycles; with six vertices and five edges exactly one component is a path, counting an isolated vertex as a one-vertex path, and the possible cycle components give the four forms. The library proves this five-edge classification by a finite certificate over the \(2^{15}\) adjacency masks of graphs on six vertices, checked in the kernel; the ten-edge theorem is its complement.
Every graph on at most five vertices that contains no \(K_5\) is contained in the fixed graph \(K_5 - e\).
On fewer than five vertices, inject into four of the five labels, avoiding an endpoint of the deleted edge. On five vertices the graph is not complete, so a missing edge is relabelled onto the deleted pair \(34\).
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 completion \(G - v + ab\) has at most nine edges, so its \(K_{3,3}\) copy exhausts both bounds. The added edge must be absent from \(G - v\), since otherwise \(G\) already contains \(K_{3,3}\). Restoring \(v\) and its two incident edges uses no unused vertex, so \(G\) is the subdivision.
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\).
Delete the vertex \(v\). If its two neighbours are adjacent, the deletion has at most eight edges and Lemma 7 places it, and Lemma 4 restores \(v\). Otherwise complete the deletion by the neighbour edge, giving at most nine edges. If the completion is representable, its placement already puts the two neighbours one unit apart, and Lemma 4 restores \(v\). If it is not, Lemma 8 gives a \(K_{3,3}\) copy in the completion, Lemma 19 identifies \(G\) with the subdivided \(K_{3,3}\), and Lemma 10’s placement transfers along the isomorphism.
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 degree sum forces nine or ten edges. With nine edges the graph is cubic, so its complement is two-regular and Lemma 6 makes it \(C_6\) or \(K_3 \sqcup K_3\); in the first case \(G\) is the triangular prism, placed by Lemma 16, and in the second \(G\) contains \(K_{3,3}\), which is excluded. With ten edges, Lemma 17 gives the four complement forms: the first two place \(G\) above the wheel of Lemma 11 and the path complement of Lemma 12; in the third form \(G\) is contained in the octahedron of Lemma 13; the fourth form makes \(G\) itself contain \(K_{3,3}\), which is excluded.
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\).
Induct on the number of vertices. A vertex of degree zero or one is deleted, the induction hypothesis places the deletion, and Lemma 4 restores it, the two forbidden-copy exclusions persisting under deletion. A vertex of degree exactly two is the case of Lemma 20. Otherwise the minimum degree is at least three, so \(3|V| \le 2|E| \le 20\) and \(|V| \le 6\); seven vertices of minimum degree three are impossible. At most five vertices are covered by Lemma 18 together with the placement of \(K_5 - e\), and six vertices by Lemma 21.
1.7 Complements and the frozen instance
If a graph \(G\) on seven vertices contains \(K_5\), then \(\overline G\) is contained in \(K_{1,1,5}\).
Send the five clique vertices to the part of size five and the two remaining vertices to the singleton parts. Every complement edge meets one of the two vertices outside the clique, and \(K_{1,1,5}\) has all such edges.
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)\).
Send the two sides of the copy to the two triangles and the remaining vertex to the hub. No complement edge joins the two sides of the copy, and the cone has exactly the edges inside the triangles and to the hub.
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 graph on seven vertices, or its complement, has a unit-distance representation in \(\mathbb {R}^3\).
By Lemma 25 one of \(G\) and \(\overline G\), the sparse colour \(H\), has at most ten edges. If \(H\) contains neither \(K_5\) nor \(K_{3,3}\), Theorem 22 places \(H\). If \(H\) contains \(K_5\), Lemma 23 embeds the other colour in \(K_{1,1,5}\), placed by Lemma 14; if \(H\) contains \(K_{3,3}\), Lemma 24 embeds it in the cone over two triangles, placed by Lemma 15. Transfers along the containments by Lemma 3, and the disjuncts are exchanged when the sparse colour is the complement. The library factors the argument through an explicit hypothesis form taking the ten-edge lemma as an assumption, which Theorem 22 then discharges.
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.
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\).