Knot theory · The Lumenary

Lens

MotivationH

Can it be untied?

People have tied knots for as long as there have been ropes. In the Andes, Inca administrators kept census and tax records in khipu, cords whose knot types and positions encoded numbers. Chinese decorative knotting, Celtic interlace and Islamic geometric strapwork turned knots into art, and sailors everywhere developed knots for every task. Inside our cells, enzymes called topoisomerases cut and reseal DNA to undo the knots and links that form when long molecules are copied and packed. Biologists identify the products under the electron microscope by their knot type.

The mathematical question is older than it looks and harder than it sounds. Take a piece of string, tie it in a tangle, and fuse the two ends, so that it can no longer slip off. Is the result really knotted? That is, is there any way to move it around in space, without cutting, so that it becomes a plain round loop? For the simplest knot, the trefoil, everyone is sure the answer is no — but sure is not proof. Wiggling the string for an hour and failing to untie it proves nothing about the next hour. A proof needs a quantity that every allowed motion preserves, and that differs between the trefoil and the plain loop.

A second question is subtler. The trefoil comes in a left-handed and a right-handed version, mirror images of each other. Can one be turned into the other? Max Dehn proved in 1914 that it cannot. This lesson proves both facts, using diagrams, three local moves, and three generations of invariants: colourings (1950s), linking numbers (Gauss, 1833) and the Jones polynomial (1984).

IntuitionH

Pictures of knots, and moves between them

A knot lives in three-dimensional space, but we draw it on paper: a closed curve with crossings, where a small gap in one strand shows that it passes under the other. The same knot has infinitely many diagrams. A round circle and a figure-eight-shaped loop with one crossing are both the unknot. So we need to know when two diagrams show the same knot.

Kurt Reidemeister's answer (1927) is that three local moves suffice:

Move I puts in or takes out a kink: a small loop with one crossing.
Move II slides one strand over another, creating or removing two crossings.
Move III slides a strand over a crossing of two other strands.

Two diagrams show the same knot exactly when one can be turned into the other by these moves (and by wiggling the drawing without changing its crossings). So to prove that two knots are different, it is enough to find a quantity, computed from a diagram, that none of the three moves can change, and that takes different values on the two diagrams. Such a quantity is a knot invariant. Each invariant in this lesson is proved invariant by checking three small pictures.

The three Reidemeister moves, each a change inside a small disc; outside the disc the diagram is untouched. I: a kink appears or disappears. II: one strand slides across another, creating two crossings. III: a strand slides across a crossing of two other strands, passing over both.

DefinitionsH

Knots, diagrams and invariants

Definition— knot, link, equivalence

A knot is a smooth embedding $K : S^1 \to \R^3$ (or into $S^3 = \R^3 \cup \{\infty\}$ ); a link with $m$ components is a smooth embedding of $m$ disjoint circles. Two knots or links are equivalent if there is an ambient isotopy between them: a continuous family of homeomorphisms $h_t : \R^3 \to \R^3$ , $t \in [0, 1]$ , with $h_0 = \mathrm{id}$ and $h_1$ carrying the first onto the second. The unknot is the round circle; a knot equivalent to it is unknotted.

Requiring smoothness (or, equivalently for our purposes, that knots be polygonal — tame) excludes wild knots, with infinitely many smaller and smaller knots tied in them. For wild knots, the theory below fails.

Definition— diagram, Reidemeister moves

A diagram of a knot is a projection to a plane that is injective except at finitely many transverse double points, the crossings, each marked with which strand passes over. Every tame knot has diagrams. The arcs of a diagram are the unbroken strands between undercrossings. The Reidemeister moves I, II, III are the local changes pictured above.

Definition— knot invariant

A knot invariant is a function on knots that takes equal values on equivalent knots. In practice it is computed from a diagram and proved to be unchanged by the three Reidemeister moves. The crossing number $c(K)$ , the least number of crossings in any diagram of $K$ , is an invariant by definition — but it is hard to compute, since one must know about all diagrams.

Definition— Fox colouring, tricolourability

Let $p \ge 3$ be an integer. A Fox $p$ -colouring of a diagram assigns to each arc a colour in $\Z/p$ such that at every crossing, with over-arc coloured $x$ and under-arcs coloured $y, z$ ,

2x \equiv y + z \pmod p .

