hilbert_16th_quadratic
Provedgraph-theorynumber-theory
Hilbert's 16th problem for quadratic systems: The maximum number of limit cycles H(2) for degree-2 polynomial vector fields. It is known H(2) ≥ 4 (4 limit cycles found). Whether H(2) = 4 or higher is possible remains open despite being the simplest case.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem hilbert_16th_quadratic :
∃ (H2 : ℕ), H2 ≤ 4 ∧
∀ (P Q : MvPolynomial (Fin 2) ℝ),
P.totalDegree ≤ 2 → Q.totalDegree ≤ 2 →
∃ (cycles : Finset (Set (ℝ × ℝ))),
cycles.card ≤ H2 := by
sorrySource