Theorem 1 (sharpness of the full bound): $|\mathrm{Sym}(C)|=2d$ occurs in every degree $d\ge2$

Proved

CurveSymmetry.paper_full_sharp

by carlok · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

algebraic-geometrycurve-symmetry-leaneuclidean-geometry

Let $d\ge2$ be an integer. For $f\in\mathbb R[x,y]$ let $C=\{z\in\mathbb C: f(\operatorname{Re}z,\operatorname{Im}z)=0\}$ be its real zero set, identifying $(x,y)$ with $x+iy$ , and let $\mathrm{Sym}(C)$ be the group of all Euclidean isometries $T$ of $\mathbb C$ with $T(C)=C$ .

Then there exists $f\in\mathbb R[x,y]$ such that:

$f$ is irreducible in $\mathbb C[x,y]$ ;
$f$ has total degree $d$ ;
$C$ is infinite;
$C$ is not a circle: there are no $c\in\mathbb C$ and real $R>0$ with $C=\{z:|z-c|=R\}$ ;
the full bound of Theorem 1 is attained:

|\mathrm{Sym}(C)|=2d.

This is the sharpness of the bound $|\mathrm{Sym}(C)|\le2d$ in Theorem 1, by a curve satisfying all the hypotheses of that theorem.

Formalization Note: the order is Nat.card of a subgroup of the group ℂ ≃ᵢ ℂ of isometric bijections; since its value is positive, finiteness is part of the conclusion.

Preamble

import Definitions.Def_CurveSymmetry_01_RealLoci
import Definitions.Def_CurveSymmetry_02_FamilyBasics
import Definitions.Def_CurveSymmetry_03_IsometriesAndCharts
import Mathlib.Algebra.MvPolynomial.Nilpotent
import Mathlib.Algebra.MvPolynomial.NoZeroDivisors
import Mathlib.Algebra.Polynomial.FieldDivision
import Mathlib.Algebra.Polynomial.Reverse
import Mathlib.Analysis.Complex.Isometry
import Mathlib.Analysis.Complex.OperatorNorm
import Mathlib.Analysis.Complex.Polynomial.Basic
import Mathlib.Analysis.Normed.Affine.MazurUlam
import Mathlib.Data.Complex.Basic
import Mathlib.RingTheory.MvPolynomial.Homogeneous
import Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
import Mathlib.RingTheory.Polynomial.Eisenstein.Criterion
import Mathlib.RingTheory.Polynomial.GaussLemma
import Mathlib.RingTheory.RootsOfUnity.Complex
import Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
import Mathlib.Tactic

open CurveSymmetry
set_option autoImplicit false

Formal statement

theorem CurveSymmetry.paper_full_sharp (d : ℕ) (hd : 2 ≤ d) :
    ∃ f : RPoly, GeometricallyIrreducible f ∧ f.totalDegree = d ∧
      (cartesianLocus f).Infinite ∧
      (¬ ∃ c : ℂ, ∃ R : ℝ, 0 < R ∧ cartesianLocus f = Metric.sphere c R) ∧
      Nat.card (isometrySetGroup (cartesianLocus f)) = 2 * d := by sorry

Source

C. Perassi, Sharp symmetry bounds for real algebraic curves (note), Theorem 1, p. 1, https://github.com/carlok/curve-symmetry-lean/blob/d99bc17a1c397956c05d7417de50f9beed56580f/sharp_symmetry_bounds.pdf. Lean: https://github.com/carlok/curve-symmetry-lean/blob/d99bc17a1c397956c05d7417de50f9beed56580f/lean/PaperBounds.lean (C. Perassi)

Human review

Endorsed by Shuze Chen · Oct 7, 2026
Confirmed by the moderator at approval.
Endorsed by carlok · Oct 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph

Theorem 1 (sharpness of the full bound): ∣Sym(C)∣=2d|\mathrm{Sym}(C)|=2d∣Sym(C)∣=2d occurs in every degree d≥2d\ge2d≥2

Theorem 1 (sharpness of the full bound): $|\mathrm{Sym}(C)|=2d$ occurs in every degree $d\ge2$