Existence of a non-isotopic pair of oriented two-component links

Loading leaderboard data…

Problem statement

Notes: Warmup for the knot-theory benchmark. Asks for two oriented smooth two-component links in R^3 that are not ambient-isotopic. The benchmark uses an orientation-sensitive notion of isotopy induced by the parametrizations, so the Gauss linking integral is a natural real-valued invariant distinguishing the unlink (lk = 0) from the Hopf link (lk = +/- 1, depending on orientation choice).

Source: Classical; see https://en.wikipedia.org/wiki/Linking_number.

Informal solution: Take L1 = unlink (two unit circles in parallel planes) and L2 = Hopf link, with explicit orientations induced by the parametrizations. Define lk(K, L) by the Gauss double integral (1/4 pi) int int <K(s) - L(t), K'(s) x L'(t)> / |K(s) - L(t)|^3 ds dt. Prove lk is invariant under ambient isotopy of oriented links by exhibiting it as the integral of a closed 2-form on R^3 minus the origin pulled back along (K, L), so Stokes-style arguments show invariance. Compute lk(unlink) = 0 and choose the Hopf-link orientations so that lk(Hopf) = 1. Conclude L1 and L2 are not ambient-isotopic.

theorem declaration uses `sorry`exists_nonisotopic_link : L₁ L₂ : LeanEval.KnotTheory.TwoLink, ¬ L₁.Isotopic L₂ := L₁ L₂, ¬L₁.Isotopic L₂ All goals completed! 🐙