1 Dimension five graphs with fifteen edges
1.1 Definitions
A graph \(G\) is representable in \(\mathbb {R}^n\) when there is an injective \(f : V(G) \to \mathbb {R}^n\) with \(\lVert f(u) - f(v)\rVert = 1\) for every edge \(uv\). Non-adjacent vertices are unconstrained. The statement’s inlined definition and the library’s agree by Iff.rfl.
\(\dim (G) = n\) when \(n\) is least such that \(G\) is representable in \(\mathbb {R}^n\).
1.2 From the library
A representation in \(\mathbb {R}^n\) gives one in \(\mathbb {R}^m\) for \(m \ge n\), and restricts along graph homomorphisms and to subgraphs. (Corollary 5, \(\dim H \le \dim G\) for a spanning subgraph, is the library’s dim_le_of_le_compl; this proof does not need it.)
If the neighbours of \(u\) form a clique of size \(k\) with \(k + 1 \le d\), and \(G - u\) is representable in \(\mathbb {R}^d\), then so is \(G\). The points at distance one from a unit regular simplex with \(k + 1 \le d\) vertices form an infinite set, so \(u\) avoids the finitely many placed points.
At most \(d + 1\) points of \(\mathbb {R}^d\) are pairwise at distance one, and scaled basis vectors place \(K_n\) in \(\mathbb {R}^{n-1}\).
For \(n \ge 3\): two apexes over the remaining \(n - 2\) vertices for the upper bound, and \(K_{n-1} \le K_n - e\) for the lower.
Rung 1’s orthogonal-complement argument.
1.3 Theorem 8: \(\dim K_{1,3,3} = 5\)
\(K_{1,3,3}\) has no representation in \(\mathbb {R}^4\) and has one in \(\mathbb {R}^5\). The lower bound is a self-contained orthogonal-complement count in place of the paper’s circumcentre argument; the upper bound is an explicit placement, not the paper’s inclusion in \(K_7 - e\).
1.4 Lemma 9: the cocktail-party graphs
\(K_{1,2,2,2}\) and \(K_{2,2,2,2}\) have dimension four: cross-polytope placements \(\pm \tfrac {\sqrt2}{2} e_i\), and a \(K_{3,3}\) homomorphism for the lower bound. The \(K_{3,3}\) is not induced, so the lower bound goes through a homomorphism, not an embedding.
1.5 Theorem 10: at most fourteen edges is representable in \(\mathbb {R}^4\)
A two-regular graph on seven vertices has three pairwise disjoint edges, since its components are cycles of length at least three. So the complement of a \(4\)-regular graph on seven vertices has three pairwise disjoint edges.
Every finite graph with at most fourteen edges is representable in \(\mathbb {R}^4\).
By induction on the number of vertices.
A vertex of degree at most three reduces. Delete it and join its neighbours pairwise: at most as many edges and fewer vertices, so the smaller graph is representable, and Lemma 4 re-attaches the vertex to that supergraph.
Otherwise the minimum degree is at least four, so \(4|V| \le 28\) and \(|V| \le 7\).
\(|V| \le 5\): the graph is a subgraph of \(K_5\).
\(|V| = 6\): it misses an edge of \(K_6\), so it is a subgraph of \(K_6 - e\).
\(|V| = 7\): it is \(4\)-regular with fourteen edges. Its complement has three disjoint edges (Lemma 10), so it maps into \(K_{1,2,2,2}\).
1.6 The targets
\(K_6\) and \(K_{1,3,3}\) each have dimension five and fifteen edges. No uniqueness is claimed.
The least number of edges of a graph of dimension five is fifteen. \(K_6\) attains fifteen, and a graph with at most fourteen edges is representable in \(\mathbb {R}^4\), so it does not have dimension five.