Symmetries of real plane curves

How many Euclidean symmetries can a real plane algebraic curve of degree $d$ have? Rotational symmetry of a curve is classically detected from the monomials $z^a\bar z^{\,b}$ of its equation in the complex coordinate $z=x+iy$: a rotation of order $N$ about the origin can preserve the curve only if the differences $a-b$ of the nonzero monomials satisfy a congruence modulo $N$ (Lebmeir and Richter-Gebert, Section 4; Lebmeir, Theorem 5.4). Bounds on the number of symmetries in terms of the degree enter symmetry detection algorithms (Alcázar, Lávička and Vršek) and incidence geometry: Pach and de Zeeuw, Lemma 2.6 use a bound of $4d$ on the number of isometries of a curve in a distinct-distances argument.

The note Sharp symmetry bounds for real algebraic curves (C. Perassi, 2026; PDF) determines the sharp bounds, classifies the curves attaining the rotation bound in degree $d\ge5$, and describes their Möbius geometry. This mission is the complete Lean formalization of that note.

Setting

Let $f\in\mathbb R[x,y]$ be irreducible in $\mathbb C[x,y]$, of total degree $d\ge2$, and let $C=\{(x,y)\in\mathbb R^2 : f(x,y)=0\}$, identified with a subset of $\mathbb C$ through $z=x+iy$. Assume that $C$ is infinite and is not a circle. Write $\operatorname{Sym}(C)$ for the group of Euclidean isometries $T$ of $\mathbb C$ with $T(C)=C$, and $\operatorname{Sym}^+(C)$ for its orientation-preserving subgroup (the rotations and translations preserving $C$).

For an integer $m\ge1$ and a nonreal $\alpha\in\mathbb C$ with $|\alpha|=1$, the extremal family is

$$C_{m,\alpha}=\{z\in\mathbb C : \operatorname{Re}\bigl(z^m(|z|^2+\alpha)\bigr)=0\},$$

a curve of degree $m+2$. Its closure $\widehat C_{m,\alpha}$ in the Riemann sphere $\widehat{\mathbb C}=\mathbb C\cup\{\infty\}$ is acted on by Möbius maps $z\mapsto (az+b)/(cz+d)$ and by anti-Möbius maps, a Möbius map composed with complex conjugation. In the coordinates $X=z$, $Y=\bar z$ the family has the equation $P_\alpha=X^m(\alpha+XY)+Y^m(\bar\alpha+XY)$, whose zero set $V_\alpha\subset\mathbb P^1\times\mathbb P^1$ has bidegree $(m+1,m+1)$.

Formalization targets

Goal: the bounds (Theorem 1)

$$\operatorname{Sym}(C)\ \text{and}\ \operatorname{Sym}^+(C)\ \text{are finite},\qquad |\operatorname{Sym}^+(C)|\le\max\{d,\,2d-4\},\qquad |\operatorname{Sym}(C)|\le 2d .$$

The goal asserts the bounds only; their sharpness and the equality case are milestones.

Milestones

1. Theorem 1, sharpness and equality. Both bounds are attained in every degree $d\ge2$. If $d\ge5$ and $|\operatorname{Sym}^+(C)|=2d-4$, an orientation-preserving similarity carries $C$ onto $C_{d-2,\alpha}$; conversely every $C_{m,\alpha}$ with $m\ge3$ has $2m$ rotations.
2. Equation (2). The quintic $\operatorname{Re}\bigl(z^3(|z|^2+i)\bigr)=0$ satisfies $f(e^{\pi i/3}z)=-f(z)$ and has exactly six rotations: a symmetry of a zero set need not fix its defining polynomial.
3. Lemma 3. Every $T\in\operatorname{Sym}(C)$ satisfies $f\circ T=\pm f$, with sign $+1$ for reflections.
4. Theorem 2. $C_{m,\alpha}$ ($m\ge2$) is infinite, geometrically irreducible, of degree $m+2$; the full ambient Möbius symmetry group of $\widehat C_{m,\alpha}$ is $\{z\mapsto cz : c^{2m}=1\}\cup\{z\mapsto c/z : c^{2m}=\bar\alpha^{\,2}\}$, dihedral of order $4m$, with no anti-Möbius symmetry; the Euclidean symmetries are the $2m$ rotations; and for fixed $m$, $\widehat C_{m,\alpha}$ and $\widehat C_{m,\beta}$ are Möbius equivalent if and only if $\beta=\alpha$, anti-Möbius equivalent if and only if $\beta=\bar\alpha$.
5. Lemma 4. $P_\alpha$ is irreducible (and so is $V_\alpha$), the only singular points of $V_\alpha$ are $(0,0)$ and $(\infty,\infty)$, both ordinary $m$-fold points, and its function field has genus $m$.
6. Remark 5. In degree four, $\operatorname{Re}(z^4)=1$ attains the rotation bound but is not similar to any $C_{2,\alpha}$: its function field has genus three, those of the family genus two. The parameters $e^{i\theta}$, $0<\theta<\pi$, give pairwise inequivalent curves, and for algebraic $\alpha$ all the maps in Theorem 2 have algebraic coefficients.

