Prove2Me

Theorem 1 (sharpness of the rotation bound): ∣Sym+(C)∣=max⁡{d,2d−4}|\mathrm{Sym}^+(C)|=\max\{d,2d-4\} occurs in every degree d≥2d\ge2

Proved
CurveSymmetry.paper_rotation_sharp

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

algebraic-geometrycurve-symmetry-leaneuclidean-geometry

Let d≥2d\ge2 be an integer. For f∈R[x,y]f\in\mathbb R[x,y] let C={z∈C:f(Re⁡z,Im⁡z)=0}C=\{z\in\mathbb C: f(\operatorname{Re}z,\operatorname{Im}z)=0\} be its real zero set, identifying (x,y)(x,y) with x+iyx+iy, and let Sym+(C)\mathrm{Sym}^+(C) be the group of orientation-preserving Euclidean isometries z↦az+bz\mapsto az+b, ∣a∣=1|a|=1, mapping CC onto itself.

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

  1. ff is irreducible in C[x,y]\mathbb C[x,y];
  2. ff has total degree dd;
  3. CC is infinite;
  4. CC is not a circle: there are no c∈Cc\in\mathbb C and real R>0R>0 with C={z:∣z−c∣=R}C=\{z:|z-c|=R\};
  5. the rotation bound of Theorem 1 is attained:
∣Sym+(C)∣=max⁡{d, 2d−4}.|\mathrm{Sym}^+(C)|=\max\{d,\,2d-4\}.

This is the sharpness of the bound N≤max⁡{d,2d−4}N\le\max\{d,2d-4\} 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_rotation_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 (directIsometryGroup (cartesianLocus f)) = max d (2 * d - 4) := 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