A subgraph of a graph realizable in \(\mathbb {R}^n\) is realizable in \(\mathbb {R}^n\), and so is an injective homomorphic preimage: the placement transports along graph homomorphisms, embeddings, and isomorphisms.

At most \(d + 1\) points of \(\mathbb {R}^d\) are pairwise at distance one, so \(K_{d+2}\) has no realization in \(\mathbb {R}^d\). FKS Lemma 14, first half; the introduction (l. 85) calls it clear. This is what makes Theorem 30 say \(f(d) = \binom {d+2}{2}\).

For \(\lvert x\rvert = \lvert y\rvert = 1/\sqrt2\), one has \(\lvert x - y\rvert = 1\) if and only if \(\langle x, y\rangle = 0\). A placement on \(\mathbb {S}^{d-1}\) is in particular a realization in \(\mathbb {R}^d\).

If \(G_1\) is on the sphere of a subspace \(W_1\) and \(G_2\) on the sphere of \(W_2 \perp W_1\), then the join \(G_1 + G_2\), and so every graph on \(V_1 \sqcup V_2\) whose restrictions are \(G_1\) and \(G_2\), is on the sphere of \(W_1 \oplus W_2\). The poles below and Proposition 14 are instances.

If \(G - v - w\) is on \(\mathbb {S}^{d-2}\) and \(vw\) is not an edge, then \(G\) is on \(\mathbb {S}^{d-1}\): the section sits in a hyperplane, and \(v, w\) go to its two poles, which are orthogonal to the section and \(\sqrt2\) apart. The one-vertex version, for any vertex, is the same. FKS l. 384–394.

Let \(d \ge 2\). If \(x\) has degree at most \(d - 2\) and \(G - x\) is on \(\mathbb {S}^{d-1}\), then so is \(G\). The orthogonal complement of the neighbours’ span has dimension at least two, so it meets the sphere in an infinite set, which avoids the finitely many placed points. FKS l. 317–323.

Repeatedly delete a vertex of degree at most \(d - 2\). The result \(H\), the \((d-1)\)-core, is an induced subgraph of minimum degree at least \(d - 1\) (possibly empty) and does not depend on the order: it is the maximal vertex set all of whose vertices have more than \(d - 2\) neighbours inside it. The deleted vertices come with an order in which each has at most \(d - 2\) neighbours among \(H\) and the later-deleted vertices, and deleting \(v\), or the pair \(v, w\), accounts for exactly the edges meeting the deleted vertices.

If \(k \le d\) and the complement of \(H\), a graph on \(d + k\) vertices, has \(k\) disjoint edges, then \(H\) is on \(\mathbb {S}^{d-1}\): the \(i\)-th pair goes to \(\pm e_i/\sqrt2\), the other vertices to the unused \(e_j\). The written proof treats only \(k = d\) (l. 335); the uses below are \(k \le 3\).

If \(\Delta (G) \le k_1 + k_2 + 1\), the vertices split into \(V_1 \sqcup V_2\) with \(\Delta (G[V_i]) \le k_i\). Take a split minimising \((k_2+1)\, e(V_1) + (k_1+1)\, e(V_2)\): a vertex \(u \in V_1\) with \(\deg _{V_1} u \ge k_1 + 1\) has \(\deg _{V_2} u \le k_2\), and moving it lowers the sum. FKS state the general \(\alpha \)-version (l. 115); only \(\alpha = 2\) is used.

A graph of maximum degree one is on \(\mathbb {S}^1\); a graph of maximum degree two is on \(\mathbb {S}^2\). FKS call both easy (l. 123). The second is a real leaf: its components are paths and cycles, and a cycle does not in general close on a single great circle, so each cycle gets its own orthogonal placement in \(\mathbb {R}^3\) — an umbrella for odd length, a zigzag for even — and the arbitrary azimuthal offset rotates the components apart.

On \(d + 2\) vertices with a fixed pair \(\{ a, b\} \), every graph without the edge \(ab\) is realizable in \(\mathbb {R}^d\): two unit regular \(d\)-simplices sharing a facet, with apexes \(a\) and \(b\) at distance \(\sqrt{2 + 2/d} {\lt} 2\). That is the diameter; every other pair is at distance one. FKS l. 355–356.

Let \(d \ge 3\) and fix a placement in which all placed pairs are less than \(2\) apart, such as Lemma 15’s. A graph that adds new vertices and at most \(t\) edges, each meeting a new vertex, is realizable extending that placement.

• \(t \le 2\) is rung 3’s case (FKS l. 358–359): every new vertex has degree at most two, and two placed neighbours are less than \(2\) apart, so the unit spheres about them meet in a \((d-2)\)-sphere.

• \(t = 3\) is Lemma T, for rung 4, with \(d \ge 4\). The library proves it (UnitDistEmbeddable.extend_tail_three); only rung 4 uses it.