Constant colourings always work. A diagram is tricolourable if it has a $3$ -colouring using at least two colours. Since $2 \equiv -1 \pmod 3$ , the condition $2x \equiv y + z$ says $x + y + z \equiv 0$ : the three colours at a crossing are all equal or all different.

Definition— crossing sign, writhe, linking number

For an oriented diagram, a crossing is positive (right-handed) if, looking along the over-strand, the under-strand passes from right to left, and negative otherwise. The writhe $w(D)$ is the sum of the signs of all crossings. For a two-component oriented link, the linking number $\mathrm{lk}(L_1, L_2)$ is half the sum of the signs of the crossings between the two components.

Definition— Kauffman bracket, Jones polynomial

The Kauffman bracket $\langle D\rangle \in \Z[A, A^{-1}]$ of an unoriented diagram is defined by three rules: $\langle O\rangle = 1$ for the round circle; $\langle D \sqcup O\rangle = \delta \langle D\rangle$ with $\delta = -A^2 - A^{-2}$ ; and at any crossing,

\langle D \rangle = A\,\langle D_A \rangle + A^{-1} \langle D_B \rangle ,

where $D_A$ and $D_B$ are the diagrams with that crossing smoothed in the two possible ways. The A-smoothing opens a channel between the two regions swept out when the over-strand is turned anticlockwise; the B-smoothing joins the other two. Expanding every crossing gives the state sum

\langle D \rangle = \sum_{\text{states } S} A^{a(S) - b(S)} \, \delta^{\,|S| - 1},

over the $2^n$ choices of smoothings, where $a(S), b(S)$ count the A- and B-smoothings and $|S|$ is the number of resulting circles. For an oriented knot diagram, $f(D) = (-A^3)^{-w(D)} \langle D \rangle$ , and the Jones polynomial is $V_K(t) = f(D)$ with $A = t^{-1/4}$ .

Definition— Seifert surface, genus

A Seifert surface for a knot $K$ is a compact, connected, orientable surface $\Sigma \subset \R^3$ with boundary $\partial \Sigma = K$ . The genus $g(K)$ is the least genus of a Seifert surface for $K$ .

Worked examplesH

A small zoo

Example— Knots

The trefoil $3_1$ has a diagram with $3$ crossings and $3$ arcs, each passing over once; it comes in a right-handed and a left-handed form. The figure-eight knot $4_1$ has a $4$ -crossing diagram. In the standard tables (Alexander–Briggs, Rolfsen), knots are named by crossing number and position, so $5_1$ and $5_2$ are the two knots with crossing number $5$ . Mirror images are not listed separately. Up to $16$ crossings there are $1{,}701{,}936$ prime knots (Hoste, Thistlethwaite and Weeks, 1998).

Example— Links

The Hopf link consists of two circles linked once; its standard diagram has two crossings, both between the components. The Whitehead link has five crossings, four of them between the components, with signs $+1, -1, +1, -1$ , so its linking number is $0$ — yet it cannot be pulled apart. The Borromean rings are three circles, no two of which are linked (pairwise linking numbers $0$ , and any two of them alone can be separated), but the three together cannot be separated.

Example— A tricolouring of the trefoil

Colour the three arcs of the trefoil $0, 1, 2$ . At each crossing the three arcs carry all three colours, and $0 + 1 + 2 = 3 \equiv 0 \pmod 3$ . So the trefoil diagram is tricolourable. The round unknot diagram has one arc, so it is not. In total the trefoil diagram has $9$ tricolourings: $3$ constant and $6$ using all three colours (the colours of two arcs can be chosen freely, $3 \times 3 = 9$ , and the third is forced).

Example— The bracket of the trefoil, state by state

For the standard right-handed trefoil diagram, the $8$ states give $|S| = 2$ circles for AAA, $1$ circle for each state with two A's, $2$ circles for each state with one A, and $3$ circles for BBB. So

\langle 3_1 \rangle = A^3 \delta + 3A + 3A^{-1}\delta + A^{-3}\delta^2 = -A^5 - A^{-3} + A^{-7}.

All $3$ crossings are positive, so $w = 3$ and $f = (-A^3)^{-3}\langle 3_1\rangle = -A^{-16} + A^{-12} + A^{-4}$ . With $A = t^{-1/4}$ :

V_{3_1}(t) = t + t^3 - t^4 .

The same computation is carried out by the Lean file and the Python experiment below.

