Prove2Me
Navigate
DiscoverCollectionsFormalpediaGalaxyBlogsUsersMomentumMy Missions+
Prove2Me
Log in
← Formalpedia

Hryniewicz's criterion: a prime orbit bounds a disk-like global section iff it is unknotted with sl⁡=−1\operatorname{sl}=-1sl=−1

Open
HryniewiczCriterion.hryniewicz_criterion

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

contact-geometrydynamical-systemssymplectic-geometry

Let H:R4→RH:\mathbb{R}^4\to\mathbb{R}H:R4→R be smooth with S=H−1(1)S=H^{-1}(1)S=H−1(1) strictly star-shaped, and assume the Hamiltonian flow of XHX_HXH​ on SSS, a positive reparametrization of the Reeb flow of λ0∣S\lambda_0|_Sλ0​∣S​, is dynamically convex. Then for every prime periodic orbit Pˉ\bar PPˉ on SSS,

Pˉ bounds a disk-like global surface of section  ⟺  Pˉ is unknotted and sl⁡(Pˉ)=−1.\bar P\ \text{bounds a disk-like global surface of section}\iff\bar P\ \text{is unknotted and}\ \operatorname{sl}(\bar P)=-1.Pˉ bounds a disk-like global surface of section⟺Pˉ is unknotted and sl(Pˉ)=−1.

No non-degeneracy assumption is made. The criterion reduces the existence of a disk-like global section, a global dynamical property, to a topological check on the orbit.

Formalization Note Hryniewicz states the theorem for any dynamically convex contact form on S3S^3S3. Such a form is tight, and every tight contact form on S3S^3S3 is diffeomorphic to λ0∣S\lambda_0|_Sλ0​∣S​ on a star-shaped SSS (Eliashberg). That reduction is not part of this statement; Hryniewicz makes the same reduction at the start of Section 3. The flow is that of XHX_HXH​, which has the same orbits, global sections, unknots, self-linking numbers and indices as the Reeb flow.

Preamble
import Definitions.Def_HryniewiczCriterion_ConleyZehnder
import Definitions.Def_HryniewiczCriterion_GlobalSection
import Definitions.Def_HryniewiczCriterion_SelfLinking
Formal statement
namespace HryniewiczCriterion

/-- Hryniewicz's criterion (Theorem 1.7): for a dynamically convex flow on a strictly
star-shaped energy surface in `ℝ⁴`, a prime periodic orbit bounds a disk-like global
surface of section if and only if it is unknotted and has self-linking number `-1`. -/
theorem hryniewicz_criterion (H : R4 → ℝ)
    (hS : IsStrictlyStarShapedLevel H) (hdc : IsDynamicallyConvex H)
    (P : PeriodicOrbit H) (hP : P.IsPrime) :
    BoundsDiskLikeGlobalSection H P ↔ IsUnknotted H P ∧ HasSelfLinkingNumber H P (-1) := by sorry

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, Theorem 1.7, p. 3, first sentence
Read-back

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

Read-back: hryniewicz_criterion

Binders and hypotheses. Let H:R4→RH:\mathbb R^4\to\mathbb RH:R4→R be any function, and assume:

  • (hS)(hS)(hS) the level Σ=H−1(1)\Sigma=H^{-1}(1)Σ=H−1(1) is a strictly star-shaped level of HHH (HHH is C∞C^\inftyC∞, each ray from the origin meets Σ\SigmaΣ exactly once, and DH(x) x>0DH(x)\,x>0DH(x)x>0 on Σ\SigmaΣ);
  • (hdc)(hdc)(hdc) HHH is dynamically convex (every periodic orbit, of every period, with every linearized flow, has index μ≥3\mu\ge3μ≥3; see below);
  • PPP is a periodic orbit of XHX_HXH​ on Σ\SigmaΣ (a trajectory xPx_PxP​ with a period TP>0T_P>0TP​>0);
  • (hP)(hP)(hP) PPP is prime: xP(t)≠xP(0)x_P(t)\neq x_P(0)xP​(t)=xP​(0) for 0<t<TP0<t<T_P0<t<TP​.

