Prove2Me

Gauss linking integral with a (1,k)(1,k)-curve on a torus around a loop: twisting formula

Proved
HryniewiczCriterion.gaussLinkingIntegral_torus_twist

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 loop, γ(s+1)=γ(s)\gamma(s+1)=\gamma(s), and let P:R2→S3P:\mathbb{R}^2\to S^3 be a C2C^2 torus, 11-periodic in tt and 2π2\pi-periodic in φ\varphi, disjoint from γ\gamma. Let N∈S3N\in S^3 be a pole missing both. Let θ:R→R\theta:\mathbb{R}\to\mathbb{R} be C2C^2 with

θ(t+1)=θ(t)+2πk,k∈Z.\theta(t+1)=\theta(t)+2\pi k,\qquad k\in\mathbb{Z}.

Then, for the Gauss linking integral after stereographic projection from NN,

GaussN(γ, t↦P(t,θ(t)))=GaussN(γ, t↦P(t,0))+k⋅GaussN(γ, φ↦P(0,2πφ)).\mathrm{Gauss}_N\big(\gamma,\ t\mapsto P(t,\theta(t))\big)=\mathrm{Gauss}_N\big(\gamma,\ t\mapsto P(t,0)\big)+k\cdot\mathrm{Gauss}_N\big(\gamma,\ \varphi\mapsto P(0,2\pi\varphi)\big).

Proof: vary the open arcs Bτ(t)=P(t,τθ(t))B_\tau(t)=P(t,\tau\theta(t)), τ∈[0,1]\tau\in[0,1]. The pointwise closedness identity of the Gauss 22-form gives ∂τf=∂sPs−∂tQt\partial_\tau f=\partial_sP_s-\partial_tQ_t. The ss-term integrates to 00 by periodicity of γ\gamma. The tt-term leaves only the boundary terms at t=0,1t=0,1, which sweep the meridian φ↦P(0,φ)\varphi\mapsto P(0,\varphi) from θ(0)\theta(0) to θ(0)+2πk\theta(0)+2\pi k, that is, kk full turns.

Preamble
import Definitions.Def_HryniewiczCriterion_SelfLinking

open HryniewiczCriterion
open scoped ContDiff
Formal statement
theorem HryniewiczCriterion.gaussLinkingIntegral_torus_twist (N : R4) (hN : euclidNorm N = 1) (γ : ℝ → R4) (P : ℝ → ℝ → R4)
    (hγ : ContDiff ℝ 2 γ) (hP : ContDiff ℝ 2 (Function.uncurry P))
    (hγper : ∀ s, γ (s + 1) = γ s) (hPper₁ : ∀ t φ, P (t + 1) φ = P t φ)
    (hPper₂ : ∀ t φ, P t (φ + 2 * Real.pi) = P t φ)
    (hγunit : ∀ s, euclidNorm (γ s) = 1) (hPunit : ∀ t φ, euclidNorm (P t φ) = 1)
    (hγN : ∀ s, γ s ≠ N) (hPN : ∀ t φ, P t φ ≠ N) (hne : ∀ s t φ, γ s ≠ P t φ)
    (θ : ℝ → ℝ) (hθ : ContDiff ℝ 2 θ) (k : ℤ) (hθper : ∀ t, θ (t + 1) = θ t + 2 * Real.pi * k) :
    gaussLinkingIntegral N γ (fun t => P t (θ t)) =
      gaussLinkingIntegral N γ (fun t => P t 0) +
        k * gaussLinkingIntegral N γ (fun φ => P 0 (2 * Real.pi * φ)) := by sorry
Source
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