ProofH

Reidemeister's theorem and colourings

Theorem— Theorem 1 (Reidemeister 1927; Alexander and Briggs 1926 — proof referenced)

Two diagrams represent equivalent tame knots (or links) if and only if they are related by a finite sequence of Reidemeister moves and planar isotopies.

Proof sketch. One direction is clear: each move is realised by an isotopy in a neighbourhood of the small disc where it happens. For the other, replace the knots by polygons, and the isotopy by a sequence of triangle moves, each replacing one edge of the polygon by the other two sides of a triangle that meets the knot only in that edge (or the reverse). After a small perturbation into general position, the projection of each triangle move can be decomposed into Reidemeister moves. See Burde and Zieschang, Knots, chapter 1, or Lickorish (1997), chapter 1.

Theorem— Theorem 2 (Fox colourings are invariants)

For every $p$ , the number of Fox $p$ -colourings of a diagram is unchanged by Reidemeister moves. Hence it is a knot invariant, and so is tricolourability.

Proof

A move changes the diagram only inside a small disc. We show that colourings of the diagram before and after correspond one to one, agreeing outside the disc. It suffices to show that the colours of the arcs leaving the disc determine those inside, and that the constraints on the outside colours are the same before and after. Write $x \triangleright y = 2x - y$ for the colour of an under-arc $y$ after it passes under an arc of colour $x$ .

Move I. At a kink the over-arc is also one of the two under-arcs: if it has colour $a$ and the other under-arc colour $b$ , the rule says $2a = a + b$ , i.e. $b = a$ . So the strand keeps one colour through the kink, exactly as if there were no kink.

Move II. A strand of colour $x$ passes over a strand that is cut into three arcs $a, m, b$ . The two crossings say $2x = a + m$ and $2x = m + b$ , which hold exactly when $m = 2x - a$ and $b = a$ . So the middle colour is forced, and the outgoing colour equals the incoming one, as without the move.

Move III. Let the incoming colours be $t$ (top strand), $m$ (middle) and $b$ (bottom). The top strand stays $t$ on both sides. The middle strand passes under the top one on both sides and leaves with colour $t \triangleright m$ . The bottom strand passes under both. On one side it goes under the middle strand first, then under the top: it leaves with $t \triangleright (m \triangleright b)$ . On the other side it goes under the top first, then under the middle strand, whose colour there is already $t \triangleright m$ : it leaves with $(t \triangleright m) \triangleright (t \triangleright b)$ . These agree:

2t - (2m - b) = 2(2t - m) - (2t - b),

as both sides equal $2t - 2m + b$ . The interior colours are again forced.

So the colourings correspond bijectively, and their number is unchanged. A colouring uses at least two colours exactly when its counterpart does, since the colours on the boundary of the disc (and outside it) are the same.

∎

The identity in move III, $x \triangleright (y \triangleright z) = (x \triangleright y) \triangleright (x \triangleright z)$ , is self-distributivity. Together with $x \triangleright x = x$ (move I) and the invertibility of $y \mapsto x \triangleright y$ (move II), it makes $\Z/p$ a quandle — the dihedral quandle.

Theorem— Corollary 3

(a) The trefoil is knotted. (b) The figure-eight knot is knotted. (c) The trefoil and the figure-eight knot are different.

Proof

Count colourings (all counts are formalised in Lean below). The unknot's round diagram has one arc, so it has exactly $p$ colourings for every $p$ . The trefoil diagram has $9$ three-colourings, while the unknot has $3$ ; this proves (a). The figure-eight diagram has only the $3$ constant three-colourings, so it is not tricolourable — that alone proves nothing! But it has $25$ five-colourings, against $5$ for the unknot, which proves (b). The trefoil has only $5$ five-colourings and $9$ three-colourings, versus $25$ and $3$ for the figure-eight knot, which proves (c).

∎

More generally, the number of $p$ -colourings, for $p$ prime, is $p^{1 + k}$ , where $k$ is the dimension of the kernel of the reduced colouring matrix mod $p$ . A non-constant $p$ -colouring exists exactly when $p$ divides the determinant of the knot, $|\Delta_K(-1)|$ , where $\Delta_K$ is the Alexander polynomial. The determinants of $3_1, 4_1, 5_1, 5_2, 6_1$ are $3, 5, 5, 7, 9$ (see the computation section).

ProofH

