Fáry–Milnor theorem (knot total curvature ≤ 4π implies unknotted)

fary_milnor

Submitter: Kim Morrison.

Notes: A smooth knot in ℝ³ with total curvature at most 4π is unknotted. A knot is a smooth, regular, 2π-periodic, simple-on-`[0, 2π)` curve `r : ℝ → ℝ³`. Curvature is the standard parametrized expression `‖r'(t) × r''(t)‖ / ‖r'(t)‖³`; total curvature is the arc-length integral. Unknottedness is encoded as a smooth isotopy through smooth knots from r to the standard unit circle. Mathlib has the analytic primitives (`deriv`, interval integrals, `ContDiff`, `crossProduct`, Euclidean norm) but no knot-total-curvature / unknottedness API. §161 of Knill's *Some Fundamental Theorems in Mathematics*.

Source: I. Fáry, 'Sur la courbure totale d'une courbe gauche faisant un nœud', Bull. Soc. Math. France 77 (1949) 128–138; J. Milnor, 'On the total curvature of knots', Ann. of Math. (2) 52 (1950) 248–257. §161 in O. Knill, *Some Fundamental Theorems in Mathematics* (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf).

Informal solution: The classical proof goes via the **crookedness** invariant `μ(r)` of a knot: for a generic unit vector `u ∈ S²`, let `M(u)` be the number of local maxima of the height function `t ↦ ⟨r(t), u⟩` on one period, and set `μ(r) := inf M(u)` over generic `u`. (1) Every smooth knot has `M(u) ≥ 1`. A nontrivial knot has `μ(r) ≥ 2`, by the *bridge lemma*: a curve with `μ(r) = 1` lies in two half-spaces meeting along a common boundary plane and bounds an embedded disk by interpolation, hence is unknotted (this is the content Knill calls Fáry/Milnor's crookedness step). (2) An integral-geometric Crofton-style identity, with the normalised area measure `dσ` on `S²` chosen so `∫_{S²} 1 dσ = 1`, gives `∫_{S²} M(u) dσ(u) = totalCurvature(r) / (2π)`. (3) Combining (1)–(2): for a nontrivial knot, `totalCurvature(r) / (2π) = ∫ M ≥ μ(r) ≥ 2`, hence `totalCurvature(r) ≥ 4π`; the contrapositive is the Fáry–Milnor theorem. Mathlib has interval integrals, deriv, `ContDiff`, and `crossProduct`, but no knot framework, no crookedness invariant, no Crofton-style integral-geometric identity, and no unknottedness criterion.

theorem declaration uses `sorry`fary_milnor_total_curvature {r : ℝ → LeanEval.Geometry.FaryMilnorProblem.Space} (_hknot : LeanEval.Geometry.FaryMilnorProblem.IsSmoothKnot r)
    (_hK : LeanEval.Geometry.FaryMilnorProblem.totalCurvature r ≤ 4 * Real.pi) :
    LeanEval.Geometry.FaryMilnorProblem.IsUnknotted r := byr:ℝ → Space_hknot:IsSmoothKnot r_hK:totalCurvature r ≤ 4 * π⊢ IsUnknotted r
  sorryAll goals completed! 🐙

Solved by

Not yet solved.