Prove2Me

Lemma 3 in complex coordinates: isometries preserving {P(z,zˉ)=0}\{P(z,\bar z)=0\} multiply P(z,zˉ)P(z,\bar z) by ±1\pm1

Proved
CurveSymmetry.isometry_sign_of_realLocus

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

algebraic-geometrycurve-symmetry-leanfunction-fields

Let P∈C[X,Y]P\in\mathbb{C}[X,Y] be irreducible, of total degree at least 22, and let

S={z∈C:P(z,zˉ)=0}S=\{z\in\mathbb{C} : P(z,\bar z)=0\}

be its real locus, written in the coordinates X=zX=z, Y=zˉY=\bar z. Assume SS is infinite. Let TT be an isometry of the Euclidean plane C\mathbb{C} preserving SS, that is, T(z)∈S  ⟺  z∈ST(z)\in S\iff z\in S for every z∈Cz\in\mathbb{C}.

Then there is a sign ε∈{1,−1}\varepsilon\in\{1,-1\} such that

P(T(z),T(z)‾)=ε P(z,zˉ)for every z∈C,P\bigl(T(z),\overline{T(z)}\bigr)=\varepsilon\,P(z,\bar z)\qquad\text{for every } z\in\mathbb{C},

and ε=1\varepsilon=1 whenever TT reverses orientation, that is, whenever there are a,b∈Ca,b\in\mathbb{C} with T(z)=azˉ+bT(z)=a\bar z+b for all zz.

This is the sign clause of Lemma 3 of the note in the coordinates X=zX=z, Y=zˉY=\bar z introduced after it, where a real equation ff becomes P(X,Y)=f((X+Y)/2,(X−Y)/(2i))P(X,Y)=f\bigl((X+Y)/2,(X-Y)/(2i)\bigr); Lemma 3 itself, for a real Cartesian equation, is derived from it. The note's standing assumption that the curve is not a circle is not needed.

Formalization Note: TT ranges over the subgroup of the isometries ℂ ≃ᵢ ℂ preserving SS, ε\varepsilon is a complex number equal to 11 or −1-1, and no condition is imposed on the coefficients of PP.

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.Isometry
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
open MvPolynomial
Formal statement
theorem CurveSymmetry.isometry_sign_of_realLocus {P : BPoly} (hP : Irreducible P)
    (hd : 2 ≤ P.totalDegree) (hinf : (realLocus P).Infinite)
    (T : isometrySymmetryGroup P) :
    ∃ ε : ℂ, (ε = 1 ∨ ε = -1) ∧
      (∀ z : ℂ, eval (fun i : Fin 2 => if i = 0 then T.val z else star (T.val z)) P =
        ε * eval (fun i : Fin 2 => if i = 0 then z else star z) P) ∧
      ((∃ a b : ℂ, ∀ z : ℂ, T.val z = a * star z + b) → ε = 1) := by sorry
Source
C. Perassi, Sharp symmetry bounds for real algebraic curves (note): lemma of the formalization, for proof of Lemma 3, p. 2; Lemma 3, p. 2, https://github.com/carlok/curve-symmetry-lean/blob/d99bc17a1c397956c05d7417de50f9beed56580f/sharp_symmetry_bounds.pdf. Lean: https://github.com/carlok/curve-symmetry-lean/blob/d99bc17a1c397956c05d7417de50f9beed56580f/lean/IsometrySign.lean (C. Perassi)

View graph