Linking numbers in $S^3$ and the self-linking number of a periodic orbit

Definition

HryniewiczCriterion_SelfLinking

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

contact-geometrydynamical-systemssymplectic-geometry

Linking number. Orient $\mathbb{R}^4$ by $dq_1\wedge dp_1\wedge dq_2\wedge dp_2$ and $S^3$ as the boundary of the unit ball. For a unit vector $N$ , stereographic projection $\sigma_N(y)=(y-\langle y,N\rangle N)/(1-\langle y,N\rangle)$ maps $S^3\setminus\{N\}$ onto $N^\perp\cong\mathbb{R}^3$ . It preserves orientation when $N^\perp$ is oriented by $\det(-N,\cdot,\cdot,\cdot)$ . For two disjoint $1$ -periodic loops $\gamma_1,\gamma_2$ in $S^3$ that miss $N$ , put $A=\sigma_N\circ\gamma_1$ and $B=\sigma_N\circ\gamma_2$ . The Gauss integral is

\operatorname{lk}_N(\gamma_1,\gamma_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.

The integer $n$ is the linking number of $\gamma_1,\gamma_2$ if some unit $N$ misses both loops and $\operatorname{lk}_N=n$ for every such $N$ .

Self-linking number (Definition 1.5). For a periodic orbit $P=(x,T)$ on a star-shaped $S$ , let $\gamma(s)=x(Ts)/|x(Ts)|$ . Let $\gamma_\epsilon(s)$ be the radial projection of $x(Ts)+\epsilon Z_1(x(Ts))$ , the push-off of $P$ along the global section $Z_1$ of $\xi$ . Then $\operatorname{sl}(P)=n$ means that $\gamma$ and $\gamma_\epsilon$ have linking number $n$ for every sufficiently small $\epsilon>0$ .

Hryniewicz defines $\operatorname{sl}$ by pushing off along a non-vanishing section of $\xi$ over a Seifert surface and intersecting with that surface. The section $Z_1$ is global, so it restricts to such a section over every spanning disk, and the intersection number equals the linking number in $S\cong S^3$ . With these orientations a Hopf fibre of the round sphere has $\operatorname{sl}=-1$ , and two Hopf fibres have linking number $+1$ .

Two periodic orbits link non-trivially if their loops have a linking number and it is non-zero.

Formalization Note Linking is computed after radial projection $S\to S^3$ , which is a diffeomorphism for star-shaped $S$ . The definition quantifies over every admissible projection point $N$ and also asserts that one exists, so it cannot hold vacuously.

Definition code

import Definitions.Def_HryniewiczCriterion_Basic
import Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
import Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic

/-!
# Linking numbers in `S³` and the self-linking number of a periodic orbit

Hryniewicz, arXiv:1105.2077, Definition 1.5 (p. 3). For a periodic orbit `P` on
`S = H⁻¹(1)`, `sl(P)` is the linking number of `P` with its push-off along a
non-vanishing section of `ξ`. Since `ξ` has the global frame `Z₁, Z₂`, which extends
over every spanning disk, the push-off is taken along `Z₁`. Linking numbers are
computed in `S³` (after radial projection `S → S³`, a diffeomorphism) by the Gauss
integral after stereographic projection.

Orientation: `S³` is oriented as the boundary of the unit ball of `ℝ⁴`, and `ℝ⁴` by
`dq₁ ∧ dp₁ ∧ dq₂ ∧ dp₂ = ½ ω₀ ∧ ω₀`. Stereographic projection from `N` onto `N^⊥` is
orientation preserving when `N^⊥` is oriented by `det(-N, ·, ·, ·)`. With these
conventions a Hopf fibre of the round sphere has `sl = -1`.
-/

namespace HryniewiczCriterion

noncomputable section

/-- Radial projection `x ↦ x / |x|` to the unit sphere `S³`. -/
def radialNormalize (x : R4) : R4 := (euclidNorm x)⁻¹ • x

/-- Stereographic projection of `S³ \ {N}` from the unit vector `N` onto the
hyperplane `N^⊥ ≅ ℝ³`: `y ↦ (y - ⟨y, N⟩ N) / (1 - ⟨y, N⟩)`. -/
def stereographicFrom (N y : R4) : R4 :=
  (1 - dot4 y N)⁻¹ • (y - dot4 y N • N)

/-- The oriented volume of `a, b, c ∈ N^⊥`: `det(-N, a, b, c)` (rows). -/
def volumeIn (N a b c : R4) : ℝ :=
  Matrix.det (Matrix.of ![-N, a, b, c])

/-- The Gauss linking integral of two `1`-periodic loops `γ₁, γ₂` in `S³`, after
stereographic projection from `N`:
`(4π)⁻¹ ∫₀¹ ∫₀¹ vol(A'(s), B'(t), A(s) - B(t)) / |A(s) - B(t)|³ dt ds`,
`A = σ_N ∘ γ₁`, `B = σ_N ∘ γ₂`. -/
def gaussLinkingIntegral (N : R4) (γ₁ γ₂ : ℝ → R4) : ℝ :=
  (4 * Real.pi)⁻¹ * ∫ s in (0 : ℝ)..1, ∫ t in (0 : ℝ)..1,
    volumeIn N (deriv (fun s => stereographicFrom N (γ₁ s)) s)
      (deriv (fun t => stereographicFrom N (γ₂ t)) t)
      (stereographicFrom N (γ₁ s) - stereographicFrom N (γ₂ t)) /
    euclidNorm (stereographicFrom N (γ₁ s) - stereographicFrom N (γ₂ t)) ^ 3

/-- `n` is the linking number of the loops `γ₁, γ₂` in `S³`: some unit vector `N`
misses both loops, and the Gauss integral from every such `N` equals `n`. -/
def IsLinkingNumber (γ₁ γ₂ : ℝ → R4) (n : ℤ) : Prop :=
  (∃ N : R4, euclidNorm N = 1 ∧ ∀ s, γ₁ s ≠ N ∧ γ₂ s ≠ N) ∧
  ∀ N : R4, euclidNorm N = 1 → (∀ s, γ₁ s ≠ N ∧ γ₂ s ≠ N) →
    gaussLinkingIntegral N γ₁ γ₂ = n

/-- The loop `s ↦ x(Ts)/|x(Ts)|`, `s ∈ ℝ/ℤ`, of a periodic orbit, in `S³`. -/
def orbitLoop {H : R4 → ℝ} (P : PeriodicOrbit H) : ℝ → R4 :=
  fun s => radialNormalize (P.x (P.T * s))

/-- The push-off `s ↦ (x(Ts) + ε Z₁(x(Ts))) / |·|` of `P` along `ξ`, in `S³`. -/
def pushOffLoop (H : R4 → ℝ) (P : PeriodicOrbit H) (ε : ℝ) : ℝ → R4 :=
  fun s => radialNormalize (P.x (P.T * s) + ε • xiFrame1 H (P.x (P.T * s)))

/-- `sl(P) = n`: for all small `ε > 0`, `P` and its push-off along `ξ` have linking
number `n`. -/
def HasSelfLinkingNumber (H : R4 → ℝ) (P : PeriodicOrbit H) (n : ℤ) : Prop :=
  ∃ ε₀ : ℝ, 0 < ε₀ ∧ ∀ ε : ℝ, 0 < ε → ε < ε₀ →
    IsLinkingNumber (orbitLoop P) (pushOffLoop H P ε) n

/-- Two periodic orbits are linked non-trivially: their loops have a linking number,
and it is non-zero. -/
def LinksNontrivially {H : R4 → ℝ} (P Q : PeriodicOrbit H) : Prop :=
  ∃ n : ℤ, n ≠ 0 ∧ IsLinkingNumber (orbitLoop P) (orbitLoop Q) n

end

end HryniewiczCriterion

Source

Hryniewicz, Systems of global surfaces of section for dynamically convex Reeb flows on the 3-sphere, J. Symplectic Geom. 12 (2014) 791-862, https://arxiv.org/abs/1105.2077, Definition 1.5, p. 3

Read-back

What the Lean code literally says, in plain math · claude-opus-5-5

Read-back: `Def_HryniewiczCriterion_SelfLinking`

Namespace HryniewiczCriterion; uses Def_HryniewiczCriterion_Basic: $\mathbb R^4$ with coordinates $x_0,\dots,x_3$ ; Euclidean inner product $\langle x,y\rangle=\sum_i x_iy_i$ and norm $|x|=\sqrt{\langle x,x\rangle}$ ; periodic orbits $P=(x_P,T_P)$ of $H$ (a trajectory on $\{H=1\}$ with a positive, not necessarily minimal, period $T_P$ ); and the vector $\xi_1(x)=|x|^{-1}\bigl(Q_2x-\tfrac{DH_x(Q_2x)}{DH_x(x)}\,x\bigr)$ with $Q_2x=(x_3,x_2,-x_1,-x_0)$ (quotient $:=0$ if $DH_x(x)=0$ ; $\xi_1(0)=0$ ).

`radialNormalize`

\nu(x)=|x|^{-1}x ,

with junk value $\nu(0)=0$ .

`stereographicFrom`

For $N,y\in\mathbb R^4$ :

\sigma_N(y)=\frac{1}{1-\langle y,N\rangle}\Bigl(y-\langle y,N\rangle N\Bigr)\in\mathbb R^4 .

No normalisation of $N$ is assumed here. If $|N|=1$ , the value lies in the hyperplane $N^\perp$ (in general $\langle\sigma_N(y),N\rangle=\langle y,N\rangle(1-|N|^2)/(1-\langle y,N\rangle)$ ). Junk value: if $\langle y,N\rangle=1$ the prefactor is $0$ and $\sigma_N(y)=0$ . The output is a point of $\mathbb R^4$ , not coordinates in a chosen basis of $N^\perp$ .

`volumeIn`

For $N,a,b,c\in\mathbb R^4$ :

\operatorname{vol}_N(a,b,c)=\det\begin{pmatrix}-N\\ a\\ b\\ c\end{pmatrix},

the $4\times4$ determinant whose rows are $-N,a,b,c$ in that order.

`gaussLinkingIntegral`

For $N\in\mathbb R^4$ and curves $\gamma_1,\gamma_2:\mathbb R\to\mathbb R^4$ , write $\alpha(s)=\sigma_N(\gamma_1(s))$ , $\beta(t)=\sigma_N(\gamma_2(t))$ . Then

G_N(\gamma_1,\gamma_2)=\frac{1}{4\pi}\int_0^1\!\!\int_0^1\frac{\operatorname{vol}_N\bigl(\alpha'(s),\ \beta'(t),\ \alpha(s)-\beta(t)\bigr)}{|\alpha(s)-\beta(t)|^3}\,dt\,ds ,

with the inner integral over $t$ and the outer over $s$ , both oriented integrals from $0$ to $1$ , and $|\cdot|$ the Euclidean norm.

Junk values: $\alpha'(s)$ (resp. $\beta'(t)$ ) is $0$ where the composed curve is not differentiable; where $\alpha(s)=\beta(t)$ the quotient is $\cdot/0=0$ ; if the inner integrand is not integrable in $t$ the inner integral is $0$ , and likewise for the outer integral. Only the values of $\gamma_1,\gamma_2$ on $[0,1]$ (and their derivatives there) enter; the curves are not required to be closed, continuous, disjoint, or on the unit sphere.

