Prove2Me

No nonzero translation maps an irreducible real locus of degree ≥2\ge2 into itself

Proved
CurveSymmetry.no_translation_symmetry

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

curve-symmetry-leaneuclidean-geometryreal-algebraic-geometry

Identify the Euclidean plane with C\mathbb C and use the complex coordinates X=zX=z, Y=zˉY=\bar z. Let P∈C[X,Y]P\in\mathbb C[X,Y] be irreducible in C[X,Y]\mathbb C[X,Y], of total degree deg⁡P≥2\deg P\ge 2, with nonempty real locus C={z∈C:P(z,zˉ)=0}C=\{z\in\mathbb C: P(z,\bar z)=0\}. Let v∈Cv\in\mathbb C be such that the translation z↦z+vz\mapsto z+v maps CC into itself: z+v∈Cz+v\in C for every z∈Cz\in C. Then

v=0.v=0.

This is the exclusion of nonzero translations in the proof of Lemma 3. In the formalization it is used to show that the orientation-preserving symmetries of CC have a common center, that CC has no glide reflection, and that every symmetry of CC acts on the equation by a sign.

Preamble
import Definitions.Def_CurveSymmetry_01_RealLoci
import Mathlib.Algebra.MvPolynomial.Nilpotent
import Mathlib.Algebra.MvPolynomial.NoZeroDivisors
import Mathlib.Algebra.Polynomial.FieldDivision
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.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.no_translation_symmetry {P : BPoly} (hP : Irreducible P)
    (hd : 2 ≤ P.totalDegree) (hne : (realLocus P).Nonempty) {v : ℂ}
    (htrans : ∀ z ∈ realLocus P, z + v ∈ realLocus P) : v = 0 := by sorry
Source
C. Perassi, Sharp symmetry bounds for real algebraic curves (note): lemma of the formalization, for proof of 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/Translation.lean (C. Perassi)

View graph