Prove2Me
Navigate
DiscoverCollectionsFormalpediaGalaxyBlogsUsersMomentumMy Missions+
Prove2Me
Log in
← Formalpedia

The Gauss linking integral of two disjoint loops in S3S^3S3 does not depend on the stereographic pole

Proved
HryniewiczCriterion.isLinkingNumber_of_gaussLinkingIntegral_eq

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

geometry-topologysymplectic-geometry

Let γ1,γ2:R→S3⊂R4\gamma_1,\gamma_2:\mathbb{R}\to S^3\subset\mathbb{R}^4γ1​,γ2​:R→S3⊂R4 be C2C^2C2, 111-periodic loops with disjoint images. Let N∈S3N\in S^3N∈S3 be a pole missing both loops, and suppose the Gauss linking integral of the stereographic images,

14π∫01 ⁣ ⁣∫01det⁡(−N, A′(s), B′(t), A(s)−B(t))∣A(s)−B(t)∣3 dt ds,A=σN∘γ1, B=σN∘γ2,\frac{1}{4\pi}\int_0^1\!\!\int_0^1 \frac{\det\big(-N,\ A'(s),\ B'(t),\ A(s)-B(t)\big)}{|A(s)-B(t)|^3}\,dt\,ds,\qquad A=\sigma_N\circ\gamma_1,\ B=\sigma_N\circ\gamma_2,4π1​∫01​∫01​∣A(s)−B(t)∣3det(−N, A′(s), B′(t), A(s)−B(t))​dtds,A=σN​∘γ1​, B=σN​∘γ2​,

equals the integer nnn. Then nnn is the linking number of γ1,γ2\gamma_1,\gamma_2γ1​,γ2​ in the sense of IsLinkingNumber: the integral equals nnn for every pole N′∈S3N'\in S^3N′∈S3 that misses both loops.

Proof idea: the Gauss integral is constant along any C2C^2C2 homotopy of the pair of loops that keeps them disjoint (its τ\tauτ-derivative is the integral of an exact form on the torus, because u↦u/∣u∣3u\mapsto u/|u|^3u↦u/∣u∣3 is divergence free). Moving the pole along a path NτN_\tauNτ​ in S3∖(γ1∪γ2)S^3\setminus(\gamma_1\cup\gamma_2)S3∖(γ1​∪γ2​) and composing with rotations Rτ∈SO(4)R_\tau\in SO(4)Rτ​∈SO(4), RτNτ=NR_\tau N_\tau=NRτ​Nτ​=N, turns the change of pole into such a homotopy, since the integrand is invariant under rotations. The complement of two C1C^1C1 curves in S3S^3S3 is path connected: the great-circle cones over the curves from a point are images of 222-dimensional sets, so they have measure zero and a midpoint avoiding them exists.

Preamble
import Definitions.Def_HryniewiczCriterion_SelfLinking

open HryniewiczCriterion
open scoped ContDiff
Formal statement
theorem HryniewiczCriterion.isLinkingNumber_of_gaussLinkingIntegral_eq (γ₁ γ₂ : ℝ → 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)
    (N : R4) (hN : euclidNorm N = 1) (hNγ : ∀ s, γ₁ s ≠ N ∧ γ₂ s ≠ N)
    (n : ℤ) (hG : gaussLinkingIntegral N γ₁ γ₂ = n) :
    IsLinkingNumber γ₁ γ₂ n := by sorry
Source
Gauss linking integral and its independence of the projection (Rolfsen, Knots and Links, 1976, Ch. 5D; Ricca–Nipoti, Gauss' linking number revisited, J. Knot Theory Ramifications 20 (2011)).

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paperProve2Me Team
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me