Prove2Me

The Gauss linking integral is multiplied by kk when the second loop is traversed kk times

Proved
HryniewiczCriterion.gaussLinkingIntegral_comp_mul_nat

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

dynamical-systemsgeometry-topologysymplectic-geometry

Let γ1,γ2:R→S3\gamma_1,\gamma_2:\mathbb{R}\to S^3 be disjoint C2C^2 loops of period 11, and let N∈S3N\in S^3 miss both. For every k∈Nk\in\mathbb{N},

GaussN(γ1, t↦γ2(kt))=k⋅GaussN(γ1,γ2).\mathrm{Gauss}_N\big(\gamma_1,\ t\mapsto\gamma_2(kt)\big)=k\cdot\mathrm{Gauss}_N(\gamma_1,\gamma_2).

Here GaussN\mathrm{Gauss}_N is gaussLinkingIntegral, the Gauss double integral after stereographic projection from NN. The integrand is linear in the velocity of the second loop, so substituting t↦ktt\mapsto kt turns ∫01dt\int_0^1dt into ∫0k\int_0^k. By periodicity this is kk copies of ∫01\int_0^1. For k=0k=0 both sides vanish, because the second loop is constant.

Preamble
import Definitions.Def_HryniewiczCriterion_GlobalSection
import Definitions.Def_HryniewiczCriterion_SelfLinking

open HryniewiczCriterion
Formal statement
theorem HryniewiczCriterion.gaussLinkingIntegral_comp_mul_nat (N : R4) (γ₁ γ₂ : ℝ → R4)
    (h₁ : ContDiff ℝ 2 γ₁) (h₂ : ContDiff ℝ 2 γ₂)
    (hper₁ : ∀ s, γ₁ (s + 1) = γ₁ s) (hper₂ : ∀ s, γ₂ (s + 1) = γ₂ s)
    (hunit₁ : ∀ s, euclidNorm (γ₁ s) = 1) (hunit₂ : ∀ s, euclidNorm (γ₂ s) = 1)
    (hdisj : ∀ s t, γ₁ s ≠ γ₂ t) (hN : euclidNorm N = 1) (hNγ : ∀ s, γ₁ s ≠ N ∧ γ₂ s ≠ N)
    (k : ℕ) :
    gaussLinkingIntegral N γ₁ (fun t => γ₂ (k * t)) = k * gaussLinkingIntegral N γ₁ γ₂ := by sorry
Source
Elementary (change of variables in the Gauss linking integral); used for multiply covered orbits in U. Hryniewicz, Systems of global surfaces of section for dynamically convex Reeb flows on the 3-sphere, J. Symplectic Geom. 12 (2014) 791-862, arXiv:1105.2077, Definition 1.5 and Lemma 3.12.

View graph