`IsLinkingNumber`

For curves $\gamma_1,\gamma_2:\mathbb R\to\mathbb R^4$ and $n\in\mathbb Z$ , both of:

there exists $N$ with $|N|=1$ such that $\gamma_1(s)\neq N$ and $\gamma_2(s)\neq N$ for all $s\in\mathbb R$ ;
for every $N$ with $|N|=1$ such that $\gamma_1(s)\neq N$ and $\gamma_2(s)\neq N$ for all $s\in\mathbb R$ :

G_N(\gamma_1,\gamma_2)=n .

The avoidance condition is over all real parameters $s$ , not only $s\in[0,1]$ . Because of (1), at most one integer $n$ can satisfy this for given $\gamma_1,\gamma_2$ . Nothing excludes $\gamma_1$ and $\gamma_2$ intersecting (or being equal); in that case the integrand uses the junk value $0$ on the coincidence set.

`orbitLoop`

For a periodic orbit $P$ :

\gamma_P(s)=\nu\bigl(x_P(T_P\,s)\bigr),\qquad s\in\mathbb R,

the orbit radially projected to the unit sphere $S^3$ (or $0$ at times where $x_P=0$ ), reparametrised so that $s\in[0,1]$ covers the time interval $[0,T_P]$ (i.e. the period carried by $P$ , possibly a multiple of the minimal period).