Significance

The result. The bounds $\max\{d,2d-4\}$ and $2d$ are attained in every degree, so they cannot be improved as functions of $d$ alone; for $d\ge5$ the curves attaining the rotation bound form one explicit family up to similarity, with a complete invariant. The bound $2d$ sharpens the auxiliary $4d$ estimate used by Pach and de Zeeuw (no improvement of their distance exponent is claimed), and the quintic of equation (2) contradicts the degree restriction stated in Lemma 9 of the arXiv version of Alcázar, Lávička and Vršek (the journal version has not been checked).

The formalization. Every statement of the note is proved in Lean 4 with Mathlib: 208 theorems and 12 definition files here, all proved, using only the axioms propext, Classical.choice and Quot.sound. It contains material that Mathlib does not have yet and that is reusable on its own: the genus of a function field over $\mathbb C$ defined through its places and holomorphic differentials, and its invariance under isomorphism; the places of quadratic covers $w^2=h(t)$ and Kummer covers $y^n=f(x)$, with uniformizers and local Kähler differentials; the classification of places of a Dedekind domain; the four-chart atlas of $\mathbb P^1\times\mathbb P^1$ with its Zariski topology; and Möbius and anti-Möbius maps acting on the Riemann sphere. Theorem 1 is also registered with the Palomar registry as PALOMAR-2026-09-18-000007. The Lean code was written by AI agents under the author's direction; the Lean kernel checks it. The results have not been reviewed by an independent human, and neither the kernel checks nor the registration certify novelty.

Difficulty

The first argument is Bézout: the images of a point of $C$ under the rotations about a common center are distinct points on one circle, so there are at most $2d$ of them. This gives $2d$ for $\operatorname{Sym}^+(C)$, not $\max\{d,2d-4\}$, and it says nothing about which curves are extremal. A second obstacle is that a symmetry of the zero set need only fix the polynomial up to sign, as equation (2) shows, so invariant-theoretic arguments that assume $f\circ T=f$ do not apply directly. For the Möbius statements the difficulty is that a Möbius map of the sphere does not act on the real equation; the curve must be compactified and its singular points identified. In the formalization, the genus comparison of Remark 5 needs a genus that does not depend on a chosen model, which Mathlib does not provide.

Formalization scope

• Curves are given by real polynomials in two variables (MvPolynomial (Fin 2) ℝ), and the curve is their real zero set as a subset of $\mathbb C$. Geometric irreducibility means irreducibility over $\mathbb C$.
• Symmetry groups are the actual groups of isometries ℂ ≃ᵢ ℂ preserving that subset. Group orders use Nat.card, which is $0$ for an infinite set, so finiteness is part of the statements.
• Several family statements need less than the note: $\alpha\notin\mathbb R$ without $|\alpha|=1$, or $m\ge1$; the statements say so.
• The Riemann sphere is OnePoint ℂ with the action of $\mathrm{GL}_2(\mathbb C)$.
• $V_\alpha$ is the bihomogeneous zero locus in $\mathbb P^1\times\mathbb P^1$, with the topology making the four standard affine Zariski charts open embeddings. These are classical complex points, not schemes.
• The genus is the dimension of the space of differentials of the function field that are regular at every place, a place being a proper valuation subring containing $\mathbb C$. A branch point is a point of the $t$-line with fewer than two places above it. Ramification indices and a divisor-level Riemann–Hurwitz formula are not formalized; the genus of Lemma 4 comes from an explicit basis of differentials.
• The hypotheses rule out trivial versions: the curve is infinite, irreducible over $\mathbb C$ and not a circle, and the groups are those of the zero set, not of the polynomial.
• Welcome contributions: moving the reusable parts into Mathlib, a divisor-level Riemann–Hurwitz statement, and a scheme-theoretic normalization of $V_\alpha$.

Selected references

• C. Perassi, Sharp symmetry bounds for real algebraic curves, note, 2026. PDF; Lean formalization: github.com/carlok/curve-symmetry-lean.
• P. Lebmeir and J. Richter-Gebert, Rotations, translations and symmetry detection for complexified curves, Computer Aided Geometric Design 25 (2008), 707–719. doi:10.1016/j.cagd.2008.09.004
• P. M. Lebmeir, Feature Detection for Real Plane Algebraic Curves, doctoral thesis, TU München, 2009. PDF
• J. Pach and F. de Zeeuw, Distinct distances on algebraic curves in the plane, 2014. arXiv:1308.0177v3
• J. G. Alcázar, M. Lávička and J. Vršek, Symmetries and similarities of planar algebraic curves using harmonic polynomials, 2018. arXiv:1801.09962v1; Journal of Computational and Applied Mathematics 357 (2019), 302–318, doi:10.1016/j.cam.2019.02.036.
• L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language, CADE 28, LNCS 12699, Springer, 2021, 625–635. doi:10.1007/978-3-030-79876-5_37
• The mathlib Community, The Lean mathematical library, CPP 2020, 367–381. doi:10.1145/3372885.3373824