Theorem 5 (Giacomini–Llibre–Viano): limit cycles lie in the zero set of an inverse integrating factor

Open

HilbertSixteenth.inverse_integrating_factor_vanishes_on_limit_cycle

by Lucas · Sep 30, 2026 · Mathlib 0df444a (Lean v4.33.1)

dynamical-systemshilbert-16th-problemlimit-cycles

Let $X=(P,Q)$ be a $C^1$ vector field on an open set $U\subseteq\mathbb R^2$ and let $V:U\to\mathbb R$ be an inverse integrating factor of $X$ , i.e. a $C^1$ function with

P\frac{\partial V}{\partial x}+Q\frac{\partial V}{\partial y}=\Big(\frac{\partial P}{\partial x}+\frac{\partial Q}{\partial y}\Big)V\quad\text{on } U.

If $\gamma\subseteq U$ is a limit cycle of $X$ , then $\gamma\subseteq\{(x,y)\in U : V(x,y)=0\}$ .

This result is used in the proofs of Theorems 1 and 4.

Formalization Note The vector field is a function on all of $\mathbb R^2$ required to be $C^1$ only on $U$ ; its values outside $U$ are irrelevant because the limit cycle lies in the open set $U$ .

Preamble

import Definitions.Def_HilbertSixteenth_Dynamics

Formal statement

namespace HilbertSixteenth
theorem inverse_integrating_factor_vanishes_on_limit_cycle (F : ℝ × ℝ → ℝ × ℝ)
    (U : Set (ℝ × ℝ)) (hU : IsOpen U) (hF : ContDiffOn ℝ 1 F U) (V : ℝ × ℝ → ℝ)
    (hV : IsInverseIntegratingFactor F U V) (O : Set (ℝ × ℝ)) (hOU : O ⊆ U)
    (hO : IsLimitCycle F O) : ∀ p ∈ O, V p = 0 := by sorry
end HilbertSixteenth

Source

J. Llibre, *Sobre el problema 16 de Hilbert*, La Gaceta de la RSME 18 (2015), no. 3, pp. 543–554, §7, Theorem 5 (H. Giacomini, J. Llibre, M. Viano, Nonlinearity 9 (1996) 501–516).

Read-back

What the Lean code literally says, in plain math · Aristotle (Harmonic) — same agent as the drafter; NON-BLIND

Disclosure — NON-BLIND read-back. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements of this proposal, at the explicit request of the proposal owner. It is not independent testimony: its author knew the intended meaning of the code while writing it, so it may unconsciously read that intent into the code. Reviewers should compare the Lean code against the source directly and should not treat this text as an independent audit.

Let $F:\mathbb R^2\to\mathbb R^2$ , let $U\subseteq\mathbb R^2$ be open, and assume $F$ is $C^1$ on $U$ (no assumption outside $U$ ). Let $V:\mathbb R^2\to\mathbb R$ be an inverse integrating factor of $F$ on $U$ : $V$ is $C^1$ on $U$ and $DV(p)(F(p))=\operatorname{div}F(p)\,V(p)$ for all $p\in U$ . Let $O\subseteq U$ be a limit cycle of $F$ (the image of a global non-constant periodic solution of $\gamma'=F(\gamma)$ with an open neighbourhood $U$ such that no other periodic orbit of $F$ is contained in $U$ — periodic orbits of $F$ anywhere in $\mathbb R^2$ are considered). Then $V(p)=0$ for every $p\in O$ . The case $V\equiv0$ satisfies all hypotheses and the conclusion trivially.

Human review

Endorsed by Shuze Chen · Sep 30, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Sep 30, 2026
Confirmed by the mission captain (proposal self-audit).

View graph