Let \(d \ge 4\), \(\lvert a - b\rvert ^2 = 2 + 2/d\), and \(\lvert a - c\rvert = \lvert b - c\rvert = 1\). The points at distance one from \(a\), \(b\) and \(c\) form an infinite set: the triangle’s squared circumradius is \(1/(4 - \lvert a-b\rvert ^2) = d/(2(d-1)) {\lt} 1\). The other triples of Lemma 15 are equilateral and are covered by infinite_sphere_inter_of_regular_simplex. Proved in the library as EuclideanGeometry.infinite_common_unit_sphere_two_apices (\(d \ge 4\)); only rung 4 uses it, so it lies outside this project’s import closure.

The sketch’s general form (pairwise distances at most \(D\), \(D^2 {\lt} 3\), implies circumradius below one) is false: \((-\tfrac 34, 0), (\tfrac 34, 0), (0, \tfrac 1{10})\) has circumradius \(229/80\). Finding A36.

Let \(e_1, \dots , e_d\) be pairwise orthogonal with \(\lvert e_i\rvert = 1/\sqrt2\). The point \(x = 2c \sum e_i\) with \(4dc^2 - 4c - 1 = 0\) is at distance one from every \(e_i\), and \(\lvert x\rvert ^2 = 2dc^2 \ne 1/2\), so \(x\) is off \(\mathbb {S}^{d-1}\) and differs from every point placed on it. FKS l. 368–369.

Let \(K\) be a unit regular \(d\)-simplex in \(\mathbb {R}^d\). New vertices, pairwise non-adjacent, each joined to a set of at most \(d - 1\) vertices of \(K\) (possibly empty; the sets may overlap), attach injectively. Each solution set is a sphere of dimension \(d - s \ge 1\) about the sub-simplex’s circumcentre (A37). The library’s infinite_sphere_inter_of_regular_simplex is the core, and its packaged form UnitDistEmbeddable.extend_of_clique_neighbors serves rung 4 only.

At most three edges: realizable in \(\mathbb {R}^2\). If it also avoids \(K_3\) and \(K_{1,3} = K_4 - K_3\), its components are paths of at most three edges and isolated vertices, placed on the circle \(\mathbb {S}^1\) with quarter turns and rotated apart. FKS: easy to verify.

Assume \(b \le m(d)\) and \(b {\lt} m(d) + d - 4\). Then \(H\) has exactly the \(d + 2\) vertices of that subgraph, since one more core vertex brings at least \(d - 1\) further edges. Then either \(H = K_{d+2}\), or \(H\) misses \(s \in \{ 1, 2, 3\} \) triangle edges, \(H\) is placed by Lemma 15, and the tail \(t\) satisfies \(t + m(d) \le b + s\) (stated additively; natural subtraction is wrong here, A37). At \(b = g(d)\), \(t \le s - 1 \le 2\). Lemma 16 attaches it, extending the fixed placement, so the lemma returns the placement map, not only the existence of one. FKS l. 352–359.

If \(b {\lt} m(d) + d - 4\), then \(H = K_{d+1}\): two core vertices outside the clique overshoot, and one would give \(K_{d+2} - K_3\). At most \(b - \binom {d+1}{2}\) edges meet the pruned vertices.

• If some \(v \in H\) has no pruned neighbour, \(H - v = K_d\) goes on the sphere as a scaled orthonormal basis, Corollary 10 re-attaches the pruned vertices, and \(v\) goes to the point of Lemma 18. At \(b \le g(d)\) there are at most \(d\) cross edges, so such a \(v\) exists (FKS l. 363–369).

• Otherwise, at \(b = m(d)\), there are exactly \(d + 1\) cross edges and no other edges outside \(H\), each clique vertex meets exactly one pruned vertex, and every pruned vertex has at most \(d - 2\) neighbours, all in \(H\). Lemma 19 places them. Rung 4 only.

If \(H\) avoids \(K_{d+1}\) and \(K_{d+2} - K_3\) and has at most \(d + 2\) vertices, then \(H\) is on \(\mathbb {S}^{d-1}\) by Lemma 11 with \(k \le 2\). On \(d + 2\) vertices, the complement has maximum degree at most two, and if it had no two disjoint edges its edges would lie in a triangle. No budget is used. FKS l. 373–380.

Assume \(S(d-1)\), \(b - (d + 2) \le g(d-1)\), and that \(H\) avoids \(K_{d+1}\) and \(K_{d+2} - K_3\), has at least \(d + 3\) vertices, and has a vertex \(v\) adjacent to all the others. Then \(H - v\) avoids \(K_d\) and \(K_{d+1} - K_3\), \(S(d-1)\) puts it on \(\mathbb {S}^{d-2}\), and \(v\) goes to a pole. The budget condition holds at \(b = g(d)\) for every \(d \ge 3\), and at \(b = m(d)\) with slack zero for \(d \ge 5\); at \(d = 4\) it fails, which is where \(K_{3,3,1}\) lives. FKS l. 384–387.