The linking number

Theorem— Theorem 4 (the linking number is an invariant)

The linking number of an oriented two-component link is an integer and is unchanged by Reidemeister moves.

Proof

For a two-component diagram, let $s_1$ be the sum of the signs of the crossings where $L_1$ passes over $L_2$ , and $s_2$ the sum over the crossings where $L_1$ passes under $L_2$ , so that $\mathrm{lk} = \tfrac12 (s_1 + s_2)$ .

Invariance of $s_1$ and $s_2$ . Move I creates a crossing of a component with itself, which does not count. Move II creates two crossings between the same two strands, with the same strand on top and opposite signs; if the strands belong to different components, both crossings fall into the same sum, $s_1$ or $s_2$ , and cancel. Move III moves strands past a crossing without changing any crossing's sign, or which strand is on top. So $s_1$ , $s_2$ and $\mathrm{lk}$ are invariant.

$\mathrm{lk}$ is an integer. We show $s_1 = s_2$ . Switching a crossing between the components (exchanging over and under) reverses its sign and moves it from one sum to the other, so it leaves $s_1 - s_2$ unchanged. Switch every crossing where $L_1$ passes under $L_2$ . In the resulting diagram $L_1$ is on top at every crossing between the components, so we can lift $L_1$ into a horizontal slab above $L_2$ and slide it sideways. The result is a diagram with no crossings between the components, where $s_1 = s_2 = 0$ . By invariance $s_1 = s_2 = 0$ in the switched diagram too, so there $s_1 - s_2 = 0$ , and therefore $s_1 = s_2$ in the original diagram. Hence $\mathrm{lk} = s_1$ is an integer.

∎

The Hopf link has two crossings between its components, both of sign $+1$ (for one choice of orientations), so $\mathrm{lk} = 1 \ne 0$ : it cannot be pulled apart. The Whitehead link has $\mathrm{lk} = 0$ but is still linked, and the Borromean rings have all pairwise linking numbers $0$ . The linking number is a useful but incomplete invariant. Gauss found it in 1833 as an integral over the two curves, $\mathrm{lk} = \frac{1}{4\pi} \oint\oint \frac{(\mathbf{r}_1 - \mathbf{r}_2) \cdot (d\mathbf{r}_1 \times d\mathbf{r}_2)}{|\mathbf{r}_1 - \mathbf{r}_2|^3}$ , while studying the orbits of asteroids and electromagnetism.

ProofH

The Kauffman bracket and the Jones polynomial

Theorem— Theorem 5 (Kauffman 1987)

(a) The bracket $\langle D\rangle$ is unchanged by moves II and III. (b) Move I multiplies it by $-A^{3}$ or $-A^{-3}$ , according to the sign of the kink. (c) Consequently $f(D) = (-A^3)^{-w(D)}\langle D\rangle$ is an invariant of oriented knots, and so is the Jones polynomial $V_K(t)$ .

Proof

(a) Move II. Expand both crossings of the two-crossing tangle with the bracket rule. The two states that smooth both crossings the same way contribute $A^2$ and $A^{-2}$ times the bracket of the "cup–cap" tangle $\asymp$ . Of the two mixed states (each with coefficient $A \cdot A^{-1} = 1$ ), one gives two parallel strands, the tangle after the move, and the other gives $\asymp$ with an extra small circle, contributing $\delta$ times the cup–cap bracket. In total

\langle \text{II-tangle} \rangle = (A^2 + A^{-2} + \delta)\,\langle \asymp \rangle + \langle \text{parallel strands} \rangle = \langle \text{parallel strands} \rangle ,

because $\delta = -A^2 - A^{-2}$ . This is why $\delta$ must have that value.

Move III. Expand the crossing between the two lower strands (the one the moving strand does not touch) on both sides of the move. The two A-smoothings give tangles related by two moves II, and so do the two B-smoothings. By the case just proved their brackets agree, hence so do the brackets before and after move III.

(b) Move I. Smoothing the crossing of a kink one way leaves the strand plus a small circle, and the other way leaves just the strand. For a positive kink (with the conventions above) the A-smoothing produces the circle:

\langle \text{kink} \rangle = A\,\delta\,\langle | \rangle + A^{-1}\langle | \rangle = (-A^3 - A^{-1} + A^{-1})\langle | \rangle = -A^3 \langle | \rangle .

