Prove2Me

Twisting formula: a push-off winding kk times around a knot in S3S^3 links it kk more times

Proved
HryniewiczCriterion.gaussLinkingIntegral_twisted_pushOff

by Mazecto · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

geometry-topologysymplectic-geometry

Let γ:R→S3\gamma:\mathbb{R}\to S^3 be a C2C^2, 11-periodic loop, injective modulo 11, and let e1,e2e_1,e_2 be C2C^2, 11-periodic vector fields along γ\gamma with

det⁡(γ(s),γ′(s),e1(s),e2(s))>0for all s,\det\big(\gamma(s),\gamma'(s),e_1(s),e_2(s)\big)>0\qquad\text{for all } s,

so that e1,e2e_1,e_2 span a positively oriented complement of γ′\gamma' in TS3T S^3 (oriented as the boundary of the ball). Let r>0r>0 and θ\theta be C2C^2 with r(s+1)=r(s)r(s+1)=r(s) and θ(s+1)=θ(s)+2πk\theta(s+1)=\theta(s)+2\pi k. For ε>0\varepsilon>0 put

B0ε(s)=γ+εe1∣γ+εe1∣,BVε(s)=γ+εr(cos⁡θ e1+sin⁡θ e2)∣⋅∣.B_0^\varepsilon(s)=\frac{\gamma+\varepsilon e_1}{|\gamma+\varepsilon e_1|},\qquad B_V^\varepsilon(s)=\frac{\gamma+\varepsilon r(\cos\theta\, e_1+\sin\theta\, e_2)}{|\cdot|}.

Then there are a pole N∈S3N\in S^3 and ε0>0\varepsilon_0>0 such that for 0<ε<ε00<\varepsilon<\varepsilon_0 the push-off B0εB_0^\varepsilon is well defined and disjoint from γ\gamma, NN misses γ\gamma, B0εB_0^\varepsilon, BVεB_V^\varepsilon, and the Gauss linking integrals from NN satisfy

Gauss⁡N(γ,BVε)=Gauss⁡N(γ,B0ε)+k.\operatorname{Gauss}_N(\gamma,B_V^\varepsilon)=\operatorname{Gauss}_N(\gamma,B_0^\varepsilon)+k .

Proof idea: take NN off γ\gamma and ε\varepsilon so small that all push-offs stay in a thin tube around γ\gamma away from NN. The homotopy rτ=(1−τ)r+τr_\tau=(1-\tau)r+\tau, θτ=(1−τ)θ+τ⋅2πks\theta_\tau=(1-\tau)\theta+\tau\cdot 2\pi k s stays in the tube minus γ\gamma, so by homotopy invariance of the Gauss integral we may take r=1r=1, θ=2πks\theta=2\pi k s. Pulled back to the torus (s,φ)↦(γ+ε(cos⁡φ e1+sin⁡φ e2))/∣⋅∣(s,\varphi)\mapsto(\gamma+\varepsilon(\cos\varphi\,e_1+\sin\varphi\,e_2))/|\cdot|, the Biot–Savart form of γ\gamma is closed, so the curve of class (1,k)(1,k) has integral equal to that of the class (1,0)(1,0) plus kk times the meridian integral. The meridian integral is 11 (Ampère's law), as the rescaling limit ε→0\varepsilon\to 0 shows: the knot becomes its tangent line and the meridian a circle around it, whose Gauss integral is 12∫R(1+v2)−3/2 dv=1\tfrac{1}{2}\int_{\mathbb{R}}(1+v^2)^{-3/2}\,dv=1. The sign is fixed by the orientation hypothesis.

Preamble
import Definitions.Def_HryniewiczCriterion_SelfLinking

open HryniewiczCriterion
open scoped ContDiff
Formal statement
theorem HryniewiczCriterion.gaussLinkingIntegral_twisted_pushOff (γ e₁ e₂ : ℝ → R4)
    (hγ : ContDiff ℝ 2 γ) (he₁ : ContDiff ℝ 2 e₁) (he₂ : ContDiff ℝ 2 e₂)
    (hγper : ∀ s, γ (s + 1) = γ s) (he₁per : ∀ s, e₁ (s + 1) = e₁ s)
    (he₂per : ∀ s, e₂ (s + 1) = e₂ s) (hγunit : ∀ s, euclidNorm (γ s) = 1)
    (hinj : ∀ s t, γ s = γ t → ∃ n : ℤ, t = s + n)
    (hdet : ∀ s, 0 < Matrix.det (Matrix.of ![γ s, deriv γ s, e₁ s, e₂ s]))
    (r θ : ℝ → ℝ) (hr : ContDiff ℝ 2 r) (hθ : ContDiff ℝ 2 θ) (hr0 : ∀ s, 0 < r s)
    (hrper : ∀ s, r (s + 1) = r s) (k : ℤ) (hθper : ∀ s, θ (s + 1) = θ s + 2 * Real.pi * k) :
    ∃ N : R4, euclidNorm N = 1 ∧ ∃ ε₀ : ℝ, 0 < ε₀ ∧ ∀ ε : ℝ, 0 < ε → ε < ε₀ →
      (∀ s, γ s + ε • e₁ s ≠ 0) ∧
      (∀ s t, γ s ≠ radialNormalize (γ t + ε • e₁ t)) ∧
      (∀ s, γ s ≠ N ∧ radialNormalize (γ s + ε • e₁ s) ≠ N ∧
        radialNormalize (γ s + ε • (r s • (Real.cos (θ s) • e₁ s + Real.sin (θ s) • e₂ s))) ≠ N) ∧
      gaussLinkingIntegral N γ
          (fun s => radialNormalize (γ s + ε • (r s • (Real.cos (θ s) • e₁ s + Real.sin (θ s) • e₂ s)))) =
        gaussLinkingIntegral N γ (fun s => radialNormalize (γ s + ε • e₁ s)) + k := by sorry
Source
Twisting formula for framings of a knot (Rolfsen, Knots and Links, 1976, Ch. 5D; Geiges, An Introduction to Contact Topology, 2008, §3.5.2); needed for U. Hryniewicz, Fast finite-energy planes in symplectizations and applications, Trans. Amer. Math. Soc. 364 (2012), Proposition 2.1.

View graph