Prove2Me

Small push-offs of a framed loop in S3S^3 along its frame miss the loop (tube lemma)

Proved
HryniewiczCriterion.framedPushOff_tube

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

geometry-topologysymplectic-geometry

Let γ:R→S3⊂R4\gamma:\mathbb{R}\to S^3\subset\mathbb{R}^4 be a C2C^2 loop, γ(s+1)=γ(s)\gamma(s+1)=\gamma(s), injective modulo 11. Let e1,e2e_1,e_2 be continuous 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\quad\text{for all } s.

Fix 0<a≤b0<a\le b. Then there is ε0>0\varepsilon_0>0 such that for 0<ε<ε00<\varepsilon<\varepsilon_0, all s,t,φs,t,\varphi and all ρ∈[a,b]\rho\in[a,b], the vector x=γ(t)+ερ (cos⁡φ e1(t)+sin⁡φ e2(t))x=\gamma(t)+\varepsilon\rho\,(\cos\varphi\,e_1(t)+\sin\varphi\,e_2(t)) is non-zero and is not a positive multiple of γ(s)\gamma(s). Equivalently, the radially normalized push-off x/∣x∣x/|x| misses the loop.

Proof: write s=t+h+ns=t+h+n with n∈Zn\in\mathbb{Z}, ∣h∣≤12|h|\le\frac12, and suppose x=μγ(t+h)x=\mu\gamma(t+h), μ>0\mu>0; then ∣μ−1∣=O(ε)|\mu-1|=O(\varepsilon). If ∣h∣≥η|h|\ge\eta, injectivity and compactness bound ∣γ(t+h)−γ(t)∣|\gamma(t+h)-\gamma(t)| below, which is impossible. If ∣h∣<η|h|<\eta, write γ(t+h)=γ(t)+hγ′(t)+T\gamma(t+h)=\gamma(t)+h\gamma'(t)+T with ∣T∣≤Lh2|T|\le Lh^2. Pairing with γ′(t)\gamma'(t), using γ⊥γ′\gamma\perp\gamma', gives ∣h∣=O(ε)|h|=O(\varepsilon). The determinant det⁡(γ,γ′,⋅,−sin⁡φ e1+cos⁡φ e2)\det(\gamma,\gamma',\cdot,-\sin\varphi\,e_1+\cos\varphi\,e_2) then gives ερdet⁡(γ,γ′,e1,e2)=μdet⁡(γ,γ′,T,⋅)=O(ε2)\varepsilon\rho\det(\gamma,\gamma',e_1,e_2)=\mu\det(\gamma,\gamma',T,\cdot)=O(\varepsilon^2), a contradiction for small ε\varepsilon.

Preamble
import Definitions.Def_HryniewiczCriterion_SelfLinking

open HryniewiczCriterion
open scoped ContDiff
Formal statement
theorem HryniewiczCriterion.framedPushOff_tube (γ e₁ e₂ : ℝ → R4) (hγ : ContDiff ℝ 2 γ) (he₁ : Continuous e₁)
    (he₂ : Continuous 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]))
    (a b : ℝ) (ha : 0 < a) (hab : a ≤ b) :
    ∃ ε₀ : ℝ, 0 < ε₀ ∧ ∀ ε : ℝ, 0 < ε → ε < ε₀ → ∀ s t ρ φ : ℝ, a ≤ ρ → ρ ≤ b →
      γ t + ε • (ρ • (Real.cos φ • e₁ t + Real.sin φ • e₂ t)) ≠ 0 ∧
      ∀ μ : ℝ, 0 < μ → γ t + ε • (ρ • (Real.cos φ • e₁ t + Real.sin φ • e₂ t)) ≠ μ • γ s := by sorry
Source
Tubular neighbourhood of an embedded loop; D. Rolfsen, Knots and Links, Publish or Perish, 1976, Ch. 5D (linking number via the Gauss integral; a meridian links its knot once; framings and the twisting of push-offs); used for self-linking numbers in U. Hryniewicz, Systems of global surfaces of section for dynamically convex Reeb flows on the 3-sphere, J. Symplectic Geom. 12 (2014), arXiv:1105.2077, Definition 1.5.

View graph