Conclusion (an equivalence).

(P bounds a disk-like global section)  ⟺  (P is unknotted  and  P has self-linking number −1),\Bigl(P \text{ bounds a disk-like global section}\Bigr)\iff\Bigl(P\text{ is unknotted}\ \text{ and }\ P \text{ has self-linking number } -1\Bigr),(P bounds a disk-like global section)⟺(P is unknotted  and  P has self-linking number −1),

where:

  • left side: there exists e:R2→R4e:\mathbb R^2\to\mathbb R^4e:R2→R4, C∞C^\inftyC∞, injective with injective derivative on D‾\overline{\mathbb D}D, with e(D‾)⊆Σe(\overline{\mathbb D})\subseteq\Sigmae(D)⊆Σ, e(S1)=im⁡Pe(S^1)=\operatorname{im}Pe(S1)=imP, XH(e(u))∉range⁡De(u)X_H(e(u))\notin\operatorname{range}De(u)XH​(e(u))∈/rangeDe(u) for all uuu in the open disk D\mathbb DD, and such that every trajectory yyy with y(0)∉im⁡Py(0)\notin\operatorname{im}Py(0)∈/imP meets e(D‾)e(\overline{\mathbb D})e(D) at some time >a>a>a and at some time <a<a<a, for every a∈Ra\in\mathbb Ra∈R;
  • right side, first part: there exists a C∞C^\inftyC∞ e:R2→R4e:\mathbb R^2\to\mathbb R^4e:R2→R4, injective with injective derivative on D‾\overline{\mathbb D}D, with e(D‾)⊆Σe(\overline{\mathbb D})\subseteq\Sigmae(D)⊆Σ and e(S1)=im⁡Pe(S^1)=\operatorname{im}Pe(S1)=imP;
  • right side, second part: there is ε0>0\varepsilon_0>0ε0​>0 such that for every ε∈(0,ε0)\varepsilon\in(0,\varepsilon_0)ε∈(0,ε0​) the loops
ℓP(s)=xP(TPs)∣xP(TPs)∣,ℓPε(s)=xP(TPs)+ε ξ1(xP(TPs))∣xP(TPs)+ε ξ1(xP(TPs))∣\ell_P(s)=\frac{x_P(T_Ps)}{|x_P(T_Ps)|},\qquad \ell_P^\varepsilon(s)=\frac{x_P(T_Ps)+\varepsilon\,\xi_1(x_P(T_Ps))}{\bigl|x_P(T_Ps)+\varepsilon\,\xi_1(x_P(T_Ps))\bigr|}ℓP​(s)=∣xP​(TP​s)∣xP​(TP​s)​,ℓPε​(s)=​xP​(TP​s)+εξ1​(xP​(TP​s))​xP​(TP​s)+εξ1​(xP​(TP​s))​

have linking number −1-1−1 (some unit NNN avoided by both loops on R\mathbb RR exists, and for every such NNN the Gauss integral GN(ℓP,ℓPε)=−1G_N(\ell_P,\ell_P^\varepsilon)=-1GN​(ℓP​,ℓPε​)=−1).

Edge cases. The left side contains no orientation condition and no condition on the direction of the boundary orbit; the self-linking number on the right is computed with the specific frame vector ξ1\xi_1ξ1​ and with the given parametrization s↦xP(TPs)s\mapsto x_P(T_Ps)s↦xP​(TP​s), s∈[0,1]s\in[0,1]s∈[0,1]. Both directions of the equivalence are asserted under (hS)(hS)(hS), (hdc)(hdc)(hdc), (hP)(hP)(hP).


Unfolded definitions used above

