Knot theory

Embeddings of circles in three-space up to ambient isotopy: knot and link diagrams, chirality, slice knots, and geometric invariants such as ropelength, distortion and quadrisecants.

• Knots, links and ambient isotopy
• Distortion of knots
• Quadrisecant theorem
• Slice knots
• Knot diagrams
• Ropelength and crossing number

TheoremExistence of a chiral knot#●ready to prove

There exists an oriented smooth knot \(K\) in \(\mathbb{R}^3\) that is chiral: it is not ambient-isotopic, as an oriented knot, to its mirror image \(r \circ K\), where \(r(x, y, z) = (x, y, -z)\) is the reflection through the \(xy\)-plane.

public theorem_wanted exists_chiral_knot : ∃ K : Knot, K.Chiral

Sources

• Classical; see https://en.wikipedia.org/wiki/Chirality_(mathematics) and https://en.wikipedia.org/wiki/Trefoil_knot. Problem exists_chiral_knot of the lean-eval benchmark.

Uses 2

Statement usesOriented smooth knot · Chiral knot

TheoremOesper's determinant formula for three-strand weaving knots#✓fully proved

Let \(k \ge 1\) be an integer, let \(F_i\) be the Fibonacci numbers (\(F_0 = 0\), \(F_1 = 1\)), let \(C_j = \sum_{i=1}^{j} (-1)^{i+1} F_i\) for \(j \ge 0\), and let \(M\) be the \(3 \times 3\) integer matrix with rows \((2, -1, 0)\), \((0, 0, 1)\) and \((-1, 0, 2)\). Then the absolute value of the determinant of the \(2 \times 2\) matrix obtained from \(M^k - I\) by deleting its first row and first column equals \(-(C_{2k-2} + 1) C_{2k} + C_{2k-1}^2\).

Here \(M\) is the base-word matrix of the spiral knot \(S(3, k, (1, -1))\), which is the three-strand weaving knot \(W(k, 3)\), and the left-hand side is the determinant of this knot: the cofactor minors of \(M^k - I\) agree up to sign, so taking the absolute value gives the nonnegative knot determinant.

theorem oesper_weaving_three_determinant (k : Nat) (hk : 0 < k) :
    let C : Nat -> Int := fun j => Finset.sum (Finset.Icc 1 j)
      (fun i => (-1 : Int) ^ (i + 1) * Nat.fib i);
    let M : Matrix (Fin 3) (Fin 3) Int := !![2, -1, 0; 0, 0, 1; -1, 0, 2];
    abs (Matrix.det
          (((M ^ k) - 1).submatrix (Fin.succAbove (0 : Fin 3))
            (Fin.succAbove (0 : Fin 3)))) =
      -(C (2 * k - 2) + 1) * C (2 * k) + C (2 * k - 1) ^ 2

Sources

• Seong Ju Kim, Ryan Stees, and Laura Taalman, "Sequences of Spiral Knot Determinants", Journal of Integer Sequences 19 (2016), Article 16.1.4, lines 409-412: https://cs.uwaterloo.ca/journals/JIS/VOL19/Stees/stees4.tex The formula is attributed to L. Oesper, "p-colorings of weaving knots" (preprint).

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.