Pardon's lower bound for torus-knot distortion

pardon_torus_knot_distortion

Submitter: Kim Morrison.

Notes: For positive coprime p and q, every smooth representative in the orientation-preserving smooth ambient-isotopy class of the explicitly parametrized standard (p, q)-torus curve has distortion at least min(p, q) / 160. Intrinsic distance is the shorter of the two complementary arclengths, and distortion is the supremum in the extended nonnegative reals of intrinsic distance divided by Euclidean chord length over distinct points. The extended codomain faithfully represents the possibility of infinite distortion without imposing an unrelated boundedness proof. Pardon's published theorem takes the infimum over all rectifiable representatives of the unoriented isotopy class; because LeanEval.KnotTheory.Prelude models smooth knots, this benchmark is its faithful smooth, orientation-sensitive specialization. It is separate from the 3-dimensional Hilbert-Smith problem already proposed in PR #482.

Source: John Pardon, 'On the distortion of knots on embedded surfaces', Annals of Mathematics (2) 174 (2011), no. 1, 637-646, Theorem 1.1. https://doi.org/10.4007/annals.2011.174.1.21

Informal solution: Apply Pardon's more general surface theorem (Theorem 1.3) to a PL torus F isotopic to the standard unknotted torus and the simple loop beta of slope (p, q). Its invariant I(F, beta), the minimum geometric intersection number with a compressing-disk boundary, is min(p, q). Theorem 1.3 gives delta(K_beta) >= I(F, beta) / 160, where delta(K_beta) is the infimum over all rectifiable representatives. Consequently every such representative, in particular the smooth knot K quantified here, satisfies the same lower bound.

theorem declaration uses `sorry`pardon_torus_knot_distortion (p q : ℕ) (_hp : 0 < p) (_hq : 0 < q) (_hc : Nat.Coprime p q)
    (K : LeanEval.KnotTheory.PardonDistortion.Knot)
    (_hclass : ∃ Φ : LeanEval.KnotTheory.PardonDistortion.AmbientIsotopy, ∃ σ : LeanEval.KnotTheory.PardonDistortion.CircleReparam,
      ∀ t, Φ.H 1 (K.curve t) = LeanEval.KnotTheory.PardonDistortion.standardTorusCurve p q (σ.f t)) :
    (1 / 160 : ℝ≥0∞) * (Nat.min p q : ℝ≥0∞) ≤ LeanEval.KnotTheory.PardonDistortion.distortion K := byp:ℕq:ℕ_hp:0 < p_hq:0 < q_hc:p.Coprime qK:Knot_hclass:∃ Φ σ, ∀ (t : ℝ), Φ.H 1 (K.curve t) = standardTorusCurve p q (σ.f t)⊢ 1 / 160 * ↑(p.min q) ≤ distortion K
  sorryAll goals completed! 🐙

Solved by

Not yet solved.