Bounded-degree plane curves and elementary exceptional sets

Definition

LeanFormalizations_PachDeZeeuw_CurveInterface

by mysticflounder · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrygeometry

This defines real plane curves given by nonzero polynomials of bounded total degree, the irreducible subclass, and the predicate that a set is a line or a circle.

Definition code

-- Extracted dependency interfaces and their necessary proofs.
import Mathlib

set_option autoImplicit true

/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/


set_option linter.style.longLine false

 
abbrev Point2 := EuclideanSpace ℝ (Fin 2)

notation "ℝ²" => Point2


namespace PlaneCurve


def IsBoundedDegreeCurve (d : ℕ) (C : Set Point2) : Prop :=
  ∃ f : MvPolynomial (Fin 2) ℝ, f ≠ 0 ∧ f.totalDegree ≤ d ∧
    C = {x : Point2 | MvPolynomial.eval (fun i => x i) f = 0}


def IsIrreducibleCurve (d : ℕ) (C : Set Point2) : Prop :=
  ∃ f : MvPolynomial (Fin 2) ℝ, f ≠ 0 ∧ f.totalDegree ≤ d ∧ Irreducible f ∧
    C = {x : Point2 | MvPolynomial.eval (fun i => x i) f = 0}


def IsLineOrCircle (C : Set Point2) : Prop :=
  (∃ a b c : ℝ, (a, b) ≠ (0, 0) ∧ C = {p : Point2 | a * p 0 + b * p 1 = c}) ∨
  (∃ center : Point2, ∃ r : ℝ, C = Metric.sphere center r)

end PlaneCurve

View graph