Throughout, R4\mathbb R^4R4 is the space of functions {0,1,2,3}→R\{0,1,2,3\}\to\mathbb R{0,1,2,3}→R (with the sup norm as its normed-space structure), points are written x=(x0,x1,x2,x3)x=(x_0,x_1,x_2,x_3)x=(x0​,x1​,x2​,x3​), and R2\mathbb R^2R2 (points u=(u0,u1)u=(u_0,u_1)u=(u0​,u1​)) is likewise {0,1}→R\{0,1\}\to\mathbb R{0,1}→R. DH(x)DH(x)DH(x) denotes the Fréchet derivative of HHH at xxx, which is by convention the zero map wherever HHH is not differentiable; similarly for every other derivative below. Divisions by 000 and inverses of 000 evaluate to 000.

Basic objects.

  • Liouville form and standard symplectic form:
λx(v)=12 (x0v1−x1v0+x2v3−x3v2),ω0(u,v)=u0v1−u1v0+u2v3−u3v2.\lambda_x(v)=\tfrac12\,(x_0v_1-x_1v_0+x_2v_3-x_3v_2),\qquad \omega_0(u,v)=u_0v_1-u_1v_0+u_2v_3-u_3v_2 .λx​(v)=21​(x0​v1​−x1​v0​+x2​v3​−x3​v2​),ω0​(u,v)=u0​v1​−u1​v0​+u2​v3​−u3​v2​.
  • Euclidean inner product and norm: ⟨x,y⟩=∑i=03xiyi\langle x,y\rangle=\sum_{i=0}^3 x_iy_i⟨x,y⟩=∑i=03​xi​yi​, ∣x∣=⟨x,x⟩|x|=\sqrt{\langle x,x\rangle}∣x∣=⟨x,x⟩​.
  • Partial derivatives ∂iH(x)=DH(x) ei\partial_iH(x)=DH(x)\,e_i∂i​H(x)=DH(x)ei​ (eie_iei​ the iii-th standard basis vector), and the Hamiltonian vector field
XH(x)=(−∂1H(x), ∂0H(x), −∂3H(x), ∂2H(x)).X_H(x)=\bigl(-\partial_1H(x),\ \partial_0H(x),\ -\partial_3H(x),\ \partial_2H(x)\bigr).XH​(x)=(−∂1​H(x), ∂0​H(x), −∂3​H(x), ∂2​H(x)).
  • Energy surface Σ={x∈R4:H(x)=1}\Sigma=\{x\in\mathbb R^4: H(x)=1\}Σ={x∈R4:H(x)=1}.
  • Strictly star-shaped level (hypothesis hShShS): (i) H:R4→RH:\mathbb R^4\to\mathbb RH:R4→R is C∞C^\inftyC∞ on all of R4\mathbb R^4R4; (ii) for every u≠0u\neq 0u=0 there is exactly one r>0r>0r>0 with H(ru)=1H(ru)=1H(ru)=1; (iii) for every xxx with H(x)=1H(x)=1H(x)=1, DH(x) x>0DH(x)\,x>0DH(x)x>0. (Consequence of (iii): H(0)≠1H(0)\neq 1H(0)=1, so 0∉Σ0\notin\Sigma0∈/Σ, and XH≠0X_H\neq 0XH​=0 on Σ\SigmaΣ.)
  • Trajectory: a map y:R→R4y:\mathbb R\to\mathbb R^4y:R→R4 that is differentiable at every t∈Rt\in\mathbb Rt∈R with y′(t)=XH(y(t))y'(t)=X_H(y(t))y′(t)=XH​(y(t)), and with H(y(t))=1H(y(t))=1H(y(t))=1 for all t∈Rt\in\mathbb Rt∈R.
  • Periodic orbit PPP: a pair (xP,TP)(x_P,T_P)(xP​,TP​) consisting of a trajectory xP:R→R4x_P:\mathbb R\to\mathbb R^4xP​:R→R4 and a number TP>0T_P>0TP​>0 with xP(t+TP)=xP(t)x_P(t+T_P)=x_P(t)xP​(t+TP​)=xP​(t) for all ttt. TPT_PTP​ is a period, not necessarily the minimal one; the same geometric orbit gives many different PPP (any time shift, any positive multiple of the minimal period). Its image is im⁡P={xP(t):t∈R}\operatorname{im}P=\{x_P(t):t\in\mathbb R\}imP={xP​(t):t∈R}.
  • Prime: xP(t)≠xP(0)x_P(t)\neq x_P(0)xP​(t)=xP​(0) for all 0<t<TP0<t<T_P0<t<TP​ (i.e. TPT_PTP​ is the minimal period).
  • Two fixed linear maps Q1(x)=(−x2, x3, x0, −x1)Q_1(x)=(-x_2,\,x_3,\,x_0,\,-x_1)Q1​(x)=(−x2​,x3​,x0​,−x1​) and Q2(x)=(x3, x2, −x1, −x0)Q_2(x)=(x_3,\,x_2,\,-x_1,\,-x_0)Q2​(x)=(x3​,x2​,−x1​,−x0​), and the frame vectors