For a negative kink the roles of the smoothings swap, giving $A + A^{-1}\delta = -A^{-3}$ .

(c) Moves II and III do not change the writhe (move II adds one positive and one negative crossing; move III preserves the signs). Move I changes $w$ by $\pm 1$ and $\langle D \rangle$ by $-A^{\pm 3}$ , and these cancel in $f(D)$ . For a knot, the exponents of $A$ in $f(D)$ are multiples of $4$ , so the substitution $A = t^{-1/4}$ gives a Laurent polynomial in $t$ .

∎

Theorem— Corollary 6 (the trefoil is chiral; Dehn 1914)

The right-handed trefoil is not equivalent to its mirror image.

Proof

Reflecting a diagram switches every crossing. That exchanges A- and B-smoothings, so $\langle \bar D\rangle(A) = \langle D\rangle(A^{-1})$ , and it negates every crossing sign, so $w(\bar D) = -w(D)$ . Hence $V_{\bar K}(t) = V_K(t^{-1})$ . For the trefoil, $V(t) = t + t^3 - t^4$ , while its mirror has $V(t) = t^{-1} + t^{-3} - t^{-4}$ . These differ, and $V$ is an invariant (Theorem 5), so the two knots are not equivalent.

∎

The figure-eight knot has $V(t) = t^{-2} - t^{-1} + 1 - t + t^2 = V(t^{-1})$ , consistent with the fact that it is equivalent to its mirror image (it is amphichiral; one sees this by an explicit isotopy). The symmetry of $V$ alone would not prove this: the knot $9_{42}$ is chiral but its Jones polynomial is symmetric.

Dehn's original proof (1914) used the fundamental group of the knot complement. The Jones polynomial, discovered by Vaughan Jones in 1984, made the result a short computation.

ProofH

Seifert surfaces and genus

Theorem— Theorem 7 (Seifert 1934)

Every knot bounds a Seifert surface. If a diagram of $K$ with $c$ crossings produces $s$ Seifert circles (see the proof), the resulting surface has genus $\tfrac12(c - s + 1)$ .

Proof

Seifert's algorithm. Orient the knot and take a diagram. At each crossing, smooth in the way that respects the orientation: the two incoming strands are joined to the two outgoing ones without reversing direction. The result is a family of disjoint oriented circles in the plane, the Seifert circles. Fill each with a disc, placing nested discs at different heights. At each former crossing, attach a half-twisted band joining the two discs there, twisted according to the crossing. The boundary of this surface is the knot.

The surface is orientable: give each disc the orientation from its circle (anticlockwise discs face up, clockwise ones down); the half-twisted bands join discs consistently, because the smoothing respected the orientation. It is connected if the diagram is connected. It deformation retracts onto a graph with $s$ vertices (the discs) and $c$ edges (the bands), so its Euler characteristic is $\chi = s - c$ . A compact connected orientable surface of genus $g$ with one boundary circle has $\chi = 2 - 2g - 1 = 1 - 2g$ . So $g = \tfrac12(1 - s + c)$ .

∎

Seifert's algorithm on the standard trefoil diagram: smoothing the 3 crossings along the orientation gives 2 nested Seifert circles; the discs they bound are joined by 3 half-twisted bands. Then χ = 2 − 3 = −1 = 1 − 2g, so the surface has genus 1 — a punctured torus.

