Knots, links and ambient isotopy

StructureParametrized knot#✓fully proved

An oriented parametrized smooth knot in Euclidean 3-space is a \(C^\infty\) curve \(\gamma \colon \mathbb{R} \to \mathbb{R}^3\) that is \(2\pi\)-periodic (\(\gamma(t + 2\pi) = \gamma(t)\) for all \(t\)), injective on \([0, 2\pi)\), and an immersion (\(\gamma'(t) \neq 0\) for all \(t\)).

structure ParametrizedKnot where
  curve : ℝ → R3
  smooth : ContDiff ℝ (⊤ : ℕ∞) curve
  periodic : ∀ t, curve (t + 2 * Real.pi) = curve t
  injOn : Set.InjOn curve (Set.Ico 0 (2 * Real.pi))
  immersion : ∀ t, deriv curve t ≠ 0
Uses 1 · Used by 26
Statement usesEuclidean 3-space
Used byLinks with a crossing-free regular projection admit alternating diagrams · The crossing number is an isotopy invariant · A link's own regular projection bounds its crossing number · Points with the same projection have different heights · The projected trace is the union of the projected components · Admitting an alternating diagram is an isotopy invariant · Point of a link at a parameter point · Projected curve of a link component · Projected tangent vector · Isotopy of parametrized knots · Isotopy of parametrized links · Knots are the same as parametrized knots · Isotopy of knots agrees with isotopy of parametrized knots · Parametrized knots as knots · Labeled two-component links as two-component links · Parametrized link · Ropelength of a parametrized knot · Ropelength is an isotopy invariant · Ropelength is at most the ropelength ratio · Parametrized knot as a one-component link · Isotopic knots give isotopic one-component links · Knots as parametrized knots · Two-component links as labeled links · Total contour length of a parametrized link · Trace of a parametrized link · Two-component link isotopy agrees with labeled link isotopy

An oriented labeled parametrized smooth link with \(n\) components in Euclidean 3-space is a family \((\gamma_i)_{i < n}\) of parametrized knots whose traces \(\gamma_i(\mathbb{R})\) are pairwise disjoint.

structure ParametrizedLink (n : ℕ) where
  component : Fin n → ParametrizedKnot
  pairwiseDisjoint : Set.PairwiseDisjoint (Set.univ : Set (Fin n))
    (fun i => Set.range (component i).curve)
Uses 2 · Used by 61
Statement usesEuclidean 3-space · Parametrized knot
Used byLinks admitting an alternating diagram · Links with a crossing-free regular projection admit alternating diagrams · Crossings of a link projection · Crossing count of a regular projection · A crossing-free regular projection has crossing count zero · A regular projection with a crossing has positive crossing count · Crossing number of a link · The crossing number is an isotopy invariant · Crossing number zero from a crossing-free representative · Regular projections of isotopic links bound the crossing number · A link's own regular projection bounds its crossing number · Finiteness of the crossing number · Cyclically adjacent crossing preimages · Double points of a link projection · The over and under preimages exhaust a crossing · Double points have exactly two preimages · The over-strand preimage exists and is unique · The under-strand preimage exists and is unique · Height of a parameter point · Points with the same projection have different heights · The under-strand lies strictly below the over-strand · The projected trace is the union of the projected components · Alternating regular projections · Crossingless regular projections are alternating · Crossing preimages · Over/under status at a crossing preimage · The two preimages of a crossing have opposite status · Being the over-strand preimage of a crossing · Regular projections · Being the under-strand preimage of a crossing · Admitting an alternating diagram is an isotopy invariant · Over-strand preimage of a crossing · Point of a link at a parameter point · Projected curve of a link component · Projected point of a link at a parameter point · The over-strand preimage lies over its crossing · The under-strand preimage lies over its crossing · Projected tangent vector · Under-strand preimage of a crossing · Over and under preimages differ · Isotopy of parametrized links · Labeled two-component links as two-component links · Ropelength of a parametrized link · Ropelength is an isotopy invariant · Ropelength is at most the ratio of any isotopic link · Ropelength is at most the ropelength ratio · Ropelength ratio of a parametrized link · Parametrized knot as a one-component link · Isotopic knots give isotopic one-component links · Two-component links as labeled links · Total contour length of a parametrized link · Trace of a parametrized link · Two-component link isotopy agrees with labeled link isotopy · Alternating link types have finite crossing number · Alternating link types have a natural-number crossing number · Admissible constants for the tight-knot inequality · Admissible constants for the tight alternating knot inequality · Zero is an admissible alternating constant · Zero is an admissible tight-knot constant · Admissible alternating constants are downward closed among nonnegative reals · Admissibility passes to smaller nonnegative constants

StructureSmooth ambient isotopy of Euclidean 3-space#✓fully proved

A smooth ambient isotopy of \(\mathbb{R}^3\) consists of two families of maps \(H_t, G_t \colon \mathbb{R}^3 \to \mathbb{R}^3\), indexed by times \(t \in \mathbb{R}\), such that \((t, x) \mapsto H_t(x)\) and \((t, x) \mapsto G_t(x)\) are \(C^\infty\) on \(\mathbb{R} \times \mathbb{R}^3\), \(G_t(H_t(x)) = x\) and \(H_t(G_t(x)) = x\) for all \(t\) and \(x\), and \(H_0\) is the identity.

structure AmbientIsotopy where
  H : ℝ → R3 → R3
  Hinv : ℝ → R3 → R3
  smooth : ContDiff ℝ (⊤ : ℕ∞) (Function.uncurry H)
  smooth_inv : ContDiff ℝ (⊤ : ℕ∞) (Function.uncurry Hinv)
  inv_left : ∀ t x, Hinv t (H t x) = x
  inv_right : ∀ t x, H t (Hinv t x) = x
  start : H 0 = id
Uses 1 · Used by 16
Statement usesEuclidean 3-space
Used byLinks with a crossing-free regular projection admit alternating diagrams · The crossing number is an isotopy invariant · A link's own regular projection bounds its crossing number · Admitting an alternating diagram is an isotopy invariant · Composition of ambient isotopies · Identity ambient isotopy · Isotopy of parametrized knots · Isotopy of parametrized links · Isotopy of knots agrees with isotopy of parametrized knots · Euclidean ambient isotopies as Conway-knot ambient isotopies · Ropelength is an isotopy invariant · Ropelength is at most the ropelength ratio · Inverse ambient isotopy · Conway-knot ambient isotopies as Euclidean ambient isotopies · Isotopic knots give isotopic one-component links · Two-component link isotopy agrees with labeled link isotopy

DefinitionIdentity ambient isotopy#✓fully proved

The identity ambient isotopy of \(\mathbb{R}^3\) has forward and inverse families \(H_t\) and \(G_t\) equal to the identity map of \(\mathbb{R}^3\) for every time \(t\).

MathlibExt.Topology.Knot.Euclidean.AmbientIsotopy.id · 20 lines 
def AmbientIsotopy.id : AmbientIsotopy where
  H := fun _ => _root_.id
  Hinv := fun _ => _root_.id
  smooth := by
    have hfun : Function.uncurry (fun _ => _root_.id) =
        (Prod.snd : ℝ × R3 → R3) := by
      funext ⟨t, x⟩
      rfl
    rw [hfun]
    exact contDiff_snd
  smooth_inv := by
    have hfun : Function.uncurry (fun _ => _root_.id) =
        (Prod.snd : ℝ × R3 → R3) := by
      funext ⟨t, x⟩
      rfl
    rw [hfun]
    exact contDiff_snd
  inv_left := fun _ _ => rfl
  inv_right := fun _ _ => rfl
  start := rfl
Uses 2 · Used by 3
Statement usesEuclidean 3-space · Smooth ambient isotopy of Euclidean 3-space
Used byLinks with a crossing-free regular projection admit alternating diagrams · A link's own regular projection bounds its crossing number · Ropelength is at most the ropelength ratio

DefinitionInverse ambient isotopy#✓fully proved

The inverse of an ambient isotopy with forward family \((H_t)\) and inverse family \((H_t^{-1})\) is the ambient isotopy whose forward family is \((H_t^{-1})\) and whose inverse family is \((H_t)\); at each time \(t\) it is the inverse diffeomorphism of \(H_t\).

def AmbientIsotopy.symm (Φ : AmbientIsotopy) : AmbientIsotopy where
  H := Φ.Hinv
  Hinv := Φ.H
  smooth := Φ.smooth_inv
  smooth_inv := Φ.smooth
  inv_left := Φ.inv_right
  inv_right := Φ.inv_left
  start := by
    funext x
    have h := Φ.inv_right 0 x
    rw [Φ.start] at h
    exact h
Uses 2 · Used by 2
Statement usesEuclidean 3-space · Smooth ambient isotopy of Euclidean 3-space
Used byThe crossing number is an isotopy invariant · Ropelength is an isotopy invariant

DefinitionComposition of ambient isotopies#✓fully proved

If \(\Phi\) and \(\Psi\) are smooth ambient isotopies of \(\mathbb{R}^3\) with forward families \(H_t, H'_t\) and inverse families \(G_t, G'_t\), their composition (first \(\Phi\), then \(\Psi\), at the same time parameter) is the ambient isotopy with forward family \(H'_t \circ H_t\) and inverse family \(G_t \circ G'_t\).

MathlibExt.Topology.Knot.Euclidean.AmbientIsotopy.comp · 32 lines 
def AmbientIsotopy.comp (Φ Ψ : AmbientIsotopy) : AmbientIsotopy where
  H := fun t x => Ψ.H t (Φ.H t x)
  Hinv := fun t x => Φ.Hinv t (Ψ.Hinv t x)
  smooth := by
    have hpre : ContDiff ℝ (⊤ : ℕ∞)
        (fun p : ℝ × R3 => (p.1, Φ.H p.1 p.2)) :=
      contDiff_fst.prodMk Φ.smooth
    have hfun : Function.uncurry (fun t x => Ψ.H t (Φ.H t x)) =
        fun p : ℝ × R3 => Ψ.H p.1 (Φ.H p.1 p.2) := by
      funext ⟨t, x⟩
      rfl
    rw [hfun]
    exact Ψ.smooth.comp hpre
  smooth_inv := by
    have hpre : ContDiff ℝ (⊤ : ℕ∞)
        (fun p : ℝ × R3 => (p.1, Ψ.Hinv p.1 p.2)) :=
      contDiff_fst.prodMk Ψ.smooth_inv
    have hfun : Function.uncurry (fun t x => Φ.Hinv t (Ψ.Hinv t x)) =
        fun p : ℝ × R3 => Φ.Hinv p.1 (Ψ.Hinv p.1 p.2) := by
      funext ⟨t, x⟩
      rfl
    rw [hfun]
    exact Φ.smooth_inv.comp hpre
  inv_left := by
    intro t x
    simp [Φ.inv_left, Ψ.inv_left]
  inv_right := by
    intro t x
    simp [Φ.inv_right, Ψ.inv_right]
  start := by
    funext x
    simp [Φ.start, Ψ.start]
Uses 2 · Used by 3
Statement usesEuclidean 3-space · Smooth ambient isotopy of Euclidean 3-space
Used byThe crossing number is an isotopy invariant · Admitting an alternating diagram is an isotopy invariant · Ropelength is an isotopy invariant

StructureOrientation-preserving reparametrization of the circle#✓fully proved

An orientation-preserving smooth reparametrization of the circle is given by maps \(f, g \colon \mathbb{R} \to \mathbb{R}\), both \(C^\infty\) and inverse to each other (\(g(f(t)) = t\) and \(f(g(t)) = t\) for all \(t\)), such that \(f(t + 2\pi) = f(t) + 2\pi\) and \(g(t + 2\pi) = g(t) + 2\pi\) for all \(t\), and \(f\) is strictly increasing. Here \(f\) is a lift of the reparametrization and \(g\) is a lift of its inverse.

structure CircleReparam where
  f : ℝ → ℝ
  finv : ℝ → ℝ
  smooth : ContDiff ℝ (⊤ : ℕ∞) f
  smooth_inv : ContDiff ℝ (⊤ : ℕ∞) finv
  left_inv : ∀ t, finv (f t) = t
  right_inv : ∀ t, f (finv t) = t
  periodic : ∀ t, f (t + 2 * Real.pi) = f t + 2 * Real.pi
  periodic_inv : ∀ t, finv (t + 2 * Real.pi) = finv t + 2 * Real.pi
  mono : StrictMono f
Used by 16
Used byLinks with a crossing-free regular projection admit alternating diagrams · The crossing number is an isotopy invariant · A link's own regular projection bounds its crossing number · Admitting an alternating diagram is an isotopy invariant · Composition of circle reparametrizations · Identity reparametrization of the circle · Isotopy of parametrized knots · Isotopy of parametrized links · Isotopy of knots agrees with isotopy of parametrized knots · Euclidean circle reparametrizations as Conway-knot ones · Ropelength is an isotopy invariant · Ropelength is at most the ropelength ratio · Inverse circle reparametrization · Conway-knot circle reparametrizations as Euclidean ones · Isotopic knots give isotopic one-component links · Two-component link isotopy agrees with labeled link isotopy

DefinitionIdentity reparametrization of the circle#✓fully proved

The identity circle reparametrization has lift and inverse lift both equal to the identity map of \(\mathbb{R}\).

def CircleReparam.id : CircleReparam where
  f := _root_.id
  finv := _root_.id
  smooth := contDiff_id
  smooth_inv := contDiff_id
  left_inv := fun _ => rfl
  right_inv := fun _ => rfl
  periodic := fun _ => rfl
  periodic_inv := fun _ => rfl
  mono := strictMono_id
Uses 1 · Used by 3
Statement usesOrientation-preserving reparametrization of the circle
Used byLinks with a crossing-free regular projection admit alternating diagrams · A link's own regular projection bounds its crossing number · Ropelength is at most the ropelength ratio

DefinitionInverse circle reparametrization#✓fully proved

The inverse of a circle reparametrization with lift \(f\) and inverse lift \(f^{-1}\) is the circle reparametrization whose lift is \(f^{-1}\) and whose inverse lift is \(f\).

MathlibExt.Topology.Knot.Euclidean.CircleReparam.symm · 16 lines 
def CircleReparam.symm (σ : CircleReparam) : CircleReparam where
  f := σ.finv
  finv := σ.f
  smooth := σ.smooth_inv
  smooth_inv := σ.smooth
  left_inv := σ.right_inv
  right_inv := σ.left_inv
  periodic := σ.periodic_inv
  periodic_inv := σ.periodic
  mono := by
    intro a b hab
    by_contra hnot
    have hle : σ.finv b ≤ σ.finv a := le_of_not_gt hnot
    have hmono := σ.mono.monotone hle
    rw [σ.right_inv, σ.right_inv] at hmono
    exact not_lt_of_ge hmono hab
Uses 1 · Used by 2
Statement usesOrientation-preserving reparametrization of the circle
Used byThe crossing number is an isotopy invariant · Ropelength is an isotopy invariant

DefinitionComposition of circle reparametrizations#✓fully proved

If \(\sigma\) and \(\tau\) are circle reparametrizations with lifts \(f_\sigma, f_\tau\) and inverse lifts \(g_\sigma, g_\tau\), their composition (first \(\sigma\), then \(\tau\)) is the circle reparametrization with lift \(f_\tau \circ f_\sigma\) and inverse lift \(g_\sigma \circ g_\tau\).

MathlibExt.Topology.Knot.Euclidean.CircleReparam.comp · 18 lines 
def CircleReparam.comp (σ τ : CircleReparam) : CircleReparam where
  f := τ.f ∘ σ.f
  finv := σ.finv ∘ τ.finv
  smooth := τ.smooth.comp σ.smooth
  smooth_inv := σ.smooth_inv.comp τ.smooth_inv
  left_inv := by
    intro t
    simp [τ.left_inv, σ.left_inv]
  right_inv := by
    intro t
    simp [σ.right_inv, τ.right_inv]
  periodic := by
    intro t
    simp [σ.periodic, τ.periodic]
  periodic_inv := by
    intro t
    simp [τ.periodic_inv, σ.periodic_inv]
  mono := τ.mono.comp σ.mono
Uses 1 · Used by 3
Statement usesOrientation-preserving reparametrization of the circle
Used byThe crossing number is an isotopy invariant · Admitting an alternating diagram is an isotopy invariant · Ropelength is an isotopy invariant

DefinitionIsotopy of parametrized knots#✓fully proved

Two parametrized knots \(\gamma_1, \gamma_2\) in \(\mathbb{R}^3\) are isotopic (oriented ambient isotopy) if there are a smooth ambient isotopy of \(\mathbb{R}^3\) with forward family \(H_t\) and an orientation-preserving reparametrization of the circle with lift \(f\) such that \(H_1(\gamma_1(t)) = \gamma_2(f(t))\) for every \(t \in \mathbb{R}\).

def ParametrizedKnot.Isotopic (K₁ K₂ : ParametrizedKnot) : Prop :=
  ∃ Φ : AmbientIsotopy, ∃ σ : CircleReparam,
    ∀ t, Φ.H 1 (K₁.curve t) = K₂.curve (σ.f t)
Uses 4 · Used by 2
Statement usesEuclidean 3-space · Smooth ambient isotopy of Euclidean 3-space · Orientation-preserving reparametrization of the circle · Parametrized knot
Used byIsotopy of knots agrees with isotopy of parametrized knots · Isotopic knots give isotopic one-component links

DefinitionIsotopy of parametrized links#✓fully proved

Two parametrized links in \(\mathbb{R}^3\) with \(n\) components \(\gamma^1_i\) and \(\gamma^2_i\) (\(i < n\)) are isotopic (oriented, labeled ambient isotopy) if there are a single smooth ambient isotopy of \(\mathbb{R}^3\) with forward family \(H_t\) and, for each \(i < n\), an orientation-preserving reparametrization of the circle with lift \(f_i\), such that \(H_1(\gamma^1_i(t)) = \gamma^2_i(f_i(t))\) for every \(i < n\) and every \(t \in \mathbb{R}\).

def ParametrizedLink.Isotopic {n : ℕ}
    (L₁ L₂ : ParametrizedLink n) : Prop :=
  ∃ Φ : AmbientIsotopy, ∃ σ : Fin n → CircleReparam,
    ∀ i t, Φ.H 1 ((L₁.component i).curve t) =
      (L₂.component i).curve ((σ i).f t)
Uses 5 · Used by 16
Statement usesEuclidean 3-space · Smooth ambient isotopy of Euclidean 3-space · Orientation-preserving reparametrization of the circle · Parametrized knot · Parametrized link
Used byLinks admitting an alternating diagram · Links with a crossing-free regular projection admit alternating diagrams · Crossing number of a link · The crossing number is an isotopy invariant · Crossing number zero from a crossing-free representative · Regular projections of isotopic links bound the crossing number · A link's own regular projection bounds its crossing number · Finiteness of the crossing number · Admitting an alternating diagram is an isotopy invariant · Ropelength of a parametrized link · Ropelength is an isotopy invariant · Ropelength is at most the ratio of any isotopic link · Ropelength is at most the ropelength ratio · Isotopic knots give isotopic one-component links · Two-component link isotopy agrees with labeled link isotopy · Alternating link types have finite crossing number

DefinitionTrace of a parametrized link#✓fully proved

The trace of a parametrized link \(L\) in Euclidean 3-space is the union of the images of its component curves: the set of all points \(\gamma(t)\), where \(\gamma\) is a component of \(L\) and \(t \in \mathbb{R}\).

def ParametrizedLink.trace {n : ℕ} (L : ParametrizedLink n) : Set R3 :=
  ⋃ i, Set.range (L.component i).curve
Uses 3 · Used by 2
Statement usesEuclidean 3-space · Parametrized knot · Parametrized link
Used byThe projected trace is the union of the projected components · Ropelength ratio of a parametrized link

DefinitionTotal contour length of a parametrized link#✓fully proved

Let \(L\) be a parametrized link in Euclidean 3-space with components \(\gamma_1, \dots, \gamma_n\), each a \(2\pi\)-periodic curve. The total contour length of \(L\) is the sum over all components \(\gamma_i\) of the contour length of \(\gamma_i\) on one period \([0, 2\pi]\). It is a value in \([0, \infty]\).

noncomputable def ParametrizedLink.totalContourLength {n : ℕ}
    (L : ParametrizedLink n) : ENNReal :=
  ∑ i, contourLength (L.component i).curve 0 (2 * Real.pi)
Uses 4 · Used by 1
Statement usesEuclidean 3-space · Contour length · Parametrized knot · Parametrized link
Used byRopelength ratio of a parametrized link

DefinitionRopelength ratio of a parametrized link#✓fully proved

For a parametrized link \(L\), the ropelength ratio of \(L\) is its total contour length divided by the thickness of its trace (the union of the images of its components), a value in \([0, \infty]\) computed with the division of \([0, \infty]\).

noncomputable def ParametrizedLink.ropelengthRatio {n : ℕ}
    (L : ParametrizedLink n) : ENNReal :=
  L.totalContourLength / thickness L.trace
Uses 4 · Used by 4
Statement usesThickness · Parametrized link · Total contour length of a parametrized link · Trace of a parametrized link
Used byRopelength of a parametrized link · Ropelength is an isotopy invariant · Ropelength is at most the ratio of any isotopic link · Ropelength is at most the ropelength ratio

DefinitionRopelength of a parametrized link#✓fully proved

For a parametrized link \(L\) with \(n\) components, the ropelength of \(L\) is the infimum, in \([0, \infty]\), of the ropelength ratios of all parametrized links \(L'\) with \(n\) components that are isotopic to \(L\). It is the ropelength of the oriented, labeled ambient-isotopy type of \(L\).

noncomputable def ParametrizedLink.ropelength {n : ℕ}
    (L : ParametrizedLink n) : ENNReal :=
  ⨅ L' : ParametrizedLink n, ⨅ _ : L'.Isotopic L, L'.ropelengthRatio
Uses 3 · Used by 10
Statement usesParametrized link · Isotopy of parametrized links · Ropelength ratio of a parametrized link
Used byRopelength of a parametrized knot · Ropelength is an isotopy invariant · Ropelength is at most the ratio of any isotopic link · Ropelength is at most the ropelength ratio · Admissible constants for the tight-knot inequality · Admissible constants for the tight alternating knot inequality · Zero is an admissible alternating constant · Zero is an admissible tight-knot constant · Admissible alternating constants are downward closed among nonnegative reals · Admissibility passes to smaller nonnegative constants

TheoremRopelength is at most the ratio of any isotopic link#✓fully proved

Let \(L\) and \(L'\) be parametrized links with \(n\) components. If \(L'\) is isotopic to \(L\), then the ropelength of \(L\) is at most the ropelength ratio of \(L'\).

theorem ParametrizedLink.ropelength_le_ratio_of_isotopic {n : ℕ}
    {L L' : ParametrizedLink n} (h : L'.Isotopic L) :
    L.ropelength ≤ L'.ropelengthRatio
Uses 4 · Used by 2
Statement usesParametrized link · Isotopy of parametrized links · Ropelength of a parametrized link · Ropelength ratio of a parametrized link
Used byRopelength is an isotopy invariant · Ropelength is at most the ropelength ratio

TheoremRopelength is at most the ropelength ratio#✓fully proved

For every parametrized link \(L\) with \(n\) components, the ropelength of \(L\) is at most the ropelength ratio of \(L\).

theorem ParametrizedLink.ropelength_le_ratio_self {n : ℕ}
    (L : ParametrizedLink n) : L.ropelength ≤ L.ropelengthRatio
Uses 11
Statement usesParametrized link · Ropelength of a parametrized link · Ropelength ratio of a parametrized link
Proof usesEuclidean 3-space · Smooth ambient isotopy of Euclidean 3-space · Identity ambient isotopy · Orientation-preserving reparametrization of the circle · Identity reparametrization of the circle · Parametrized knot · Isotopy of parametrized links · Ropelength is at most the ratio of any isotopic link

TheoremRopelength is an isotopy invariant#✓fully proved

Let \(L_1\) and \(L_2\) be parametrized links with \(n\) components. If \(L_1\) is isotopic to \(L_2\) (by an oriented, labeled ambient isotopy), then the ropelength of \(L_1\) equals the ropelength of \(L_2\).

theorem ParametrizedLink.ropelength_eq_of_isotopic {n : ℕ}
    {L₁ L₂ : ParametrizedLink n} (h : L₁.Isotopic L₂) :
    L₁.ropelength = L₂.ropelength
Uses 13
Statement usesParametrized link · Isotopy of parametrized links · Ropelength of a parametrized link
Proof usesEuclidean 3-space · Smooth ambient isotopy of Euclidean 3-space · Composition of ambient isotopies · Inverse ambient isotopy · Orientation-preserving reparametrization of the circle · Composition of circle reparametrizations · Inverse circle reparametrization · Parametrized knot · Ropelength ratio of a parametrized link · Ropelength is at most the ratio of any isotopic link

A parametrized knot \(K\) determines the parametrized link with one component, whose single component is \(K\); the pairwise disjointness condition holds trivially.

def ParametrizedKnot.toLink (K : ParametrizedKnot) : ParametrizedLink 1 where
  component := fun _ => K
  pairwiseDisjoint := by
    intro i _ j _ hij
    exact (hij (Subsingleton.elim i j)).elim
Uses 3 · Used by 2
Statement usesEuclidean 3-space · Parametrized knot · Parametrized link
Used byRopelength of a parametrized knot · Isotopic knots give isotopic one-component links

If \(K_1\) and \(K_2\) are parametrized knots and \(K_1\) is isotopic to \(K_2\), then the one-component parametrized link of \(K_1\) is isotopic to the one-component parametrized link of \(K_2\).

theorem ParametrizedKnot.Isotopic.toLink {K₁ K₂ : ParametrizedKnot}
    (h : K₁.Isotopic K₂) : K₁.toLink.Isotopic K₂.toLink
Uses 8
Statement usesParametrized knot · Isotopy of parametrized knots · Parametrized knot as a one-component link · Isotopy of parametrized links
Proof usesEuclidean 3-space · Smooth ambient isotopy of Euclidean 3-space · Orientation-preserving reparametrization of the circle · Parametrized link

DefinitionRopelength of a parametrized knot#✓fully proved

The ropelength of a parametrized knot \(K\) is the ropelength of the one-component parametrized link determined by \(K\): the infimum, in \([0, \infty]\), of the ropelength ratios of all one-component parametrized links that are isotopic to the one-component link of \(K\).

noncomputable def ParametrizedKnot.ropelength (K : ParametrizedKnot) :
    ENNReal :=
  K.toLink.ropelength
Uses 3
Statement usesParametrized knot · Parametrized knot as a one-component link · Ropelength of a parametrized link

AbbreviationEuclidean space \(\mathbb{R}^3\)#✓fully proved

The ambient space of the knots here is \(\mathbb{R}^3\) with its standard Euclidean inner product.

abbrev R3 : Type := EuclideanSpace ℝ (Fin 3)
Used by 43
Used byDistortion ratio · Pardon's lower bound for the distortion of torus knots · Speed of a knot · Standard torus curve · Smooth ambient isotopy of \(\mathbb{R}^3\) · Tracing a strand through one crossing · Polyline closure of a braid word · Chiral knot · The Conway knot · Smooth representative of a PL knot · Image of a PL knot · Local flatness at a boundary point · Local flatness at an interior point · Simple PL knot · Ambient isotopy of oriented knots · Ambient isotopy of oriented two-component links · Oriented smooth knot · Knots are the same as parametrized knots · Isotopy of knots agrees with isotopy of parametrized knots · Point from three coordinates · Model half-plane · Model interior \(2\)-plane · Euclidean ambient isotopies as Conway-knot ambient isotopies · Parametrized knots as knots · Labeled two-component links as two-component links · One pass of the braid closure · Parametrization of a closed polyline · PL knot (closed polyline) · Reflection in the \(xy\)-plane · Smoothly slice (smooth knot version) · Braid closure traversal state · Conway-knot ambient isotopies as Euclidean ambient isotopies · Knots as parametrized knots · Two-component links as labeled links · Topological ambient isotopy · Topologically slice (smooth knot version) · Two-component link · Two-component link isotopy agrees with labeled link isotopy · Topological ambient isotopy of subsets · Closed upper half-space · Quadrisecant of a knot · Unknotted knot · Standard circle

StructureOriented smooth knot#✓fully proved

An oriented smooth knot in \(\mathbb{R}^3\) is a smooth map \(\gamma : \mathbb{R} \to \mathbb{R}^3\) that is \(2\pi\)-periodic, injective on \([0, 2\pi)\), and an immersion, meaning \(\gamma'(t) \ne 0\) for every real \(t\). The orientation is the one induced by the parametrization.

structure Knot where
  /-- The parametrizing map. -/
  curve : ℝ → R3
  /-- The map is smooth. -/
  smooth : ContDiff ℝ (⊤ : ℕ∞) curve
  /-- The map has period `2π`. -/
  periodic : ∀ t, curve (t + 2 * Real.pi) = curve t
  /-- The map is injective on a fundamental period. -/
  injOn : Set.InjOn curve (Set.Ico 0 (2 * Real.pi))
  /-- The map is an immersion (its derivative is everywhere nonzero). -/
  immersion : ∀ t, deriv curve t ≠ 0
Uses 1 · Used by 28
Statement usesEuclidean space \(\mathbb{R}^3\)
Used byDistortion of a knot · Distortion ratio · Intrinsic distance on a knot · Arc length between two parameters · Pardon's lower bound for the distortion of torus knots · Speed of a knot · Total arc length of a knot · Existence of a chiral knot · Chiral knot · Existence of non-isotopic knots · Smooth representative of a PL knot · Ambient isotopy of oriented knots · Ambient isotopy of oriented two-component links · Knots are the same as parametrized knots · Isotopy of knots agrees with isotopy of parametrized knots · Parametrized knots as knots · Labeled two-component links as two-component links · Smoothly slice (smooth knot version) · Smoothly slice (PL knot version) · Knots as parametrized knots · Two-component links as labeled links · Topologically slice (smooth knot version) · Topologically slice (PL knot version) · Two-component link · Two-component link isotopy agrees with labeled link isotopy · Quadrisecant of a knot · Unknotted knot · Quadrisecant theorem (Pannwitz–Kuperberg)

An oriented two-component smooth link in \(\mathbb{R}^3\) is a pair \((K, L)\) of oriented smooth knots whose images in \(\mathbb{R}^3\) are disjoint.

structure TwoLink where
  /-- The first component. -/
  K : Knot
  /-- The second component. -/
  L : Knot
  /-- The two components have disjoint images in `ℝ³`. -/
  disjoint : Disjoint (Set.range K.curve) (Set.range L.curve)
Uses 2 · Used by 5
Statement usesOriented smooth knot · Euclidean space \(\mathbb{R}^3\)
Used byNon-isotopic two-component links exist · Ambient isotopy of oriented two-component links · Labeled two-component links as two-component links · Two-component links as labeled links · Two-component link isotopy agrees with labeled link isotopy

StructureSmooth ambient isotopy of \(\mathbb{R}^3\)#✓fully proved

A smooth ambient isotopy of \(\mathbb{R}^3\) consists of two families of maps \(H_t, G_t \colon \mathbb{R}^3 \to \mathbb{R}^3\) indexed by \(t \in \mathbb{R}\) such that \((t, x) \mapsto H_t(x)\) and \((t, x) \mapsto G_t(x)\) are smooth (\(C^\infty\)) maps \(\mathbb{R} \times \mathbb{R}^3 \to \mathbb{R}^3\), \(G_t\) is a two-sided inverse of \(H_t\) for every \(t\), and \(H_0\) is the identity. In particular every \(H_t\) is a diffeomorphism of \(\mathbb{R}^3\).

MathlibExt.Topology.ConwayKnotShared.KnotTheory.AmbientIsotopy · 15 lines 
structure AmbientIsotopy where
  /-- The forward family. -/
  H : ℝ → R3 → R3
  /-- The inverse family. -/
  Hinv : ℝ → R3 → R3
  /-- The forward family is jointly smooth in `(t, x)`. -/
  smooth : ContDiff ℝ (⊤ : ℕ∞) (Function.uncurry H)
  /-- The inverse family is jointly smooth in `(t, x)`. -/
  smooth_inv : ContDiff ℝ (⊤ : ℕ∞) (Function.uncurry Hinv)
  /-- `Hinv t` is a left inverse of `H t`. -/
  inv_left : ∀ t x, Hinv t (H t x) = x
  /-- `Hinv t` is a right inverse of `H t`. -/
  inv_right : ∀ t x, H t (Hinv t x) = x
  /-- The isotopy starts at the identity. -/
  start : H 0 = id
Uses 1 · Used by 8
Statement usesEuclidean space \(\mathbb{R}^3\)
Used byPardon's lower bound for the distortion of torus knots · Chiral knot · Ambient isotopy of oriented knots · Ambient isotopy of oriented two-component links · Isotopy of knots agrees with isotopy of parametrized knots · Euclidean ambient isotopies as Conway-knot ambient isotopies · Conway-knot ambient isotopies as Euclidean ambient isotopies · Two-component link isotopy agrees with labeled link isotopy

DefinitionAmbient isotopy of oriented knots#✓fully proved

Let \(K_1\) and \(K_2\) be oriented knots, each given by its \(2\pi\)-periodic parametrization. They are ambient-isotopic if there are a smooth ambient isotopy \((\Phi_t)_{t \in \mathbb{R}}\) of \(\mathbb{R}^3\) and an orientation-preserving smooth reparametrization \(\sigma\) of the circle such that \(\Phi_1(K_1(t)) = K_2(\sigma(t))\) for every real \(t\). Here an orientation-preserving smooth reparametrization of the circle is a smooth, strictly increasing bijection \(\sigma : \mathbb{R} \to \mathbb{R}\) with smooth inverse such that \(\sigma(t + 2\pi) = \sigma(t) + 2\pi\) for every \(t\).

def Knot.Isotopic (K₁ K₂ : Knot) : Prop :=
  ∃ Φ : AmbientIsotopy, ∃ σ : CircleReparam, ∀ t, Φ.H 1 (K₁.curve t) = K₂.curve (σ.f t)
Uses 3 · Used by 3
Statement usesSmooth ambient isotopy of \(\mathbb{R}^3\) · Oriented smooth knot · Euclidean space \(\mathbb{R}^3\)
Used byExistence of non-isotopic knots · Isotopy of knots agrees with isotopy of parametrized knots · Unknotted knot

DefinitionAmbient isotopy of oriented two-component links#✓fully proved

Let \(L = (K, J)\) and \(L' = (K', J')\) be oriented two-component links, each knot given by its \(2\pi\)-periodic parametrization. Then \(L\) and \(L'\) are ambient-isotopic if there are a smooth ambient isotopy \((\Phi_t)_{t \in \mathbb{R}}\) of \(\mathbb{R}^3\) and orientation-preserving smooth reparametrizations \(\sigma\), \(\tau\) of the circle such that \(\Phi_1(K(t)) = K'(\sigma(t))\) and \(\Phi_1(J(t)) = J'(\tau(t))\) for every real \(t\). Here an orientation-preserving smooth reparametrization of the circle is a smooth, strictly increasing bijection \(\sigma : \mathbb{R} \to \mathbb{R}\) with smooth inverse such that \(\sigma(t + 2\pi) = \sigma(t) + 2\pi\) for every \(t\).

def TwoLink.Isotopic (L₁ L₂ : TwoLink) : Prop :=
  ∃ Φ : AmbientIsotopy, ∃ σ τ : CircleReparam,
    (∀ t, Φ.H 1 (L₁.K.curve t) = L₂.K.curve (σ.f t)) ∧
    (∀ t, Φ.H 1 (L₁.L.curve t) = L₂.L.curve (τ.f t))
Uses 4 · Used by 2
Statement usesSmooth ambient isotopy of \(\mathbb{R}^3\) · Oriented smooth knot · Euclidean space \(\mathbb{R}^3\) · Two-component link
Used byNon-isotopic two-component links exist · Two-component link isotopy agrees with labeled link isotopy

DefinitionReflection in the \(xy\)-plane#✓fully proved

The reflection of \(\mathbb{R}^3\) through the \(xy\)-plane is the map \((x, y, z) \mapsto (x, y, -z)\).

def reflectZ (p : R3) : R3 :=
  WithLp.toLp 2 (fun i : Fin 3 => if i = 2 then -p.ofLp i else p.ofLp i)
Uses 1 · Used by 1
Statement usesEuclidean space \(\mathbb{R}^3\)
Used byChiral knot

DefinitionChiral knot#✓fully proved

Let \(K \colon \mathbb{R} \to \mathbb{R}^3\) be an oriented smooth knot, and let \(\rho(x, y, z) = (x, y, -z)\) be the reflection of \(\mathbb{R}^3\) through the \(xy\)-plane. Call \(\sigma \colon \mathbb{R} \to \mathbb{R}\) an orientation-preserving reparametrization of the circle if it is a strictly increasing smooth bijection with smooth inverse satisfying \(\sigma(t + 2\pi) = \sigma(t) + 2\pi\) for all \(t \in \mathbb{R}\), that is, the lift of an orientation-preserving diffeomorphism of \(\mathbb{R} / 2\pi\mathbb{Z}\). The knot \(K\) is chiral if there is no smooth ambient isotopy \((H_t)\) of \(\mathbb{R}^3\) together with such a \(\sigma\) satisfying \(H_1(K(t)) = \rho(K(\sigma(t)))\) for all \(t \in \mathbb{R}\). Equivalently, \(K\) is not ambient isotopic, as an oriented knot, to its mirror image \(\rho \circ K\).

def Knot.Chiral (K : Knot) : Prop :=
  ¬ ∃ Φ : AmbientIsotopy, ∃ σ : CircleReparam,
    ∀ t, Φ.H 1 (K.curve t) = reflectZ (K.curve (σ.f t))
Uses 4 · Used by 1
Statement usesSmooth ambient isotopy of \(\mathbb{R}^3\) · Oriented smooth knot · Euclidean space \(\mathbb{R}^3\) · Reflection in the \(xy\)-plane
Used byExistence of a chiral knot

StructureTopological ambient isotopy#✓fully proved

A topological ambient isotopy of \(\mathbb{R}^3\) is a family of maps \(H_t : \mathbb{R}^3 \to \mathbb{R}^3\), indexed by \(t \in \mathbb{R}\), together with a family \(G_t : \mathbb{R}^3 \to \mathbb{R}^3\) such that \((t, x) \mapsto H_t(x)\) and \((t, x) \mapsto G_t(x)\) are continuous, \(G_t\) is a two-sided inverse of \(H_t\) for every \(t\) (so each \(H_t\) is a homeomorphism of \(\mathbb{R}^3\)), and \(H_0\) is the identity.

The time domain is all of \(\mathbb{R}\), but only \(H_0\) and \(H_1\) matter for the isotopy relation.

MathlibExt.Topology.ConwayKnotShared.KnotTheory.TopAmbientIsotopy · 15 lines 
structure TopAmbientIsotopy where
  /-- The forward family. -/
  H : ℝ → R3 → R3
  /-- The inverse family. -/
  Hinv : ℝ → R3 → R3
  /-- The forward family is jointly continuous in `(t, x)`. -/
  continuous : Continuous (Function.uncurry H)
  /-- The inverse family is jointly continuous in `(t, x)`. -/
  continuous_inv : Continuous (Function.uncurry Hinv)
  /-- `Hinv t` is a left inverse of `H t`. -/
  inv_left : ∀ t x, Hinv t (H t x) = x
  /-- `Hinv t` is a right inverse of `H t`. -/
  inv_right : ∀ t x, H t (Hinv t x) = x
  /-- The isotopy starts at the identity. -/
  start : H 0 = id
Uses 1 · Used by 1
Statement usesEuclidean space \(\mathbb{R}^3\)
Used byTopological ambient isotopy of subsets

DefinitionTopological ambient isotopy of subsets#✓fully proved

Two subsets \(A\) and \(B\) of \(\mathbb{R}^3\) are unoriented topologically ambient isotopic if there is a topological ambient isotopy \((H_t)\) of \(\mathbb{R}^3\) whose time-one map carries \(A\) onto \(B\), that is, \(H_1(A) = B\).

"Unoriented" because this is a set-level relation that forgets any parametrization.

def Set.UnorientedTopAmbIsotopic (A B : Set R3) : Prop :=
  ∃ Φ : TopAmbientIsotopy, Φ.H 1 '' A = B
Uses 2 · Used by 1
Statement usesEuclidean space \(\mathbb{R}^3\) · Topological ambient isotopy
Used bySmooth representative of a PL knot

AbbreviationClosed unit disk in the plane#✓fully proved

The closed unit Euclidean disk \(\{(x, y) \in \mathbb{R} \times \mathbb{R} \mid x^2 + y^2 \le 1\}\), the source of the parametrization of a slicing disk.

The disk and its boundary circle are written out by the equations \(x^2 + y^2 \le 1\) and \(x^2 + y^2 = 1\) rather than as the closed unit ball and unit sphere of \(\mathbb{R} \times \mathbb{R}\). The product carries the sup norm, so that ball would be the square \([-1, 1]^2\) and that sphere its boundary, which has corners. At a corner, no smooth map with injective derivative can match a corner-free smooth knot as its boundary, so slice disks parametrized by the square cannot exist, and every knot would fail to be smoothly slice.

abbrev disk2 : Set (ℝ × ℝ) := {p | p.1 ^ 2 + p.2 ^ 2 ≤ 1}
Used by 4
Used byLocal flatness at a boundary point · Local flatness at an interior point · Smoothly slice (smooth knot version) · Topologically slice (smooth knot version)

AbbreviationUnit circle in the plane#✓fully proved

The unit Euclidean circle \(\{(x, y) \in \mathbb{R} \times \mathbb{R} \mid x^2 + y^2 = 1\}\), the source of the boundary of a slicing disk.

abbrev circle1 : Set (ℝ × ℝ) := {p | p.1 ^ 2 + p.2 ^ 2 = 1}
Used by 2
Used bySmoothly slice (smooth knot version) · Topologically slice (smooth knot version)

DefinitionClosed upper half-space#✓fully proved

The closed upper half-space in \(\mathbb{R}^3 \times \mathbb{R}\) is the set \(\mathbb{R}^3 \times [0, \infty)\) of points \((x, s)\) with \(s \ge 0\).

We identify \(\mathbb{R}^3 \times [0, \infty)\) with \(B^4 \setminus \{\mathrm{pt}\}\), so slice disks live here.

def upperHalf : Set (R3 × ℝ) := { q | 0 ≤ q.2 }
Uses 1 · Used by 1
Statement usesEuclidean space \(\mathbb{R}^3\)
Used byLocal flatness at a boundary point

DefinitionModel interior \(2\)-plane#✓fully proved

The model interior \(2\)-plane in \(\mathbb{R}^3 \times \mathbb{R}\) is the set of points \(((x_1, x_2, x_3), t)\) with \(x_2 = x_3 = 0\), where \(x_1\) and \(t\) are arbitrary. It is the local model for interior local flatness of an embedded \(2\)-disk.

def modelPlane2 : Set (R3 × ℝ) := { q | q.1 1 = 0 ∧ q.1 2 = 0 }
Uses 1 · Used by 1
Statement usesEuclidean space \(\mathbb{R}^3\)
Used byLocal flatness at an interior point

DefinitionModel half-plane#✓fully proved

The model half-plane is the set of pairs \(((p_1, p_2, p_3), s)\) in \(\mathbb{R}^3 \times \mathbb{R}\) with \(p_2 = p_3 = 0\) and \(s \ge 0\). It is a copy of the closed half-plane \(\mathbb{R} \times [0, \infty)\), with coordinates \(p_1\) and \(s\), lying in the upper half-space \(s \ge 0\).

It is the local model for boundary local flatness of a properly embedded disk.

def modelHalfPlane2 : Set (R3 × ℝ) := { q | q.1 1 = 0 ∧ q.1 2 = 0 ∧ 0 ≤ q.2 }
Uses 1 · Used by 1
Statement usesEuclidean space \(\mathbb{R}^3\)
Used byLocal flatness at a boundary point

DefinitionSmoothly slice (smooth knot version)#✓fully proved

Let \(\Delta = \{(x, y) \in \mathbb{R}^2 : x^2 + y^2 \le 1\}\) be the closed unit disk and \(C = \{(x, y) \in \mathbb{R}^2 : x^2 + y^2 = 1\}\) its boundary circle. A smooth knot \(K\) is smoothly slice if there is a smooth (\(C^\infty\)) map \(f : \mathbb{R}^2 \to \mathbb{R}^3 \times \mathbb{R}\) such that \(f\) is injective on \(\Delta\); for every \(p \in \Delta\) the last coordinate of \(f(p)\) is nonnegative, and it is \(0\) exactly when \(p \in C\); the derivative of \(f\) at every point of \(\Delta\) is injective; and the image of \(C\) under the \(\mathbb{R}^3\)-component of \(f\) is the image of \(K\).

def Knot.SmoothlySlice (K : Knot) : Prop :=
  ∃ D : ℝ × ℝ → R3 × ℝ,
    ContDiff ℝ (⊤ : ℕ∞) D ∧
    Set.InjOn D disk2 ∧
    (∀ p ∈ disk2, 0 ≤ (D p).2) ∧
    (∀ p ∈ disk2, (D p).2 = 0 ↔ p ∈ circle1) ∧
    (∀ p ∈ disk2, Function.Injective (fderiv ℝ D p)) ∧
    (fun p => (D p).1) '' circle1 = Set.range K.curve
Uses 4 · Used by 1
Statement usesOriented smooth knot · Euclidean space \(\mathbb{R}^3\) · Unit circle in the plane · Closed unit disk in the plane
Used bySmoothly slice (PL knot version)

DefinitionLocal flatness at an interior point#✓fully proved

Let \(q \in \mathbb{R}^3 \times \mathbb{R}\) and \(D : \mathbb{R}^2 \to \mathbb{R}^3 \times \mathbb{R}\). Write \(\Delta = \{(x, y) : x^2 + y^2 \le 1\}\) for the closed unit disk and \(P = \{((p_1, p_2, p_3), s) : p_2 = p_3 = 0\}\) for the model plane. The image \(D(\Delta)\) is locally flat at \(q\) in the interior sense if there is a homeomorphism \(h : U \to V\) between open subsets \(U\), \(V\) of \(\mathbb{R}^3 \times \mathbb{R}\) such that \(q \in U\) and \(h(U \cap D(\Delta)) = V \cap P\).

def IsLocallyFlatInterior (D : ℝ × ℝ → R3 × ℝ) (q : R3 × ℝ) : Prop :=
  ∃ h : OpenPartialHomeomorph (R3 × ℝ) (R3 × ℝ),
    q ∈ h.source ∧
    h.toFun '' (h.source ∩ D '' disk2) = h.target ∩ modelPlane2
Uses 3 · Used by 1
Statement usesEuclidean space \(\mathbb{R}^3\) · Closed unit disk in the plane · Model interior \(2\)-plane
Used byTopologically slice (smooth knot version)

DefinitionLocal flatness at a boundary point#✓fully proved

Let \(q \in \mathbb{R}^3 \times \mathbb{R}\) and \(D : \mathbb{R}^2 \to \mathbb{R}^3 \times \mathbb{R}\). Write \(\Delta = \{(x, y) : x^2 + y^2 \le 1\}\) for the closed unit disk, \(H = \{(p, s) : s \ge 0\}\) for the closed upper half-space, and \(P = \{((p_1, p_2, p_3), s) : p_2 = p_3 = 0,\ s \ge 0\}\) for the model half-plane. The image \(D(\Delta)\) is locally flat at \(q\) in the boundary sense if there is a homeomorphism \(h : U \to V\) between open subsets \(U\), \(V\) of \(\mathbb{R}^3 \times \mathbb{R}\) such that \(q \in U\), \(h(U \cap H) = V \cap H\) and \(h(U \cap D(\Delta)) = V \cap P\).

The chart is open in \(\mathbb{R}^3 \times \mathbb{R}\) rather than in \(H\): when the last coordinate of \(q\) is \(0\), every open neighbourhood of \(q\) leaves \(H\).

def IsLocallyFlatBoundary (D : ℝ × ℝ → R3 × ℝ) (q : R3 × ℝ) : Prop :=
  ∃ h : OpenPartialHomeomorph (R3 × ℝ) (R3 × ℝ),
    q ∈ h.source ∧
    h.toFun '' (h.source ∩ upperHalf) = h.target ∩ upperHalf ∧
    h.toFun '' (h.source ∩ D '' disk2) = h.target ∩ modelHalfPlane2
Uses 4 · Used by 1
Statement usesEuclidean space \(\mathbb{R}^3\) · Closed unit disk in the plane · Model half-plane · Closed upper half-space
Used byTopologically slice (smooth knot version)

DefinitionTopologically slice (smooth knot version)#✓fully proved

Write points of \(\mathbb{R}^3 \times \mathbb{R}\) as \((x, s)\) with \(x = (x_1, x_2, x_3)\). Let \(H = \{(x, s) : s \ge 0\}\) be the closed upper half-space, \(P = \{(x, s) : x_2 = x_3 = 0\}\) the model plane and \(P_+ = P \cap H\) the model half-plane, and let \(D^2 = \{(a, b) \in \mathbb{R}^2 : a^2 + b^2 \le 1\}\) and \(S^1 = \{(a, b) \in \mathbb{R}^2 : a^2 + b^2 = 1\}\). A smooth knot \(K\) is topologically slice if there is a continuous map \(D : \mathbb{R}^2 \to \mathbb{R}^3 \times \mathbb{R}\), injective on \(D^2\), such that: for every \(p \in D^2\) the last coordinate of \(D(p)\) is nonnegative, and it is \(0\) exactly when \(p \in S^1\); for every \(p \in D^2 \setminus S^1\) there is a homeomorphism \(h : U \to V\) between open subsets of \(\mathbb{R}^3 \times \mathbb{R}\) with \(D(p) \in U\) and \(h(U \cap D(D^2)) = V \cap P\); for every \(p \in S^1\) there is such a homeomorphism with \(D(p) \in U\), \(h(U \cap H) = V \cap H\) and \(h(U \cap D(D^2)) = V \cap P_+\); and the image of \(S^1\) under the \(\mathbb{R}^3\)-component of \(D\) is the image of \(K\).

def Knot.TopologicallySlice (K : Knot) : Prop :=
  ∃ D : ℝ × ℝ → R3 × ℝ,
    Continuous D ∧
    Set.InjOn D disk2 ∧
    (∀ p ∈ disk2, 0 ≤ (D p).2) ∧
    (∀ p ∈ disk2, (D p).2 = 0 ↔ p ∈ circle1) ∧
    (∀ p ∈ disk2 \ circle1, IsLocallyFlatInterior D (D p)) ∧
    (∀ p ∈ circle1, IsLocallyFlatBoundary D (D p)) ∧
    (fun p => (D p).1) '' circle1 = Set.range K.curve
Uses 6 · Used by 1
Statement usesLocal flatness at a boundary point · Local flatness at an interior point · Oriented smooth knot · Euclidean space \(\mathbb{R}^3\) · Unit circle in the plane · Closed unit disk in the plane
Used byTopologically slice (PL knot version)

DefinitionParametrization of a closed polyline#✓fully proved

Let \(v_0, \dots, v_{n-1}\) be a list of \(n \ge 1\) points of \(\mathbb{R}^3\). The polyline curve is the \(n\)-periodic map \(\gamma : \mathbb{R} \to \mathbb{R}^3\) with \(\gamma(k + \alpha) = (1 - \alpha) v_k + \alpha v_{k+1}\) for integers \(0 \le k < n\) and reals \(0 \le \alpha < 1\), where indices are taken modulo \(n\) (so \(v_n = v_0\)). For the empty list the curve is constantly \(0\).

noncomputable def plCurve (vertices : List R3) (t : ℝ) : R3 :=
  if h : vertices.length = 0 then 0
  else
    let n : ℕ := vertices.length
    let s : ℝ := t - (n : ℝ) * Int.floor (t / (n : ℝ))
    let k : ℕ := (Int.floor s).toNat
    let α : ℝ := s - k
    (1 - α) • vertices[k % n]'(Nat.mod_lt _ (Nat.pos_of_ne_zero h)) +
      α • vertices[(k + 1) % n]'(Nat.mod_lt _ (Nat.pos_of_ne_zero h))
Uses 1 · Used by 2
Statement usesEuclidean space \(\mathbb{R}^3\)
Used byImage of a PL knot · Simple PL knot

StructurePL knot (closed polyline)#✓fully proved

A PL knot is a list \(v_0, \dots, v_{n-1}\) of points of \(\mathbb{R}^3\) with \(n \ge 3\), viewed as the vertices, in order, of the closed polyline with edges from \(v_i\) to \(v_{i+1}\) for \(i < n - 1\) and from \(v_{n-1}\) back to \(v_0\).

Simplicity of the polyline (that it is an embedded closed curve) is not part of the data; it is imposed as a separate condition.

structure PLKnot where
  /-- The ordered list of polyline vertices. -/
  vertices : List R3
  /-- A closed polyline needs at least three vertices to be non-degenerate. -/
  three_le : 3 ≤ vertices.length
Uses 1 · Used by 7
Statement usesEuclidean space \(\mathbb{R}^3\)
Used byThe Conway knot · Smooth representative of a PL knot · Image of a PL knot · Simple PL knot · Smoothly slice (PL knot version) · Topologically slice (PL knot version) · A topologically slice knot that is not smoothly slice

DefinitionImage of a PL knot#✓fully proved

Let \(K\) be a PL knot with vertices \(v_0, \dots, v_{n-1}\). Its image is the subset of \(\mathbb{R}^3\) traced by the closed polyline through these vertices: the image of the half-open interval \([0, n)\) under the parametrization that sends \(k + \alpha\), for an integer \(0 \le k < n\) and a real \(0 \le \alpha < 1\), to \((1 - \alpha) v_k + \alpha v_{k+1}\), with indices taken modulo \(n\).

def PLKnot.image (K : PLKnot) : Set R3 :=
  plCurve K.vertices '' Set.Ico (0 : ℝ) (K.vertices.length : ℝ)
Uses 3 · Used by 1
Statement usesPL knot (closed polyline) · Euclidean space \(\mathbb{R}^3\) · Parametrization of a closed polyline
Used bySmooth representative of a PL knot

DefinitionSimple PL knot#✓fully proved

A PL knot \(K\) with vertices \(v_0, \dots, v_{n-1}\) is simple if its closed polyline parametrization, which sends \(k + \alpha\), for an integer \(0 \le k < n\) and a real \(0 \le \alpha < 1\), to \((1 - \alpha) v_k + \alpha v_{k+1}\) (indices modulo \(n\)), is injective on the half-open interval \([0, n)\).

Equivalently, the polyline is a simple closed curve: all vertices are distinct, non-adjacent edges are disjoint, and adjacent edges meet only at their shared vertex.

def PLKnot.IsSimple (K : PLKnot) : Prop :=
  ∀ s t : ℝ,
    s ∈ Set.Ico (0 : ℝ) (K.vertices.length : ℝ) →
    t ∈ Set.Ico (0 : ℝ) (K.vertices.length : ℝ) →
    plCurve K.vertices s = plCurve K.vertices t →
    s = t
Uses 3 · Used by 1
Statement usesPL knot (closed polyline) · Euclidean space \(\mathbb{R}^3\) · Parametrization of a closed polyline
Used byThe Conway knot polyline is a simple closed curve

DefinitionSmooth representative of a PL knot#✓fully proved

A smooth knot \(J\) is a smooth representative of the piecewise-linear knot \(K\) if the image of \(J\) and the image of \(K\) are unoriented topologically ambient isotopic in \(\mathbb{R}^3\): some topological ambient isotopy \((H_t)\) of \(\mathbb{R}^3\) satisfies \(H_1(\operatorname{im} J) = \operatorname{im} K\).

When the polyline \(K\) is simple, both curves are tame, and this agrees with the usual relation of having the same smooth/PL knot type.

def PLKnot.HasSmoothRepresentative (K : PLKnot) (J : Knot) : Prop :=
  Set.UnorientedTopAmbIsotopic (Set.range J.curve) K.image
Uses 5 · Used by 2
Statement usesOriented smooth knot · PL knot (closed polyline) · Image of a PL knot · Euclidean space \(\mathbb{R}^3\) · Topological ambient isotopy of subsets
Used bySmoothly slice (PL knot version) · Topologically slice (PL knot version)

DefinitionSmoothly slice (PL knot version)#✓fully proved

A PL knot \(K\) is smoothly slice if there is a smooth knot \(J\) that is smoothly slice and is a smooth representative of \(K\): for some topological ambient isotopy \((H_t)\) of \(\mathbb{R}^3\), the map \(H_1\) carries the image of \(J\) onto the image (trace) of the polyline \(K\).

Piccirillo's theorem that the Conway knot is not smoothly slice is stated with this notion.

def PLKnot.SmoothlySlice (K : PLKnot) : Prop :=
  ∃ J : Knot, K.HasSmoothRepresentative J ∧ J.SmoothlySlice
Uses 4 · Used by 2
Statement usesOriented smooth knot · Smoothly slice (smooth knot version) · PL knot (closed polyline) · Smooth representative of a PL knot
Used byThe Conway knot is not smoothly slice (Piccirillo) · A topologically slice knot that is not smoothly slice

DefinitionTopologically slice (PL knot version)#✓fully proved

A PL knot \(K\) is topologically slice if there is a smooth knot \(J\) that is a smooth representative of \(K\), meaning that the image of \(J\) and the image of \(K\) are unoriented topologically ambient isotopic subsets of \(\mathbb{R}^3\), and such that \(J\) is topologically slice as a smooth knot.

def PLKnot.TopologicallySlice (K : PLKnot) : Prop :=
  ∃ J : Knot, K.HasSmoothRepresentative J ∧ J.TopologicallySlice
Uses 4 · Used by 2
Statement usesOriented smooth knot · Topologically slice (smooth knot version) · PL knot (closed polyline) · Smooth representative of a PL knot
Used byThe Conway knot is topologically slice · A topologically slice knot that is not smoothly slice

DefinitionPoint from three coordinates#✓fully proved

For real numbers \(x\), \(y\), \(z\), this is the point \((x, y, z)\) of the Euclidean space \(\mathbb{R}^3\).

noncomputable def mkR3 (x y z : ℝ) : R3 :=
  WithLp.toLp 2 (fun i : Fin 3 =>
    if i.val = 0 then x else if i.val = 1 then y else z)
Uses 1 · Used by 3
Statement usesEuclidean space \(\mathbb{R}^3\)
Used byTracing a strand through one crossing · Polyline closure of a braid word · One pass of the braid closure

StructureBraid closure traversal state#✓fully proved

A traversal state for tracing the closure of a braid consists of the current strand position, a natural number, and the list of points of \(\mathbb{R}^3\) accumulated so far, in order, as vertices of the polyline.

structure State where
  /-- Current strand `x`-position. -/
  pos : ℕ
  /-- Polyline vertices accumulated so far, in order. -/
  vertices : List R3
Uses 1 · Used by 5
Statement usesEuclidean space \(\mathbb{R}^3\)
Used byTracing a strand through one crossing · Tracing a strand through a braid word · Polyline closure of a braid word · Iterated braid-closure passes · One pass of the braid closure

DefinitionTracing a strand through one crossing#✓fully proved

Let a traversal state consist of a current strand position \(p \in \mathbb{N}\) and a list of vertices in \(\mathbb{R}^3\), let \(w \in \mathbb{Z}\) be a braid generator with \(i = |w|\), and let \(z_{\mathrm{top}}, z_{\mathrm{bot}} \in \mathbb{R}\). Put \(z_{\mathrm{hi}} = z_{\mathrm{top}} - (z_{\mathrm{top}} - z_{\mathrm{bot}})/4\) and \(z_{\mathrm{lo}} = z_{\mathrm{bot}} + (z_{\mathrm{top}} - z_{\mathrm{bot}})/4\). The new state is obtained by changing the position and appending the listed points, in order, to the vertex list. If \(p = i\) and \(w > 0\), the new position is \(i + 1\) and the points are \((i, 1, z_{\mathrm{hi}})\), \((i + 1, 1, z_{\mathrm{lo}})\), \((i + 1, 0, z_{\mathrm{bot}})\). If \(p = i\) and \(w \le 0\), the new position is \(i + 1\) and the only point is \((i + 1, 0, z_{\mathrm{bot}})\). If \(p = i + 1\) and \(w > 0\), the new position is \(i\) and the only point is \((i, 0, z_{\mathrm{bot}})\). If \(p = i + 1\) and \(w \le 0\), the new position is \(i\) and the points are \((i + 1, 1, z_{\mathrm{hi}})\), \((i, 1, z_{\mathrm{lo}})\), \((i, 0, z_{\mathrm{bot}})\). Otherwise the position stays \(p\) and the only point is \((p, 0, z_{\mathrm{bot}})\).

The step is meant for \(z_{\mathrm{bot}} < z_{\mathrm{top}}\), with the crossing in the slab between these heights: the strand passing over is lifted to \(y = 1\), and the strand passing under stays at \(y = 0\).

MathlibExt.Topology.ConwayKnotShared.KnotTheory.BraidClosure.applyCrossing · 34 lines 
noncomputable def applyCrossing (state : State) (w : ℤ) (zTop zBot : ℝ) : State :=
  let i : ℕ := w.natAbs
  let p : ℕ := state.pos
  let zMidHi : ℝ := zTop - (zTop - zBot) / 4
  let zMidLo : ℝ := zBot + (zTop - zBot) / 4
  if p = i then
    -- We are at the lower-index strand of the crossing; we swap to position `i + 1`.
    if 0 < w then
      -- σ_i: lower strand goes OVER. Lift to `y = 1`, swap, drop.
      { pos := i + 1
        vertices := state.vertices ++
          [ mkR3 (i : ℝ) 1 zMidHi,
            mkR3 ((i + 1 : ℕ) : ℝ) 1 zMidLo,
            mkR3 ((i + 1 : ℕ) : ℝ) 0 zBot ] }
    else
      -- σ_i⁻¹: lower strand goes UNDER. Stay at `y = 0`, swap.
      { pos := i + 1
        vertices := state.vertices ++ [ mkR3 ((i + 1 : ℕ) : ℝ) 0 zBot ] }
  else if p = i + 1 then
    -- We are at the upper-index strand of the crossing; we swap to position `i`.
    if 0 < w then
      -- σ_i: we are the UNDER strand.
      { pos := i
        vertices := state.vertices ++ [ mkR3 (i : ℝ) 0 zBot ] }
    else
      -- σ_i⁻¹: we are the OVER strand.
      { pos := i
        vertices := state.vertices ++
          [ mkR3 ((i + 1 : ℕ) : ℝ) 1 zMidHi,
            mkR3 (i : ℝ) 1 zMidLo,
            mkR3 (i : ℝ) 0 zBot ] }
  else
    -- Not participating in this crossing; descend straight.
    { state with vertices := state.vertices ++ [ mkR3 (p : ℝ) 0 zBot ] }
Uses 3 · Used by 1
Statement usesBraid closure traversal state · Point from three coordinates · Euclidean space \(\mathbb{R}^3\)
Used byTracing a strand through a braid word

DefinitionTracing a strand through a braid word#✓fully proved

Given a traversal state \(s\), a braid word \(w_0 w_1 \cdots w_{m-1}\) (a list of integers) and a starting index \(k \in \mathbb{N}\), the one-crossing step is applied to the state for each generator in turn, starting from \(s\): the generator \(w_j\) is applied with top height \(-(k + j)\) and bottom height \(-(k + j + 1)\). The result is the final state; for the empty word it is \(s\).

noncomputable def applyWord : State → List ℤ → ℕ → State
  | state, [], _ => state
  | state, w :: ws, k =>
      let state' := applyCrossing state w (-(k : ℝ)) (-((k : ℝ) + 1))
      applyWord state' ws (k + 1)
Uses 2 · Used by 1
Statement usesBraid closure traversal state · Tracing a strand through one crossing
Used byOne pass of the braid closure

DefinitionOne pass of the braid closure#✓fully proved

Let \(w\) be a braid word (a list of integers) of length \(m\). Starting from a traversal state, one pass applies the letters of \(w\) in order as crossings, the \(k\)-th letter (counting from \(0\)) occupying the slab \(-(k+1) \le z \le -k\); this moves the state to a strand position \(p\) and appends the crossing vertices. It then appends the closure arc: the vertices \((p, 100, -m)\) and \((p, 100, 0)\), followed by \((p, 0, 0)\) unless \(p = 1\). The resulting state has position \(p\) and the extended vertex list.

When \(p = 1\) the vertex \((1, 0, 0)\) is left out because the polyline starts there, so the closure arc already returns to its first vertex.

noncomputable def onePass (word : List ℤ) (state : State) : State :=
  let afterBraid := applyWord state word 0
  let m : ℝ := word.length
  let p : ℕ := afterBraid.pos
  let arc :=
    if p = 1 then
      [ mkR3 (p : ℝ) 100 (-m), mkR3 (p : ℝ) 100 0 ]
    else
      [ mkR3 (p : ℝ) 100 (-m), mkR3 (p : ℝ) 100 0, mkR3 (p : ℝ) 0 0 ]
  { pos := p, vertices := afterBraid.vertices ++ arc }
Uses 4 · Used by 1
Statement usesBraid closure traversal state · Tracing a strand through a braid word · Point from three coordinates · Euclidean space \(\mathbb{R}^3\)
Used byIterated braid-closure passes

DefinitionIterated braid-closure passes#✓fully proved

For a braid word \(w\), a number \(f\) of remaining passes and a traversal state \(S\), the iteration returns \(S\) when \(f = 0\). When \(f > 0\) it applies one pass of \(w\) to \(S\), obtaining a state \(S'\); it returns \(S'\) if the strand position of \(S'\) is \(1\), and otherwise iterates on \(S'\) with \(f - 1\) passes remaining.

The bound \(f\) guarantees termination. The braid closure on \(n\) strands uses \(f = n\), since at most \(n\) distinct strand positions are visited.

noncomputable def iterate (word : List ℤ) : ℕ → State → State
  | 0, state => state
  | f + 1, state =>
      let s' := onePass word state
      if s'.pos = 1 then s' else iterate word f s'
Uses 2 · Used by 1
Statement usesBraid closure traversal state · One pass of the braid closure
Used byPolyline closure of a braid word

DefinitionPolyline closure of a braid word#✓fully proved

Let \(n \in \mathbb{N}\), and let \(w = w_0 w_1 \cdots w_{m-1}\) be a braid word (a list of integers, where \(i > 0\) stands for \(\sigma_i\) and \(-i\) for \(\sigma_i^{-1}\)). If \(m = 0\), the value is the junk list \((0, 0, 0)\), \((1, 0, 0)\), \((0, 1, 0)\). Otherwise the value is a list of vertices in \(\mathbb{R}^3\) tracing the closure of \(w\) as one polyline component. It starts at the vertex \((1, 0, 0)\) on strand position \(1\) and makes passes through the braid: in each pass the crossing \(w_j\) occupies the slab between heights \(z = -(j + 1)\) and \(z = -j\), with the strand passing over lifted to \(y = 1\), and each pass is followed by a closure arc through \(y = 100\) back up to height \(z = 0\). Tracing stops as soon as a pass ends at position \(1\), or after \(n\) passes.

The layout is designed for words with \(1 \le |w_j| \le n - 1\) for every \(j\), where the strands sit at the \(x\)-positions \(1, \dots, n\); other words still yield a vertex list, but not a meaningful one.

noncomputable def braidClosure (n : ℕ) (word : List ℤ) : List R3 :=
  if word.length = 0 then
    -- Junk fallback for the empty-word case (no PL data to derive).
    [BraidClosure.mkR3 0 0 0, BraidClosure.mkR3 1 0 0, BraidClosure.mkR3 0 1 0]
  else
    let init : BraidClosure.State :=
      { pos := 1, vertices := [BraidClosure.mkR3 1 0 0] }
    (BraidClosure.iterate word n init).vertices
Uses 4 · Used by 1
Statement usesBraid closure traversal state · Iterated braid-closure passes · Point from three coordinates · Euclidean space \(\mathbb{R}^3\)
Used byThe Conway knot

DefinitionBraid word for the Conway knot#✓fully proved

The braid word \(\sigma_1^{-2} \sigma_2 \sigma_1^{-1} \sigma_2 \sigma_1^{-1} \sigma_3 \sigma_2^{-2} \sigma_3^{2}\) on \(4\) strands, encoded as the list of integers \([-1, -1, 2, -1, 2, -1, 3, -2, -2, 3, 3]\), where an entry \(i > 0\) stands for the generator \(\sigma_i\) and \(-i\) for \(\sigma_i^{-1}\). It has length \(11\) and writhe \(-1\), and is a braid word for the Conway knot 11n34.

def conwayBraidWord : List ℤ := [-1, -1, 2, -1, 2, -1, 3, -2, -2, 3, 3]
Sources
  • KnotInfo's 11n_34 record, braid_notation field. The Knot Atlas records a different but Markov-equivalent presentation for the same knot, [1, 1, 2, -3, 2, 1, -3, -2, -2, -3, -3] (which it labels K11n34, the mirror of the Conway knot); both representations agree on braid index 4, braid length 11, and writhe -1. Sliceness is mirror-invariant, so either braid word is a valid witness for conway_knot_not_smoothly_slice.
Used by 1
Used byThe Conway knot

DefinitionThe Conway knot#✓fully proved

The Conway knot 11n34 as a piecewise-linear closed polyline in \(\mathbb{R}^3\): its vertices are those of the polyline closure, on \(4\) strands, of the braid word \(\sigma_1^{-2} \sigma_2 \sigma_1^{-1} \sigma_2 \sigma_1^{-1} \sigma_3 \sigma_2^{-2} \sigma_3^{2}\) for the Conway knot.

noncomputable def conwayKnot : PLKnot where
  vertices := braidClosure 4 conwayBraidWord
  three_le := by
    have h : (braidClosure 4 conwayBraidWord).length = 78 := by rfl
    omega
Uses 4 · Used by 3
Statement usesPL knot (closed polyline) · Euclidean space \(\mathbb{R}^3\) · Polyline closure of a braid word · Braid word for the Conway knot
Used byThe Conway knot polyline is a simple closed curve · The Conway knot is not smoothly slice (Piccirillo) · The Conway knot is topologically slice

DefinitionKnots as parametrized knots#✓fully proved

A knot in \(\mathbb{R}^3\), given by a smooth \(2\pi\)-periodic immersion \(\gamma : \mathbb{R} \to \mathbb{R}^3\) that is injective on \([0, 2\pi)\), is sent to the parametrized knot with the same parametrization \(\gamma\).

def toParametrizedKnot (K : ConwayKnotShared.KnotTheory.Knot) :
    Knot.Euclidean.ParametrizedKnot where
  curve := K.curve
  smooth := K.smooth
  periodic := K.periodic
  injOn := K.injOn
  immersion := K.immersion
Uses 4 · Used by 3
Statement usesEuclidean 3-space · Oriented smooth knot · Euclidean space \(\mathbb{R}^3\) · Parametrized knot
Used byKnots are the same as parametrized knots · Isotopy of knots agrees with isotopy of parametrized knots · Two-component links as labeled links

DefinitionParametrized knots as knots#✓fully proved

A parametrized knot in \(\mathbb{R}^3\), given by a smooth \(2\pi\)-periodic immersion \(\gamma : \mathbb{R} \to \mathbb{R}^3\) that is injective on \([0, 2\pi)\), is sent to the knot with the same parametrization \(\gamma\).

def ofParametrizedKnot (K : Knot.Euclidean.ParametrizedKnot) :
    ConwayKnotShared.KnotTheory.Knot where
  curve := K.curve
  smooth := K.smooth
  periodic := K.periodic
  injOn := K.injOn
  immersion := K.immersion
Uses 4 · Used by 2
Statement usesEuclidean 3-space · Oriented smooth knot · Euclidean space \(\mathbb{R}^3\) · Parametrized knot
Used byKnots are the same as parametrized knots · Labeled two-component links as two-component links

DefinitionKnots are the same as parametrized knots#✓fully proved

Sending a knot in \(\mathbb{R}^3\) to the parametrized knot with the same parametrization is a bijection from knots to parametrized knots, whose inverse sends a parametrized knot to the knot with the same parametrization.

def knotEquiv :
    ConwayKnotShared.KnotTheory.Knot ≃ Knot.Euclidean.ParametrizedKnot where
  toFun := toParametrizedKnot
  invFun := ofParametrizedKnot
  left_inv := ofParametrizedKnot_toParametrizedKnot
  right_inv := toParametrizedKnot_ofParametrizedKnot
Uses 6
Statement usesEuclidean 3-space · Parametrized knots as knots · Knots as parametrized knots · Oriented smooth knot · Euclidean space \(\mathbb{R}^3\) · Parametrized knot

DefinitionConway-knot ambient isotopies as Euclidean ambient isotopies#✓fully proved

An ambient isotopy of \(\mathbb{R}^3\) in the sense of the Conway knot statements, given by maps \(H_t : \mathbb{R}^3 \to \mathbb{R}^3\) for \(t \in \mathbb{R}\) with \((t, x) \mapsto H_t(x)\) smooth and \(H_0 = \mathrm{id}\), and maps \(G_t : \mathbb{R}^3 \to \mathbb{R}^3\) with \((t, x) \mapsto G_t(x)\) smooth and \(G_t \circ H_t = H_t \circ G_t = \mathrm{id}\) for every \(t\), is sent to the smooth ambient isotopy of Euclidean 3-space, in the sense of parametrized links, with the same forward family \(H\) and inverse family \(G\).

def toEuclideanAmbientIsotopy
    (Φ : ConwayKnotShared.KnotTheory.AmbientIsotopy) :
    Knot.Euclidean.AmbientIsotopy where
  H := Φ.H
  Hinv := Φ.Hinv
  smooth := Φ.smooth
  smooth_inv := Φ.smooth_inv
  inv_left := Φ.inv_left
  inv_right := Φ.inv_right
  start := Φ.start
Uses 4 · Used by 2
Statement usesEuclidean 3-space · Smooth ambient isotopy of \(\mathbb{R}^3\) · Euclidean space \(\mathbb{R}^3\) · Smooth ambient isotopy of Euclidean 3-space
Used byIsotopy of knots agrees with isotopy of parametrized knots · Two-component link isotopy agrees with labeled link isotopy

DefinitionEuclidean ambient isotopies as Conway-knot ambient isotopies#✓fully proved

A smooth ambient isotopy of Euclidean 3-space in the sense of parametrized links, given by maps \(H_t : \mathbb{R}^3 \to \mathbb{R}^3\) for \(t \in \mathbb{R}\) with \((t, x) \mapsto H_t(x)\) smooth and \(H_0 = \mathrm{id}\), and maps \(G_t : \mathbb{R}^3 \to \mathbb{R}^3\) with \((t, x) \mapsto G_t(x)\) smooth and \(G_t \circ H_t = H_t \circ G_t = \mathrm{id}\) for every \(t\), is sent to the ambient isotopy of \(\mathbb{R}^3\) in the sense of the Conway knot statements with the same forward family \(H\) and inverse family \(G\).

def ofEuclideanAmbientIsotopy (Φ : Knot.Euclidean.AmbientIsotopy) :
    ConwayKnotShared.KnotTheory.AmbientIsotopy where
  H := Φ.H
  Hinv := Φ.Hinv
  smooth := Φ.smooth
  smooth_inv := Φ.smooth_inv
  inv_left := Φ.inv_left
  inv_right := Φ.inv_right
  start := Φ.start
Uses 4 · Used by 2
Statement usesEuclidean 3-space · Smooth ambient isotopy of \(\mathbb{R}^3\) · Euclidean space \(\mathbb{R}^3\) · Smooth ambient isotopy of Euclidean 3-space
Used byIsotopy of knots agrees with isotopy of parametrized knots · Two-component link isotopy agrees with labeled link isotopy

DefinitionConway-knot circle reparametrizations as Euclidean ones#✓fully proved

An orientation-preserving smooth reparametrization of the circle in the sense of the Conway knot statements, given by a smooth strictly increasing map \(f : \mathbb{R} \to \mathbb{R}\) with smooth two-sided inverse \(g\) such that \(f(t + 2\pi) = f(t) + 2\pi\) and \(g(t + 2\pi) = g(t) + 2\pi\) for all \(t\), is sent to the circle reparametrization, in the sense of parametrized links, with the same lift \(f\) and inverse lift \(g\).

def toEuclideanCircleReparam
    (σ : ConwayKnotShared.KnotTheory.CircleReparam) :
    Knot.Euclidean.CircleReparam where
  f := σ.f
  finv := σ.finv
  smooth := σ.smooth
  smooth_inv := σ.smooth_inv
  left_inv := σ.left_inv
  right_inv := σ.right_inv
  periodic := σ.periodic
  periodic_inv := σ.periodic_inv
  mono := σ.mono
Uses 1 · Used by 2
Statement usesOrientation-preserving reparametrization of the circle
Used byIsotopy of knots agrees with isotopy of parametrized knots · Two-component link isotopy agrees with labeled link isotopy

DefinitionEuclidean circle reparametrizations as Conway-knot ones#✓fully proved

A circle reparametrization in the sense of parametrized links, given by a smooth strictly increasing map \(f : \mathbb{R} \to \mathbb{R}\) with smooth two-sided inverse \(g\) such that \(f(t + 2\pi) = f(t) + 2\pi\) and \(g(t + 2\pi) = g(t) + 2\pi\) for all \(t\), is sent to the orientation-preserving smooth reparametrization of the circle in the sense of the Conway knot statements with the same lift \(f\) and inverse lift \(g\).

def ofEuclideanCircleReparam (σ : Knot.Euclidean.CircleReparam) :
    ConwayKnotShared.KnotTheory.CircleReparam where
  f := σ.f
  finv := σ.finv
  smooth := σ.smooth
  smooth_inv := σ.smooth_inv
  left_inv := σ.left_inv
  right_inv := σ.right_inv
  periodic := σ.periodic
  periodic_inv := σ.periodic_inv
  mono := σ.mono
Uses 1 · Used by 2
Statement usesOrientation-preserving reparametrization of the circle
Used byIsotopy of knots agrees with isotopy of parametrized knots · Two-component link isotopy agrees with labeled link isotopy

TheoremIsotopy of knots agrees with isotopy of parametrized knots#✓fully proved

For all knots \(K_1\) and \(K_2\) in \(\mathbb{R}^3\), \(K_1\) and \(K_2\) are ambient isotopic if and only if the parametrized knots with the same parametrizations as \(K_1\) and \(K_2\) are ambient isotopic as parametrized knots.

theorem knot_isotopic_iff {K₁ K₂ : ConwayKnotShared.KnotTheory.Knot} :
    ConwayKnotShared.KnotTheory.Knot.Isotopic K₁ K₂ ↔
      Knot.Euclidean.ParametrizedKnot.Isotopic
        (toParametrizedKnot K₁) (toParametrizedKnot K₂)
Uses 14
Statement usesKnots as parametrized knots · Oriented smooth knot · Ambient isotopy of oriented knots · Isotopy of parametrized knots
Proof usesEuclidean 3-space · Euclidean ambient isotopies as Conway-knot ambient isotopies · Euclidean circle reparametrizations as Conway-knot ones · Conway-knot ambient isotopies as Euclidean ambient isotopies · Conway-knot circle reparametrizations as Euclidean ones · Smooth ambient isotopy of \(\mathbb{R}^3\) · Euclidean space \(\mathbb{R}^3\) · Smooth ambient isotopy of Euclidean 3-space · Orientation-preserving reparametrization of the circle · Parametrized knot

A two-component link in \(\mathbb{R}^3\) with first component \(K\) and second component \(L\) is sent to the labeled parametrized link with two components whose component \(0\) is the parametrized knot with the same parametrization as \(K\) and whose component \(1\) is the parametrized knot with the same parametrization as \(L\).

def toParametrizedLink (L : ConwayKnotShared.KnotTheory.TwoLink) :
    Knot.Euclidean.ParametrizedLink 2 where
  component := ![toParametrizedKnot L.K, toParametrizedKnot L.L]
  pairwiseDisjoint := by
    intro i _ j _ hij
    fin_cases i <;> fin_cases j
    · exact absurd rfl hij
    · exact L.disjoint
    · exact L.disjoint.symm
    · exact absurd rfl hij
Uses 7 · Used by 1
Statement usesEuclidean 3-space · Knots as parametrized knots · Oriented smooth knot · Euclidean space \(\mathbb{R}^3\) · Two-component link · Parametrized knot · Parametrized link
Used byTwo-component link isotopy agrees with labeled link isotopy

A labeled parametrized link with two components \(0\) and \(1\) is sent to the two-component link in \(\mathbb{R}^3\) whose first component is the knot with the same parametrization as component \(0\) and whose second component is the knot with the same parametrization as component \(1\).

def ofParametrizedLink (L : Knot.Euclidean.ParametrizedLink 2) :
    ConwayKnotShared.KnotTheory.TwoLink where
  K := ofParametrizedKnot (L.component 0)
  L := ofParametrizedKnot (L.component 1)
  disjoint := by
    have h := L.pairwiseDisjoint (Set.mem_univ 0) (Set.mem_univ 1)
      (by decide : (0 : Fin 2) ≠ 1)
    exact h
Uses 7
Statement usesEuclidean 3-space · Parametrized knots as knots · Oriented smooth knot · Euclidean space \(\mathbb{R}^3\) · Two-component link · Parametrized knot · Parametrized link

Let \(L_1\) and \(L_2\) be oriented two-component smooth links in \(\mathbb{R}^3\), and regard each as an oriented labeled smooth link with two components, whose component \(0\) is its first component and whose component \(1\) is its second. Then \(L_1\) and \(L_2\) are ambient isotopic, meaning that a single smooth ambient isotopy carries each component of \(L_1\) onto the corresponding component of \(L_2\) up to orientation-preserving reparametrizations of the circle, if and only if the associated labeled links are ambient isotopic.

theorem twoLink_isotopic_iff
    {L₁ L₂ : ConwayKnotShared.KnotTheory.TwoLink} :
    ConwayKnotShared.KnotTheory.TwoLink.Isotopic L₁ L₂ ↔
      Knot.Euclidean.ParametrizedLink.Isotopic
        (toParametrizedLink L₁) (toParametrizedLink L₂)
Uses 16
Statement usesTwo-component links as labeled links · Two-component link · Ambient isotopy of oriented two-component links · Isotopy of parametrized links
Proof usesEuclidean 3-space · Euclidean ambient isotopies as Conway-knot ambient isotopies · Euclidean circle reparametrizations as Conway-knot ones · Conway-knot ambient isotopies as Euclidean ambient isotopies · Conway-knot circle reparametrizations as Euclidean ones · Smooth ambient isotopy of \(\mathbb{R}^3\) · Oriented smooth knot · Euclidean space \(\mathbb{R}^3\) · Smooth ambient isotopy of Euclidean 3-space · Orientation-preserving reparametrization of the circle · Parametrized knot · Parametrized link

There exist two oriented smooth two-component links \(L_1\) and \(L_2\) in \(\mathbb{R}^3\) that are not ambient isotopic as oriented links with ordered components: no ambient isotopy of \(\mathbb{R}^3\) carries the first component of \(L_1\) to the first component of \(L_2\) and the second component of \(L_1\) to the second component of \(L_2\), each up to an orientation-preserving reparametrization of the circle.

public theorem_wanted exists_nonisotopic_link : ∃ L₁ L₂ : TwoLink, ¬ L₁.Isotopic L₂
Sources
  • Classical; see https://en.wikipedia.org/wiki/Linking_number. Problem exists_nonisotopic_link of the lean-eval benchmark.
Uses 2
Statement usesTwo-component link · Ambient isotopy of oriented two-component links

TheoremExistence of non-isotopic knots#●ready to prove

There are two oriented smooth knots \(K_1\) and \(K_2\) in \(\mathbb{R}^3\) that are not ambient-isotopic.

public theorem_wanted exists_nonisotopic_knots : ∃ K₁ K₂ : Knot, ¬ K₁.Isotopic K₂
Sources
  • Classical; see https://en.wikipedia.org/wiki/Knot_invariant. Problem exists_nonisotopic_knots of the lean-eval benchmark.
Uses 2
Statement usesOriented smooth knot · Ambient isotopy of oriented knots
68 fully proved2 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.