ξ1(x)=1∣x∣(Q2x−DH(x) Q2xDH(x) x x),ξ2(x)=1∣x∣(Q1x−DH(x) Q1xDH(x) x x)\xi_1(x)=\frac{1}{|x|}\Bigl(Q_2x-\frac{DH(x)\,Q_2x}{DH(x)\,x}\,x\Bigr),\qquad \xi_2(x)=\frac{1}{|x|}\Bigl(Q_1x-\frac{DH(x)\,Q_1x}{DH(x)\,x}\,x\Bigr)ξ1​(x)=∣x∣1​(Q2​x−DH(x)xDH(x)Q2​x​x),ξ2​(x)=∣x∣1​(Q1​x−DH(x)xDH(x)Q1​x​x)

(with the junk convention 1/0=01/0=01/0=0).

Dynamical convexity (hypothesis hdchdchdc).

  • ρ(s)=(cos⁡s,sin⁡s)∈R2\rho(s)=(\cos s,\sin s)\in\mathbb R^2ρ(s)=(coss,sins)∈R2.
  • Given a path of real 2×22\times22×2 matrices φ:R→M2(R)\varphi:\mathbb R\to M_2(\mathbb R)φ:R→M2​(R) and s∈Rs\in\mathbb Rs∈R, an angle lift from sss is a function θ:R→R\theta:\mathbb R\to\mathbb Rθ:R→R, continuous on [0,1][0,1][0,1], with θ(0)=s\theta(0)=sθ(0)=s, such that for every t∈[0,1]t\in[0,1]t∈[0,1] there is r>0r>0r>0 with φ(t) ρ(s)=r ρ(θ(t))\varphi(t)\,\rho(s)=r\,\rho(\theta(t))φ(t)ρ(s)=rρ(θ(t)). (No continuity or invertibility of φ\varphiφ is assumed; if φ(t)ρ(s)=0\varphi(t)\rho(s)=0φ(t)ρ(s)=0 for some t∈[0,1]t\in[0,1]t∈[0,1], no lift from sss exists.)
  • Winding set W(φ)={θ(1)−s2π: s∈[0,2π], θ an angle lift of φ from s}⊆RW(\varphi)=\bigl\{\tfrac{\theta(1)-s}{2\pi}:\ s\in[0,2\pi],\ \theta \text{ an angle lift of }\varphi\text{ from }s\bigr\}\subseteq\mathbb RW(φ)={2πθ(1)−s​: s∈[0,2π], θ an angle lift of φ from s}⊆R.
  • Index: let a=inf⁡W(φ)a=\inf W(\varphi)a=infW(φ), b=sup⁡W(φ)b=\sup W(\varphi)b=supW(φ) (each set to 000 if W(φ)W(\varphi)W(φ) is empty or unbounded on that side), and k=⌈b⌉k=\lceil b\rceilk=⌈b⌉ (least integer ≥b\ge b≥b). Then
