Quadrisecant theorem

DefinitionPeriod#✓fully proved

The period is the real number \(2\pi\).

noncomputable def period : ℝ := 2 * Real.pi

Used by 1

Used byQuadrisecant of a knot

DefinitionStandard circle#✓fully proved

The standard circle is the curve \(\mathbb{R} \to \mathbb{R}^3\) given by \(t \mapsto (\cos t, \sin t, 0)\), the unit circle in the \(xy\)-plane.

noncomputable def standardCircle (t : ℝ) : R3 :=
  !₂[Real.cos t, Real.sin t, 0]

Uses 1 · Used by 1

Statement usesEuclidean space \(\mathbb{R}^3\)

Used byUnknotted knot

DefinitionUnknotted knot#✓fully proved

A knot \(K\) is unknotted when there is a knot \(J\) whose parametrization is the standard circle \(t \mapsto (\cos t, \sin t, 0)\) such that \(K\) is ambient-isotopic to \(J\) as an oriented knot.

def IsUnknotted (K : Knot) : Prop :=
  ∃ J : Knot, J.curve = standardCircle ∧ K.Isotopic J

Uses 4 · Used by 1

Statement usesOriented smooth knot · Ambient isotopy of oriented knots · Euclidean space \(\mathbb{R}^3\) · Standard circle

Used byQuadrisecant theorem (Pannwitz–Kuperberg)

DefinitionQuadrisecant of a knot#✓fully proved

A knot \(K\) with parametrization \(\gamma \colon \mathbb{R} \to \mathbb{R}^3\) has a quadrisecant when there are pairwise distinct reals \(t_0, t_1, t_2, t_3 \in [0, 2\pi)\), a point \(p \in \mathbb{R}^3\), a nonzero vector \(v \in \mathbb{R}^3\) and reals \(a_0, a_1, a_2, a_3\) such that \(\gamma(t_i) = p + a_i v\) for each \(i\), that is, the four points \(\gamma(t_i)\) lie on one line.

def HasQuadrisecant (K : Knot) : Prop :=
  ∃ t0 t1 t2 t3 : ℝ, ∃ p v : R3, ∃ a0 a1 a2 a3 : ℝ,
    t0 ∈ Set.Ico (0 : ℝ) period ∧ t1 ∈ Set.Ico (0 : ℝ) period ∧
      t2 ∈ Set.Ico (0 : ℝ) period ∧ t3 ∈ Set.Ico (0 : ℝ) period ∧
      [t0, t1, t2, t3].Nodup ∧ v ≠ 0 ∧
      K.curve t0 = p + a0 • v ∧ K.curve t1 = p + a1 • v ∧
      K.curve t2 = p + a2 • v ∧ K.curve t3 = p + a3 • v

Uses 3 · Used by 1

Statement usesOriented smooth knot · Euclidean space \(\mathbb{R}^3\) · Period

Used byQuadrisecant theorem (Pannwitz–Kuperberg)

TheoremQuadrisecant theorem (Pannwitz–Kuperberg)#●ready to prove

Every smooth knot \(K\) in \(\mathbb{R}^3\) that is not unknotted has a quadrisecant.

public theorem_wanted smooth_knot_has_quadrisecant
    (K : Knot) (_hnontrivial : ¬ IsUnknotted K) :
    HasQuadrisecant K

Sources

• E. Pannwitz (1933); G. Kuperberg, Quadrisecants of knots and links, J. Knot Theory Ramif. 3 (1994). Knill, §161. Problem smooth_knot_has_quadrisecant of the lean-eval benchmark.

Uses 3

Statement usesOriented smooth knot · Quadrisecant of a knot · Unknotted knot

4 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.