Pannwitz–Kuperberg quadrisecant theorem

smooth_knot_has_quadrisecant

Submitter: Kim Morrison.

Notes: Every smooth knot that is not the unknot has a quadrisecant (a line meeting it in four points). Trusted helpers (IsSmoothKnot, IsUnknotted, HasQuadrisecant, …) are non-holes. Mathlib has no knot theory. The Fáry–Milnor total-curvature theorem of §161 is a separate lean-eval problem. Candidate from §161 of the Knill survey.

Source: E. Pannwitz (1933); G. Kuperberg, *Quadrisecants of knots and links*, J. Knot Theory Ramif. 3 (1994). Knill, §161.

Informal solution: Unavailable.

theorem declaration uses `sorry`smooth_knot_has_quadrisecant {r : ℝ → LeanEval.KnotTheory.Quadrisecant.Space} (_hknot : LeanEval.KnotTheory.Quadrisecant.IsSmoothKnot r) (_hnontrivial : ¬ LeanEval.KnotTheory.Quadrisecant.IsUnknotted r) :
    LeanEval.KnotTheory.Quadrisecant.HasQuadrisecant r := byr:ℝ → Space_hknot:IsSmoothKnot r_hnontrivial:¬IsUnknotted r⊢ HasQuadrisecant r
  sorryAll goals completed! 🐙

Solved by

Not yet solved.