The Gauss linking integral of two disjoint loops in does not depend on the stereographic pole
ProvedHryniewiczCriterion.isLinkingNumber_of_gaussLinkingIntegral_eqLet be , -periodic loops with disjoint images. Let be a pole missing both loops, and suppose the Gauss linking integral of the stereographic images,
equals the integer . Then is the linking number of in the sense of IsLinkingNumber: the integral equals for every pole that misses both loops.
Proof idea: the Gauss integral is constant along any homotopy of the pair of loops that keeps them disjoint (its -derivative is the integral of an exact form on the torus, because is divergence free). Moving the pole along a path in and composing with rotations , , turns the change of pole into such a homotopy, since the integrand is invariant under rotations. The complement of two curves in is path connected: the great-circle cones over the curves from a point are images of -dimensional sets, so they have measure zero and a midpoint avoiding them exists.
import Definitions.Def_HryniewiczCriterion_SelfLinking open HryniewiczCriterion open scoped ContDiff
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