`pushOffLoop`

For $H$ , $P$ and $\varepsilon\in\mathbb R$ :

\gamma_{P,\varepsilon}(s)=\nu\Bigl(x_P(T_Ps)+\varepsilon\,\xi_1\bigl(x_P(T_Ps)\bigr)\Bigr),

the orbit displaced by $\varepsilon$ times the vector $\xi_1$ (only $\xi_1$ , not $\xi_2$ ) and then radially projected to $S^3$ .

`HasSelfLinkingNumber`

For $H$ , $P$ and $n\in\mathbb Z$ :

\exists\,\varepsilon_0>0\ \ \forall\,\varepsilon\in(0,\varepsilon_0):\ \ n \text{ is the linking number (in the sense above) of } \gamma_P \text{ and } \gamma_{P,\varepsilon}.

Only positive $\varepsilon$ are used. Since each such $\varepsilon$ determines $n$ uniquely (if it works at all), at most one $n$ satisfies this for given $(H,P)$ .

`LinksNontrivially`

For two periodic orbits $P,Q$ of the same $H$ :

\exists\,n\in\mathbb Z,\ n\neq0,\ \text{such that } n \text{ is the linking number of } \gamma_P \text{ and } \gamma_Q .

$P$ and $Q$ are not required to be distinct or to have disjoint images.

Human review

Endorsed by Shuze Chen · Oct 6, 2026
Confirmed by the moderator at approval.
Endorsed by Mazecto · Oct 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Linking numbers in S3S^3S3 and the self-linking number of a periodic orbit

Read-back: Def_HryniewiczCriterion_SelfLinking

radialNormalize

stereographicFrom

volumeIn

gaussLinkingIntegral

IsLinkingNumber

orbitLoop

pushOffLoop

HasSelfLinkingNumber

LinksNontrivially