diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md
index a921346..f5a19ff 100644
--- a/book/src/SUMMARY.md
+++ b/book/src/SUMMARY.md
@@ -17,6 +17,7 @@
     - [Lookup argument](design/proving-system/lookup-argument.md)
     - [Permutation argument](design/proving-system/permutation.md)
     - [Circuit commitments](design/proving-system/circuit-commitments.md)
+    - [Vanishing argument](design/proving-system/vanishing.md)
     - [Multipoint opening argument](design/proving-system/multipoint-opening.md)
     - [Comparison to other work](design/proving-system/comparison.md)
   - [Implementation](design/implementation.md)
diff --git a/book/src/design/proving-system/vanishing.md b/book/src/design/proving-system/vanishing.md
new file mode 100644
index 0000000..51922ce
--- /dev/null
+++ b/book/src/design/proving-system/vanishing.md
@@ -0,0 +1,79 @@
+# Vanishing argument
+
+Having committed to the circuit assignments, the prover now needs to demonstrate that the
+various circuit relations are satisfied:
+
+- The custom gates, represented by polynomials $\text{gate}_i(X)$.
+- The rules of the lookup arguments.
+- The rules of the equality constraint permutations.
+
+Each of these relations is inherently represented as a polynomial of degree $d$ (the
+maximum degree of any of the relations). Given that the degree of the assignment
+polynomials (over which these relations are built) is $n - 1$, the full polynomial
+representing each relation has degree $d(n - 1)$.
+
+> In our [example](../proving-system.md#example), these would be the gate polynomials, of
+> degree $3n - 3$:
+>
+> - $\text{gate}_0(X) = a_0(X) \cdot a_1(X) \cdot a_2(X \omega^{-1}) - a_3(X)$
+> - $\text{gate}_1(X) = f_0(X \omega^{-1}) \cdot a_2(X)$
+> - $\text{gate}_2(X) = f_0(X) \cdot a_3(X) \cdot a_0(X)$
+
+A relation is satisfied if its polynomial is equal to zero. One way to demonstrate this is
+to divide each polynomial relation by the vanishing polynomial $t(X) = (X^n - 1)$, which
+is the lowest-degree monomial that has roots at every $\omega^i$. If relation's polynomial
+is perfectly divisible by $t(X)$, it is equal to zero over the domain (as desired).
+
+This simple construction would require a polynomial commitment per relation. Instead, we
+commit to all of the circuit relations simultaneously: the verifier samples $y$, and then
+the prover constructs the quotient polynomial
+
+$$h(X) = \frac{\text{gate}_0(X) + y \cdot \text{gate}_1(X) + \dots + y^i \cdot \text{gate}_i(X) + \dots}{t(X)},$$
+
+where the numerator is a random (the prover commits to the cell assignments before the
+verifier samples $y$) linear combination of the circuit relations.
+
+- If the numerator polynomial (in formal indeterminate $X$) is perfectly divisible by
+  $t(X)$, then with high probability all relations are satisfied.
+- Conversely, if at least one relation is not satisfied, then with high probability
+  $h(x) \cdot t(x)$ will not equal the evaluation of the numerator at $x$. In this case,
+  the numerator polynomial would not be perfectly divisible by $t(X)$.
+
+## Committing to $h(X)$
+
+$h(X)$ has degree $(d - 1)n - d$ (because the divisor $t(X)$ has degree $n$). However, the
+polynomial commitment scheme we use for Halo 2 only supports committing to polynomials of
+degree $n - 1$ (which is the maximum degree that the rest of the protocol needs to commit
+to). Instead of increasing the cost of the polynomial commitment scheme, the prover split
+$h(X)$ into pieces of degree $n - 1$
+
+$$h_0(X) + X^n h_1(X) + \dots + X^{n(d-1)} h_{d-1}(X),$$
+
+and produces blinding commitments to each piece
+
+$$\mathbf{H} = [\text{Commit}(h_0(X)), \text{Commit}(h_1(X)), \dots, \text{Commit}(h_{d-1}(X))].$$
+
+## Evaluating the polynomials
+
+At this point, all properties of the circuit have been committed to. The verifier now
+wants to see if the prover committed to the correct $h(X)$ polynomial. The verifier
+samples $x$, and the prover produces the purported evaluations of the various polynomials
+at $x$, for all the relative offsets used in the circuit, as well as $h(X)$.
+
+> In our [example](../proving-system.md#example), this would be:
+>
+> - $a_0(x)$
+> - $a_1(x)$
+> - $a_2(x)$, $a_2(x \omega^{-1})$
+> - $a_3(x)$
+> - $f_0(x)$, $f_0(x \omega^{-1})$
+> - $h_0(x)$, ..., $h_{d-1}(x)$
+
+The verifier checks that these evaluations satisfy the form of $h(X)$:
+
+$$\frac{\text{gate}_0(x) + \dots + y^i \cdot \text{gate}_i(x) + \dots}{t(x)} = h_0(x) + \dots + x^{n(d-1)} h_{d-1}(x)$$
+
+Now content that the evaluations collectively satisfy the gate constraints, the verifier
+needs to check that the evaluations themselves are consistent with the original
+[circuit commitments](circuit-commitments.md), as well as $\mathbf{H}$. To implement this
+efficiently, we use a [multipoint opening argument](multipoint-opening.md).