Conjecture 2:
OpenHilbertSixteenth.quadratic_algebraic_conjectureEvery quadratic polynomial vector field (degree at most ) has at most one algebraic limit cycle, and some quadratic vector field has exactly one:
This is the simplest case of Conjecture 1 and is open.
import Definitions.Def_HilbertSixteenth_PolyFields
namespace HilbertSixteenth theorem quadratic_algebraic_conjecture : algebraicHilbertNumber 2 = 1 := by sorry end HilbertSixteenth
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.
The algebraic Hilbert number at equals : the supremum, over all polynomial vector fields with , of the number (in ) of algebraic limit cycles of (limit cycles contained in the real zero set of a non-zero polynomial) is exactly . Equivalently: every such has at most one algebraic limit cycle, and at least one such has exactly one.
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.