5 Henneberg moves
This section studies two ways of adding a vertex to a graph, the Henneberg moves. The Type I move adds a vertex of degree two. The Type II move deletes an edge \(ab\) and adds a vertex of degree three, joined to \(a\), \(b\) and a third vertex. The Laman graphs are exactly the graphs that can be built from \(K_2\) by these moves, a characterization due to Henneberg [ Hen11 ] , Pollaczek-Geiringer [ PG27 ] (§7, pp. 69–70) and Laman [ Lam70 ] . Jordán [ Jor16 ] proves it as Theorem 2.2.8, for minimally rigid graphs, which are the Laman graphs (section 4).
Each half of this characterization follows by induction on the number of vertices, and we prove the two inductive steps. After the definitions and a count of the edges that each move adds, we show that the moves preserve the Laman property. The other step is the reverse decomposition (theorem 5.12): every Laman graph on at least three vertices has a vertex \(v\) of degree two or three such that deleting \(v\), and in degree three joining two of its neighbours by an edge, leaves a Laman graph. The proof that every Laman graph is generically rigid in the plane (theorem 9.2) is an induction with this step. The section ends with an example.
Throughout, \(G\) is a graph on a vertex set \(V\), which is finite where a statement says so. We write \(ab\) for the edge with endpoints \(a\) and \(b\), and \(v\) for the vertex that a move adds, so that the graph the move produces has vertex set \(V \cup \{ v\} \).
5.1 Definitions
In Jordán’s survey [ Jor16 ] (§1.2.1, p. 38) the two moves are the \(0\)-extension and the \(1\)-extension in the plane, also called Henneberg moves of type I and type II.
Let \(a, b \in V\). The Type I move at \(a\) and \(b\) adds to \(G\) a new vertex \(v\) and the edges \(va\) and \(vb\).
Let \(a, b, c \in V\). The Type II move on \(ab\) and \(c\) deletes the edge \(ab\) from \(G\) if it is present, and adds a new vertex \(v\) and the edges \(va\), \(vb\) and \(vc\).
Both moves are formalized as graphs on \(\mathrm{Option}\, V\), which has an element \(\mathrm{some}\, u\) for each \(u \in V\) and one further element \(\mathrm{none}\). The new vertex \(v\) is \(\mathrm{none}\), and each vertex \(u\) of \(G\) becomes \(\mathrm{some}\, u\). This is the standard way in mathlib to adjoin one element, and it makes \(v\) new by construction, so no statement needs a hypothesis saying so. The formal statements about a move, here and in later sections, compare a graph on \(V\) with a graph on \(\mathrm{Option}\, V\) through the map \(u \mapsto \mathrm{some}\, u\), and the text identifies each \(u\) with its image.
The definitions allow any vertices \(a\), \(b\) and \(c\), but we use the moves only under Jordán’s conditions (p. 44). For the Type I move at \(a\) and \(b\) we assume \(a \ne b\), so that \(v\) has degree two; if \(a = b\), the move adds the single edge \(va\). For the Type II move on \(ab\) and \(c\) we assume that \(ab\) is an edge of \(G\) and that \(c\) is neither \(a\) nor \(b\), so that \(v\) has degree three and the number of edges grows by two.
5.2 Edge sets and edge counts
We describe the edge set of the graph that each move produces, and count it. We use the counts to verify the equation \(|E| + 3 = 2|V|\) of a Laman graph in the preservation theorems below and in the reverse decomposition.
Let \(a, b \in V\), let \(G'\) be obtained from \(G\) by the Type I move at \(a\) and \(b\), and let \(v\) be its new vertex. Then
An edge of \(G'\) either contains \(v\) or joins two vertices of \(G\). By definition 5.1, the edges of \(G'\) at \(v\) are \(va\) and \(vb\), and two vertices of \(G\) are adjacent in \(G'\) exactly when they are adjacent in \(G\).
Let \(V\) be finite, let \(a \ne b\) be vertices of \(G\), and let \(G'\) be obtained from \(G\) by the Type I move at \(a\) and \(b\). Then
The two sets on the right of lemma 5.4 are disjoint, since the edges \(va\) and \(vb\) contain the new vertex \(v\) and the edges of \(G\) do not. The edges \(va\) and \(vb\) are distinct because \(a \ne b\).
Let \(a, b, c \in V\), let \(G'\) be obtained from \(G\) by the Type II move on \(ab\) and \(c\), and let \(v\) be its new vertex. Then
As in the proof of lemma 5.4, an edge of \(G'\) either contains \(v\) or joins two vertices of \(G\). By definition 5.2, the edges of \(G'\) at \(v\) are \(va\), \(vb\) and \(vc\), and two vertices of \(G\) are adjacent in \(G'\) exactly when they are adjacent in \(G\) and are not \(a\) and \(b\).
Let \(V\) be finite, let \(a\), \(b\) and \(c\) be distinct vertices of \(G\), and let \(G'\) be obtained from \(G\) by the Type II move on \(ab\) and \(c\). Then
When \(ab\) is an edge of \(G\), as in the preservation theorems, the right-hand side is \(|E(G)| + 2\).
5.3 Preservation of the Laman property
We show that both moves preserve the Laman property, and that the Type I move also reflects it. Jordán [ Jor16 ] proves the sparsity part of these facts as Lemmas 2.1.5 and 2.1.4(a), where the two moves are called the \(0\)-extension and the \(1\)-extension.
Let \(G\) be a Laman graph and let \(a \ne b\) be vertices of \(G\). Let \(G'\) be obtained from \(G\) by the Type I move at \(a\) and \(b\). Then \(G'\) is Laman.
Let \(v\) be the new vertex of \(G'\). The graph \(G'\) has one more vertex than \(G\) and two more edges (lemma 5.5), so \(|E(G')| + 3 = 2|V(G')|\) follows from \(|E(G)| + 3 = 2|V(G)|\).
For \((2,3)\)-sparsity (definition 3.1) we show that every set \(X\) of at least two vertices of \(G'\) spans at most \(2|X| - 3\) edges. Let \(X_0 = X \setminus \{ v\} \). The edges of \(G'\) inside \(X\) are the edges of \(G\) inside \(X_0\), together with those of the new edges \(va\) and \(vb\) that lie inside \(X\). If \(v \notin X\), then \(X = X_0\), and the bound holds because \(G\) is sparse. Otherwise \(|X| = |X_0| + 1\). If \(|X_0| = 1\), then \(X_0\) spans no edge and at most one new edge lies inside \(X\), so \(X\) spans at most \(1 = 2|X| - 3\) edges. If \(|X_0| \ge 2\), then
Let \(G\) be a Laman graph, let \(ab\) be an edge of \(G\), and let \(c \ne a, b\) be a vertex of \(G\). Let \(G'\) be obtained from \(G\) by the Type II move on \(ab\) and \(c\). Then \(G'\) is Laman.
Let \(v\) be the new vertex of \(G'\). The move deletes \(ab\) and adds \(va\), \(vb\) and \(vc\), so \(G'\) has one more vertex than \(G\) and two more edges (lemma 5.7). The count follows as in theorem 5.8.
For sparsity, let \(X\) and \(X_0\) be as in the proof of theorem 5.8. The edges of \(G'\) inside \(X\) are the edges of \(G\) inside \(X_0\) other than \(ab\), together with those of \(va\), \(vb\) and \(vc\) that lie inside \(X\). The cases \(v \notin X\) and \(|X_0| = 1\) go as before. Suppose that \(v \in X\) and \(|X_0| \ge 2\). If \(a\) and \(b\) both lie in \(X_0\), then \(ab\) is an edge of \(G\) inside \(X_0\) that \(G'\) does not have, and at most three new edges lie inside \(X\). Otherwise one of \(va\) and \(vb\) does not lie inside \(X\), so at most two new edges do. In both cases \(|E_{G'}[X]| \le |E_{G}[X_0]| + 2 \le 2|X| - 3\).
The reverse decomposition (section 5.4) needs the converse of theorem 5.8, to show that removing a vertex of degree two from a Laman graph leaves a Laman graph.
Let \(G\) be a finite graph and let \(a \ne b\) be vertices of \(G\). Let \(G'\) be obtained from \(G\) by the Type I move at \(a\) and \(b\). If \(G'\) is Laman, then \(G\) is Laman.
Let \(v\) be the new vertex of \(G'\). Both new edges contain \(v\), so a set of vertices of \(G\) spans the same edges in \(G'\) as in \(G\). Hence \(G\) is \((2,3)\)-sparse because \(G'\) is. The count follows from lemma 5.5, as in theorem 5.8.
Let \(G\) be a finite graph and let \(a \ne b\) be vertices of \(G\). Let \(G'\) be obtained from \(G\) by the Type I move at \(a\) and \(b\). Then \(G'\) is Laman if and only if \(G\) is Laman.
Combine theorem 5.8 and theorem 5.10.
5.4 Reverse decomposition
Let \(v\) be a vertex of \(G\). We write \(G - v\) for the graph on \(V \setminus \{ v\} \) obtained from \(G\) by deleting \(v\), and, for vertices \(a, b \ne v\), we write \(G - v + ab\) for the graph obtained from \(G - v\) by adding the edge \(ab\), as in section 3.6. Deleting \(v\) reverses a move. If \(v\) has degree two, with neighbours \(a\) and \(b\), then the Type I move at \(a\) and \(b\) applied to \(G - v\) gives a copy of \(G\). If \(v\) has degree three, with neighbours \(a\), \(b\) and \(c\), where \(a\) and \(b\) are not adjacent, then the Type II move on \(ab\) and \(c\) applied to \(G - v + ab\) gives a copy of \(G\). The theorem below finds a vertex at which the smaller graph is again Laman.
Most of the work is in the same statement for \((2,3)\)-sparse graphs, theorem 3.19, in which \(v\) may also have degree one. A sparse graph with an edge has a vertex \(v\) of degree one, two or three, and Jordán’s Lemma 2.1.4 [ Jor16 ] treats the last two cases. If \(v\) has degree two, then \(G - v\) is sparse. If \(v\) has degree three, then \(v\) has a suitable splitting (section 3.6): two neighbours \(a\) and \(b\) of \(v\) that are not adjacent and make \(G - v + ab\) sparse. We proved the sparse statement in section 3.7. It is also the inductive step in the proof that the edge set of every \((2,3)\)-sparse graph is independent in the rigidity matroid (section 10).
Let \(V\) be finite with \(|V| \ge 3\), and let \(G\) be a Laman graph on \(V\). Then \(G\) has a vertex \(v\) for which one of the following holds.
The vertex \(v\) has degree two, with neighbours \(a\) and \(b\), and \(G - v\) is Laman.
The vertex \(v\) has degree three, with neighbours \(a\), \(b\) and \(c\), where \(a\) and \(b\) are not adjacent, and \(G - v + ab\) is Laman.
Here \(G - v\) is the graph on \(V \setminus \{ v\} \) obtained from \(G\) by deleting \(v\), and \(G - v + ab\) is obtained from \(G - v\) by adding the edge \(ab\).
Since \(G\) is Laman and \(|V| \ge 3\), it is \((2,3)\)-sparse and has \(2|V| - 3 \ge 3\) edges. So theorem 3.19 gives a vertex \(v\) of degree one, two or three. Every vertex of \(G\) has degree at least two (lemma 4.5), so \(v\) has degree two or three.
Suppose that \(v\) has degree two, with neighbours \(a\) and \(b\). Then \(G\) is isomorphic to the graph obtained from \(G - v\) by the Type I move at \(a\) and \(b\), so that graph is Laman (lemma 4.2). Hence \(G - v\) is Laman by theorem 5.11.
Suppose that \(v\) has degree three. Then the sparse statement gives neighbours \(a\), \(b\) and \(c\) of \(v\), where \(a\) and \(b\) are not adjacent, such that \(H = G - v + ab\) is \((2,3)\)-sparse. The Type II move on \(ab\) and \(c\) deletes from \(H\) the edge \(ab\) that \(H\) adds to \(G - v\), and it adds \(v\) back. So \(G\) is isomorphic to the graph \(H'\) obtained from \(H\) by this move, and \(H'\) is Laman (lemma 4.2). As \(H'\) has \(|V|\) vertices, \(|E(H')| + 3 = 2|V|\). Since \(ab\) is an edge of \(H\), lemma 5.7 gives \(|E(H')| = |E(H)| + 2\). Hence \(|E(H)| + 3 = 2(|V| - 1)\), and \(H\) is Laman.
The formal statement builds \(G - v\) and \(G - v + ab\) on a separate copy of \(V \setminus \{ v\} \), as in formalization note 3.18. The isomorphisms between \(G\) and the moved graphs, in the proof above and in the induction of Laman’s theorem (theorem 9.2), are built from the neighbours of \(v\). Formalization note 10.1 explains why a reverse decomposition describes the smaller graph directly, and not as a graph to which a move is applied.
5.5 An example: \(K_4\) minus an edge
We build \(K_4\) minus an edge from \(K_2\) by two Type I moves.
The graph on \(\{ 0, 1, 2, 3\} \) obtained from the complete graph \(K_4\) by deleting the edge \(23\) is Laman.
The complete graph on \(\{ 0, 1\} \) is Laman (theorem 4.3). The Type I move at \(0\) and \(1\) adds a new vertex \(2\) and the edges \(20\) and \(21\). The result is a triangle, which is Laman by theorem 5.8. A second Type I move at \(0\) and \(1\) adds a new vertex \(3\) and the edges \(30\) and \(31\). The result is Laman by theorem 5.8, and its edges are the pairs from \(\{ 0, 1, 2, 3\} \) other than \(23\).
In the formal proof the two new vertices are not the numbers \(2\) and \(3\) (formalization note 5.3). The graph built is therefore isomorphic to the graph of the statement, by the bijection that sends the first new vertex to \(2\) and the second to \(3\). The Laman property passes along this isomorphism (lemma 4.2).