Assume \(S(d-1)\) and \(b - (2d - 1) \le g(d-1)\), and that \(H\) avoids \(K_{d+1}\) and \(K_{d+2} - K_3\), has at least \(d + 3\) vertices, and no vertex of maximum degree is universal. If \(\Delta (H) \le d - 1\), Proposition 14 places \(H\). Otherwise, for a vertex \(v\) of maximum degree and a non-neighbour \(w \ne v\), \(H - v - w\) has at most \(g(d-1)\) edges. If it avoids \(K_d\) and \(K_{d+1} - K_3\), \(S(d-1)\) and Lemma 7 place \(H\). FKS l. 388–391.

Assume \(b {\lt} m(d) + d - 4\), and the hypotheses in force at this point: \(H\) avoids \(K_{d+1}\), has at least \(d + 3\) vertices and minimum degree at least \(d - 1\), \(\Delta (H) \ge d\), and each maximum-degree vertex has a non-neighbour \(w \ne v\). Then the core cannot be such that, for every maximum-degree \(v\) and non-neighbour \(w\), \(H - v - w\) contains a \(d\)-clique: some non-neighbour of \(v\) leaves a \(d\)-clique-free deletion. Two \(d\)-cliques meeting in at most \(d - 2\) vertices overshoot by the count \(d + m(d) - 4\); meeting in \(d - 1\), a further vertex \(y\) overshoots by \(\binom {d+1}{2} + 2d - 3\). Pure counting. FKS l. 395–401.

If \(v\) has maximum degree \(\Delta \ge d\) and a non-neighbour \(w\) with \(H - v - w \supseteq K_{d+1} - K_3\), then \(\lvert E(H)\rvert \ge \binom {d+1}{2} - 3 + \Delta + (d - 1)\), which is \(m(d) + d - 5\) at \(\Delta = d\). So Case 2 does not occur when \(b {\lt} m(d) + d - 5\): at \(b = g(d)\) for \(d \ge 5\), and at \(b = m(d)\) for \(d \ge 6\). At equality, \(H - v - w = K_{d+1} - K_3\), \(\Delta = d\), and \(\deg w = d - 1\); the library records the sharp form: under the budget \(g(d)\) the configuration persists only for \(d \le 4\), with both deleted degrees and the remaining edge count at their lower bounds. FKS l. 404–406.

In the equality configuration of Lemma 27, \(H\) is on \(\mathbb {S}^{d-1}\). Either the components of \(H[v, w, v_1, v_2, v_3]\) are paths of at most three edges, placed on a great circle with the remaining \(K_{d-2}\) on the orthogonal subsphere; or there are three disjoint non-edges and Lemma 11 applies with \(k = 3\). Rung 3 needs it only at \(d = 3\) and \(d = 4\), where \(b = g(d)\) meets the count exactly. Rung 4 at \(d \ge 6\) never needs it. FKS l. 406–412; the pair choice is written out in the Stage 0 sketch.

This is the one place the published proof needed a repair. FKS read the equality count (l. 404–406) as forcing \(H - v - w = K_{d+1} - K_3\), \(\deg v = d\), \(\deg w = d - 1\), and hence \(\lvert V(H)\rvert = d + 3\). At \(d = 3\) that deduction is false: a vertex joined only to \(v\) and \(w\) has degree \(2 = d - 1\) and survives the pruning, and the library records a seven-vertex counterexample (SimpleGraph.exists_fks_case_two_extra_vertex, Math finding A38). The theorem is unaffected. At \(d = 3\) the equality configuration makes \(H - v - w\) a star \(K_{1,3}\) plus isolated vertices; the star’s centre \(c\) has degree \(3 = \Delta \) and is not adjacent to \(v\), and \(H - c - v\) has only two edges, so \(S(2)\) and the poles place \(H\) — a contradiction, and Case 2 cannot arise at \(d = 3\). At \(d \ge 4\) an extra vertex would need \(d - 1 \ge 3\) neighbours among \(\{ v, w\} \), so the deduction holds. The bridge SphereEmbeddable.of_fks_case_two (Extremal/FKS/CaseTwoBridge.lean) implements this repair, and it is the form the step below uses.

For \(d \ge 3\), \(S(d-1)\) implies \(S(d)\). Take \(H\) to be the maximal core. If it is empty, Corollary 10 places \(G\); if it is on the sphere, Corollary 10 re-attaches the rest. If \(H\) contains \(K_{d+2} - K_3\), Branch A applies; if it contains \(K_{d+1}\), Branch B; otherwise the spherical dispatch runs Branch C small, then Proposition 14, then the universal-vertex and two-pole branches, with Case 1 excluded by Lemma 26 and Case 2 placed through the repaired bridge of Lemma 28. The Euclidean half in Branches A and B, where \(G\) does not avoid \(K_{d+1}\) or \(K_{d+2} - K_3\), uses the fact that \(K_{d+2}\) has \(m(d) {\gt} g(d)\) edges. Arithmetic facts used: \(g(d) - (d + 2) \le g(d-1)\) and \(g(d) - (2d - 1) \le g(d-1)\) for \(d \ge 3\), and \(g(d) {\lt} m(d) + d - 4\) for \(d \ge 3\). The induction is a two-parameter recursion, over \(d\) and over the core, so this node only dispatches cases.