The real curve $\operatorname{Re}(z^d)=1$ is not a circle

Proved

CurveSymmetry.fermat_not_circle

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

curve-symmetry-leanpolynomialsreal-algebraic-geometry

Identify the Euclidean plane with $\mathbb C$ and use the complex coordinates $X=z$ , $Y=\bar z$ . Let $d\ge 1$ be an integer and let $C=\{z\in\mathbb C: z^d+\bar z^{\,d}-2=0\}=\{z\in\mathbb C: \operatorname{Re}(z^d)=1\}$ be the real locus of $X^d+Y^d-2$ . Then $C$ is not a circle:

C\ne\{z\in\mathbb C: |z-c|=R\}\qquad\text{for every }c\in\mathbb C\text{ and every real }R>0.

This verifies, for the sharpness examples $\operatorname{Re}(z^d)=1$ in the proof of Theorem 1, the hypothesis that the curve is not a circle.

Preamble

import Definitions.Def_CurveSymmetry_01_RealLoci
import Definitions.Def_CurveSymmetry_02_FamilyBasics
import Mathlib.Algebra.MvPolynomial.Nilpotent
import Mathlib.Algebra.MvPolynomial.NoZeroDivisors
import Mathlib.Algebra.Polynomial.FieldDivision
import Mathlib.Algebra.Polynomial.Reverse
import Mathlib.Analysis.Complex.Polynomial.Basic
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.fermat_not_circle {d : ℕ} (hd : 0 < d) : NotCircle (fermatPolynomial d) := by sorry

Source

C. Perassi, Sharp symmetry bounds for real algebraic curves (note): lemma of the formalization, for proof of Theorem 1, sharpness examples, p. 3, https://github.com/carlok/curve-symmetry-lean/blob/d99bc17a1c397956c05d7417de50f9beed56580f/sharp_symmetry_bounds.pdf. Lean: https://github.com/carlok/curve-symmetry-lean/blob/d99bc17a1c397956c05d7417de50f9beed56580f/lean/Sharpness.lean (C. Perassi)

View graph

The real curve Re⁡(zd)=1\operatorname{Re}(z^d)=1Re(zd)=1 is not a circle

The real curve $\operatorname{Re}(z^d)=1$ is not a circle