So the trefoil has genus at most $1$ , and since it is knotted its genus is not $0$ (a knot of genus $0$ bounds an embedded disc, and so is unknotted). Hence $g(3_1) = 1$ . Two further theorems, which we only state: the genus is additive under connected sum, $g(K_1 \# K_2) = g(K_1) + g(K_2)$ (Schubert, 1949). In particular no knot can be cancelled by tying another knot in the same string. And every knot decomposes uniquely into prime knots (Schubert, 1949).

ExplanationH

What is known, and what is open

Known. Knots are classified algorithmically: Wolfgang Haken (1961) gave an algorithm to decide whether a knot is unknotted, using normal surfaces, and later work (building on Haken, Thurston's geometrisation and the work of many others) gives an algorithm to decide whether any two knots are equivalent. Unknot recognition is in the complexity class NP (Hass, Lagarias and Pippenger, 1999) and in co-NP (Lackenby). Any diagram of the unknot with $c$ crossings can be untangled with at most $(236c)^{11}$ Reidemeister moves (Lackenby, 2015). Knots are determined by their complements, up to mirror image and orientation (Gordon and Luecke, 1989). Khovanov homology, a refinement of the Jones polynomial, detects the unknot (Kronheimer and Mrowka, 2011).

Open. Does the Jones polynomial detect the unknot — is there a non-trivial knot $K$ with $V_K(t) = 1$ ? This is unknown, although the answer is known to be no for knots with few crossings, which have been checked by computer, and there are non-trivial links with the Jones polynomial of an unlink (Eliahou, Kauffman and Thistlethwaite, 2003). Also open: whether unknot recognition can be done in polynomial time (Marc Lackenby has announced a quasi-polynomial-time algorithm), and the slice–ribbon conjecture of Ralph Fox (1962): is every smoothly slice knot — one bounding a smooth disc in the four-ball — a ribbon knot? Such questions lie at the frontier of low-dimensional topology.

Formal mathematicsF

Knot diagrams in Lean

Mathlib does not (yet) contain knots as embeddings of the circle, ambient isotopy, or Reidemeister's theorem. So the Lean module works with diagram codes, finite data that Lean can compute with, and proves the algebra and the computations. It does not prove the topological step "a diagram invariant is a knot invariant"; that is Theorem 1 together with the invariance proofs above.

A diagram is a list of arcs and crossings, and a Fox colouring is a function on arcs satisfying $2x = y + z$ at every crossing:

ArcDiagramLean 4Formally verified

/-- A knot diagram, recorded by its **arcs** (the unbroken strands, numbered `0, …, arcs - 1`) and
its **crossings**. A crossing `(o, u₁, u₂)` lists the arc `o` passing over and the two arcs `u₁`,
`u₂` that end there, passing under. -/
structure ArcDiagram where
  arcs : ℕ
  crossings : List (Fin arcs × Fin arcs × Fin arcs)

Axioms used: No axiomsformal/Lumenary/KnotTheory.leanTry it in the Lean web editor

IsFoxColouringLean 4Formally verified

/-- A **Fox `p`-colouring** gives each arc a colour in `ZMod p` so that at every crossing
`2 · (over) = (under₁) + (under₂)`. For `p = 3` this says the three colours at a crossing are
all equal or all different — the tricolouring rule. -/
def IsFoxColouring (D : ArcDiagram) (p : ℕ) (c : Fin D.arcs → ZMod p) : Prop :=
  ∀ x ∈ D.crossings, 2 * c x.1 = c x.2.1 + c x.2.2

Axioms used: propext, Quot.soundformal/Lumenary/KnotTheory.leanTry it in the Lean web editor

trefoilDiagramLean 4Formally verified

/-- The standard trefoil diagram: three arcs and three crossings, each arc passing over once. -/
abbrev trefoilDiagram : ArcDiagram := ⟨3, [(0, 1, 2), (1, 2, 0), (2, 0, 1)]⟩

Axioms used: propextformal/Lumenary/KnotTheory.leanTry it in the Lean web editor

figureEightDiagramLean 4Formally verified

/-- The standard figure-eight diagram: four arcs `0 = A, 1 = B, 2 = C, 3 = D` and four crossings
(over; under, under) = (A; B, C), (C; D, A), (B; C, D), (D; A, B). -/
abbrev figureEightDiagram : ArcDiagram := ⟨4, [(0, 1, 2), (2, 3, 0), (1, 2, 3), (3, 0, 1)]⟩

Axioms used: propextformal/Lumenary/KnotTheory.leanTry it in the Lean web editor

Tricolourability of the trefoil and its failure for the unknot, and the colouring counts used in Corollary 3, verified by checking all $3^3$ , $3^4$ , $5^3$ and $5^4$ colourings with decide:

trefoil_tricolourableLean 4Proved here from basic factsFormally verified

/-- **The trefoil diagram is tricolourable**: colour its arcs `0, 1, 2`. At each crossing the
three colours are all different, and `2 · 0 = 1 + 2`, `2 · 1 = 2 + 0`, `2 · 2 = 0 + 1` in
`ZMod 3`. -/
theorem trefoil_tricolourable :
    ∃ c : Fin 3 → ZMod 3, IsFoxColouring trefoilDiagram 3 c ∧ ∃ i j, c i ≠ c j :=
  ⟨![0, 1, 2], by decide, 0, 1, by decide⟩