Pannwitz–Kuperberg quadrisecant theorem

smooth_knot_has_quadrisecant — a formalization challenge from the lean-eval benchmark.

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.

Formal statement

/-- **Quadrisecant theorem** (Pannwitz–Kuperberg). Every smooth nontrivial knot
has a quadrisecant. -/
theorem smooth_knot_has_quadrisecant
    {r : ℝ → Space} (_hknot : IsSmoothKnot r) (_hnontrivial : ¬ IsUnknotted r) :
    HasQuadrisecant r := by
  sorry

Source

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

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: smooth_knot_has_quadrisecant
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.