Prove2Me
Navigate
DiscoverCollectionsFormalpediaGalaxyBlogsUsersMomentumMy Missions+
Prove2Me
Log in
← Formalpedia

Theorem 1.7 (open book): an unknotted orbit with sl⁡=−1\operatorname{sl}=-1sl=−1 binds an adapted open book

Open
HryniewiczCriterion.adapted_open_book_of_unknotted_selfLinking

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

contact-geometrydynamical-systemssymplectic-geometry

Let S=H−1(1)⊂R4S=H^{-1}(1)\subset\mathbb{R}^4S=H−1(1)⊂R4 be a strictly star-shaped energy surface whose flow is dynamically convex. Let Pˉ\bar PPˉ be a prime periodic orbit that is unknotted with sl⁡(Pˉ)=−1\operatorname{sl}(\bar P)=-1sl(Pˉ)=−1. Then Pˉ\bar PPˉ is the binding of an open book decomposition of SSS with disk-like pages, adapted to the flow: every page is a disk-like global surface of section whose oriented boundary is Pˉ\bar PPˉ.

This strengthens the "if" direction of Hryniewicz's criterion from a single disk to a whole family of disk-like global sections that fill S∖PˉS\setminus\bar PS∖Pˉ.

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

/-- Hryniewicz, Theorem 1.7, second sentence: a prime, unknotted periodic orbit with
`sl = -1` of a dynamically convex flow is the binding of an adapted open book
decomposition with disk-like pages. -/
theorem adapted_open_book_of_unknotted_selfLinking (H : R4 → ℝ)
    (hS : IsStrictlyStarShapedLevel H) (hdc : IsDynamicallyConvex H)
    (P : PeriodicOrbit H) (hP : P.IsPrime)
    (hu : IsUnknotted H P) (hsl : HasSelfLinkingNumber H P (-1)) :
    HasAdaptedDiskOpenBook H P := 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, second sentence
Read-back

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

Read-back: adapted_open_book_of_unknotted_selfLinking

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​;
  • (hu)(hu)(hu) PPP is unknotted: there is a C∞C^\inftyC∞ map e:R2→R4e:\mathbb R^2\to\mathbb R^4e:R2→R4, injective with injective derivative on the closed unit disk 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;
  • (hsl)(hsl)(hsl) PPP has self-linking number −1-1−1: there is ε0>0\varepsilon_0>0ε0​>0 such that for all 0<ε<ε00<\varepsilon<\varepsilon_00<ε<ε0​ the loops ℓP(s)=ν(xP(TPs))\ell_P(s)=\nu(x_P(T_Ps))ℓP​(s)=ν(xP​(TP​s)) and ℓPε(s)=ν(xP(TPs)+ε ξ1(xP(TPs)))\ell_P^\varepsilon(s)=\nu\bigl(x_P(T_Ps)+\varepsilon\,\xi_1(x_P(T_Ps))\bigr)ℓPε​(s)=ν(xP​(TP​s)+εξ1​(xP​(TP​s))) have linking number −1-1−1 in the Gauss-integral sense defined below.

Conclusion. PPP has an adapted disk open book: there exists 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), jointly C∞C^\inftyC∞ and 111-periodic in ϑ\varthetaϑ, such that

  • every page FϑF_\varthetaFϑ​ is a disk-like global section map for (H,P)(H,P)(H,P) (smooth disk embedding of D‾\overline{\mathbb D}D into Σ\SigmaΣ with boundary circle mapped onto im⁡P\operatorname{im}PimP, XHX_HXH​ not tangent to the page at interior points, and every trajectory not starting on im⁡P\operatorname{im}PimP meets Fϑ(D‾)F_\vartheta(\overline{\mathbb D})Fϑ​(D) both after and before every time aaa);
  • Fϑ(cos⁡2πt,sin⁡2πt)=xP(TPt)F_\vartheta(\cos2\pi t,\sin2\pi t)=x_P(T_Pt)Fϑ​(cos2πt,sin2πt)=xP​(TP​t) for all ϑ,t\vartheta,tϑ,t;
  • ω0(∂u0Fϑ,∂u1Fϑ)>0\omega_0(\partial_{u_0}F_\vartheta,\partial_{u_1}F_\vartheta)>0ω0​(∂u0​​Fϑ​,∂u1​​Fϑ​)>0 on the open disk D\mathbb DD;
  • every point of Σ∖im⁡P\Sigma\setminus\operatorname{im}PΣ∖imP is F(ϑ,u)F(\vartheta,u)F(ϑ,u) for exactly one (ϑ,u)∈[0,1)×D(\vartheta,u)\in[0,1)\times\mathbb D(ϑ,u)∈[0,1)×D;
  • DF(ϑ,u)DF(\vartheta,u)DF(ϑ,u) is injective for all ϑ∈R\vartheta\in\mathbb Rϑ∈R, u∈Du\in\mathbb Du∈D.

Edge cases. The binding condition fixes the boundary parametrization of every page to t↦xP(TPt)t\mapsto x_P(T_Pt)t↦xP​(TP​t) with the given base point xP(0)x_P(0)xP​(0) and the given direction of c(t)=(cos⁡2πt,sin⁡2πt)c(t)=(\cos2\pi t,\sin2\pi t)c(t)=(cos2πt,sin2πt). The positivity condition fixes an orientation of each page relative to ω0\omega_0ω0​. This is an implication only (no converse is stated).


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