μ(φ)={2(k−1)if a≤k−1,2k−1otherwise.\mu(\varphi)=\begin{cases}2(k-1)&\text{if } a\le k-1,\\ 2k-1&\text{otherwise.}\end{cases}μ(φ)={2(k−1)2k−1​if a≤k−1,otherwise.​

In particular, if W(φ)=∅W(\varphi)=\emptysetW(φ)=∅ then a=b=0a=b=0a=b=0, k=0k=0k=0 and μ(φ)=−1\mu(\varphi)=-1μ(φ)=−1.

  • A linearized flow along a curve x:R→R4x:\mathbb R\to\mathbb R^4x:R→R4 is a map Y:R→L(R4,R4)Y:\mathbb R\to L(\mathbb R^4,\mathbb R^4)Y:R→L(R4,R4) (continuous linear maps) with Y(0)=IdY(0)=\mathrm{Id}Y(0)=Id and, for every t∈Rt\in\mathbb Rt∈R, YYY differentiable at ttt with Y′(t)=DXH(x(t))∘Y(t)Y'(t)=DX_H(x(t))\circ Y(t)Y′(t)=DXH​(x(t))∘Y(t), where DXHDX_HDXH​ is the Fréchet derivative of the vector field XHX_HXH​.
  • Projection along XHX_HXH​: πx(v)=v−λx(v)λx(XH(x)) XH(x)\pi_x(v)=v-\dfrac{\lambda_x(v)}{\lambda_x(X_H(x))}\,X_H(x)πx​(v)=v−λx​(XH​(x))λx​(v)​XH​(x).
  • Coordinates: cx(v)=(ω0(v,ξ2(x)), ω0(ξ1(x),v))∈R2c_x(v)=\bigl(\omega_0(v,\xi_2(x)),\ \omega_0(\xi_1(x),v)\bigr)\in\mathbb R^2cx​(v)=(ω0​(v,ξ2​(x)), ω0​(ξ1​(x),v))∈R2.
  • For a periodic orbit PPP and a map YYY, the matrix path ΦP,Y:R→M2(R)\Phi_{P,Y}:\mathbb R\to M_2(\mathbb R)ΦP,Y​:R→M2​(R) has jjj-th column (j=1,2j=1,2j=1,2)
ΦP,Y(τ) ej=cxP(TPτ)(πxP(TPτ)(Y(TPτ) ξj(xP(0)))).\Phi_{P,Y}(\tau)\,e_j=c_{x_P(T_P\tau)}\Bigl(\pi_{x_P(T_P\tau)}\bigl(Y(T_P\tau)\,\xi_j(x_P(0))\bigr)\Bigr).ΦP,Y​(τ)ej​=cxP​(TP​τ)​(πxP​(TP​τ)​(Y(TP​τ)ξj​(xP​(0)))).
  • HHH is dynamically convex means: for every periodic orbit PPP (any period TPT_PTP​, so including all multiple covers and time shifts) and every linearized flow YYY along xPx_PxP​, μ(ΦP,Y)≥3\mu(\Phi_{P,Y})\ge 3μ(ΦP,Y​)≥3. (If for some PPP no linearized flow exists, the condition is vacuous for that PPP.)

Disks and global sections.

  • D‾={u:u02+u12≤1}\overline{\mathbb D}=\{u: u_0^2+u_1^2\le1\}D={u:u02​+u12​≤1}, D={u:u02+u12<1}\mathbb D=\{u:u_0^2+u_1^2<1\}D={u:u02​+u12​<1}, S1={u:u02+u12=1}S^1=\{u:u_0^2+u_1^2=1\}S1={u:u02​+u12​=1}, and c(t)=(cos⁡2πt, sin⁡2πt)c(t)=(\cos 2\pi t,\ \sin2\pi t)c(t)=(cos2πt, sin2πt).

  • Smooth disk embedding e:R2→R4e:\mathbb R^2\to\mathbb R^4e:R2→R4: eee is C∞C^\inftyC∞ on all of R2\mathbb R^2R2, injective on D‾\overline{\mathbb D}D, and De(u)De(u)De(u) is injective for every u∈D‾u\in\overline{\mathbb D}u∈D.

  • Disk-like global section map for (H,P)(H,P)(H,P): a map e:R2→R4e:\mathbb R^2\to\mathbb R^4e:R2→R4 such that

    1. eee is a smooth disk embedding;
    2. e(D‾)⊆Σe(\overline{\mathbb D})\subseteq\Sigmae(D)⊆Σ;
    3. e(S1)=im⁡Pe(S^1)=\operatorname{im}Pe(S1)=imP (set equality);
    4. for every u∈Du\in\mathbb Du∈D (open disk), XH(e(u))∉range⁡De(u)X_H(e(u))\notin \operatorname{range} De(u)XH​(e(u))∈/rangeDe(u);
    5. for every trajectory yyy with y(0)∉im⁡Py(0)\notin\operatorname{im}Py(0)∈/imP and every a∈Ra\in\mathbb Ra∈R, there exist t>at>at>a with y(t)∈e(D‾)y(t)\in e(\overline{\mathbb D})y(t)∈e(D) and t′<at'<at′<a with y(t′)∈e(D‾)y(t')\in e(\overline{\mathbb D})y(t′)∈e(D) (the hitting set is the image of the closed disk).

    No orientation condition is imposed.

  • PPP bounds a disk-like global section: some disk-like global section map for (H,P)(H,P)(H,P) exists.

  • PPP is unknotted: there is a smooth disk embedding eee with e(D‾)⊆Σe(\overline{\mathbb D})\subseteq\Sigmae(D)⊆Σ and e(S1)=im⁡Pe(S^1)=\operatorname{im}Pe(S1)=imP (conditions 1–3 above only).

  • Adapted disk open book for (H,P)(H,P)(H,P): a map F:R×R2→R4F:\mathbb R\times\mathbb R^2\to\mathbb R^4F:R×R2→R4, F(ϑ,u)=Fϑ(u)F(\vartheta,u)=F_\vartheta(u)F(ϑ,u)=Fϑ​(u), such that

    1. FFF is jointly C∞C^\inftyC∞;
    2. Fϑ+1=FϑF_{\vartheta+1}=F_\varthetaFϑ+1​=Fϑ​ for all ϑ\varthetaϑ;
    3. every page FϑF_\varthetaFϑ​ is a disk-like global section map for (H,P)(H,P)(H,P);
    4. (binding) Fϑ(c(t))=xP(TP t)F_\vartheta(c(t))=x_P(T_P\,t)Fϑ​(c(t))=xP​(TP​t) for all ϑ,t∈R\vartheta,t\in\mathbb Rϑ,t∈R;
    5. (positivity) for all ϑ\varthetaϑ and u∈Du\in\mathbb Du∈D, ω0(∂u0Fϑ(u), ∂u1Fϑ(u))>0\omega_0\bigl(\partial_{u_0}F_\vartheta(u),\ \partial_{u_1}F_\vartheta(u)\bigr)>0ω0​(∂u0​​Fϑ​(u), ∂u1​​Fϑ​(u))>0;
    6. (fibration) every y∈Σ∖im⁡Py\in\Sigma\setminus\operatorname{im}Py∈Σ∖imP equals F(ϑ,u)F(\vartheta,u)F(ϑ,u) for exactly one pair (ϑ,u)(\vartheta,u)(ϑ,u) with ϑ∈[0,1)\vartheta\in[0,1)ϑ∈[0,1), u∈Du\in\mathbb Du∈D;
    7. (regularity) for all ϑ∈R\vartheta\in\mathbb Rϑ∈R and u∈Du\in\mathbb Du∈D, the derivative DF(ϑ,u):R×R2→R4DF(\vartheta,u):\mathbb R\times\mathbb R^2\to\mathbb R^4DF(ϑ,u):R×R2→R4 is injective.

    "PPP has an adapted disk open book" means such an FFF exists. (Since each page is injective on D‾\overline{\mathbb D}D, the binding condition forces t↦xP(TPt)t\mapsto x_P(T_Pt)t↦xP​(TP​t) to be injective on [0,1)[0,1)[0,1), i.e. PPP prime.)

Linking and self-linking.

  • ν(x)=x/∣x∣\nu(x)=x/|x|ν(x)=x/∣x∣ (with ν(0)=0\nu(0)=0ν(0)=0).
  • For N∈R4N\in\mathbb R^4N∈R4, the map σN(y)=y−⟨y,N⟩N1−⟨y,N⟩\sigma_N(y)=\dfrac{y-\langle y,N\rangle N}{1-\langle y,N\rangle}σN​(y)=1−⟨y,N⟩y−⟨y,N⟩N​ (equal to 000 when ⟨y,N⟩=1\langle y,N\rangle=1⟨y,N⟩=1), with values in R4\mathbb R^4R4.
  • vol⁡N(a,b,c)=det⁡\operatorname{vol}_N(a,b,c)=\detvolN​(a,b,c)=det of the 4×44\times44×4 matrix with rows −N,a,b,c-N,a,b,c−N,a,b,c.
  • Gauss integral of two curves γ1,γ2:R→R4\gamma_1,\gamma_2:\mathbb R\to\mathbb R^4γ1​,γ2​:R→R4 with respect to NNN: writing α(s)=σN(γ1(s))\alpha(s)=\sigma_N(\gamma_1(s))α(s)=σN​(γ1​(s)), β(t)=σN(γ2(t))\beta(t)=\sigma_N(\gamma_2(t))β(t)=σN​(γ2​(t)),
GN(γ1,γ2)=14π∫01 ⁣ ⁣∫01vol⁡N(α′(s), β′(t), α(s)−β(t))∣α(s)−β(t)∣3 dt ds,G_N(\gamma_1,\gamma_2)=\frac1{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,GN​(γ1​,γ2​)=4π1​∫01​∫01​∣α(s)−β(t)∣3volN​(α′(s), β′(t), α(s)−β(t))​dtds,

where derivatives are 000 at non-differentiability points, the integrand is 000 where α(s)=β(t)\alpha(s)=\beta(t)α(s)=β(t), and an interval integral of a non-integrable function is 000.

  • γ1,γ2\gamma_1,\gamma_2γ1​,γ2​ have linking number n∈Zn\in\mathbb Zn∈Z: (a) there exists NNN with ∣N∣=1|N|=1∣N∣=1 such that γ1(s)≠N\gamma_1(s)\neq Nγ1​(s)=N and γ2(s)≠N\gamma_2(s)\neq Nγ2​(s)=N for all s∈Rs\in\mathbb Rs∈R; and (b) for every NNN with ∣N∣=1|N|=1∣N∣=1 avoiding both curves on all of R\mathbb RR in that sense, GN(γ1,γ2)=nG_N(\gamma_1,\gamma_2)=nGN​(γ1​,γ2​)=n. (Avoidance is required over all s∈Rs\in\mathbb Rs∈R; the integral uses only [0,1][0,1][0,1]. The curves are not required to be closed or smooth.)
  • Orbit loop ℓP(s)=ν(xP(TPs))\ell_P(s)=\nu\bigl(x_P(T_Ps)\bigr)ℓP​(s)=ν(xP​(TP​s)); push-off loop ℓPε(s)=ν(xP(TPs)+ε ξ1(xP(TPs)))\ell^{\varepsilon}_P(s)=\nu\bigl(x_P(T_Ps)+\varepsilon\,\xi_1(x_P(T_Ps))\bigr)ℓPε​(s)=ν(xP​(TP​s)+εξ1​(xP​(TP​s))). Over s∈[0,1]s\in[0,1]s∈[0,1] these traverse the period TPT_PTP​, which is the minimal period only if PPP is prime.
  • PPP has self-linking number nnn: there is ε0>0\varepsilon_0>0ε0​>0 such that for every ε∈(0,ε0)\varepsilon\in(0,\varepsilon_0)ε∈(0,ε0​), the curves ℓP,ℓPε\ell_P,\ell_P^\varepsilonℓP​,ℓPε​ have linking number nnn (in the sense above).
  • PPP links QQQ nontrivially: there is an integer n≠0n\neq0n=0 such that ℓP,ℓQ\ell_P,\ell_QℓP​,ℓQ​ have linking number nnn.
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

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