Existence of a chiral oriented knot

← All problems

exists_chiral_knot

Submitter: Kim Morrison.

Notes: Challenge problem of the knot-theory benchmark. Asks for an oriented smooth knot whose image is not ambient-isotopic to its mirror image (under reflection through the xy-plane), using the benchmark's orientation-sensitive notion of isotopy induced by the parametrization. The model must construct an ambient-isotopy invariant that takes different values on a knot and its mirror -- the knot determinant and Alexander polynomial alone do not suffice, since the figure-eight is amphichiral in the usual unoriented sense.

Source: Classical; see https://en.wikipedia.org/wiki/Chirality_(mathematics) and https://en.wikipedia.org/wiki/Trefoil_knot.

Informal solution: Take K = right-handed trefoil. Construct the knot signature sigma(K) from a Seifert matrix V as the signature of V + V^T, and verify that sigma is an ambient-isotopy invariant of knots that negates under mirror reflection. Compute sigma(right trefoil) = -2, so sigma(K) != sigma(mirror K) and K is chiral. (Alternatively, use the Jones polynomial V_K(t) = -t^{-4} + t^{-3} + t^{-1}, which is not symmetric under t <-> t^{-1}.)

theorem declaration uses `sorry`exists_chiral_knot : K : LeanEval.KnotTheory.Knot, K.Chiral := K, K.Chiral All goals completed! 🐙

Solved by

Not yet solved.