Prove2Me

For ∣α∣=1|\alpha|=1, the map z↦czz\mapsto cz sends C^m,α\widehat C_{m,\alpha} into itself if and only if c2m=1c^{2m}=1

Proved
CurveSymmetry.family_sphere_dilation_filter

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

algebraic-geometrycurve-symmetry-leanzariski-topology

Let m≥1m\ge1 be an integer, let α∈C\alpha\in\mathbb C with ∣α∣=1|\alpha|=1 and α∉R\alpha\notin\mathbb R, and let c∈Cc\in\mathbb C with c≠0c\ne0. Let Cm,α={z∈C:Re⁡(zm(∣z∣2+α))=0}C_{m,\alpha}=\{z\in\mathbb C:\operatorname{Re}(z^m(|z|^2+\alpha))=0\}, let C^m,α\widehat C_{m,\alpha} be its closure in the Riemann sphere C^=C∪{∞}\widehat{\mathbb C}=\mathbb C\cup\{\infty\}, and let Dc ⁣:C^→C^D_c\colon\widehat{\mathbb C}\to\widehat{\mathbb C} be the dilation Dc(z)=czD_c(z)=cz for z∈Cz\in\mathbb C, Dc(∞)=∞D_c(\infty)=\infty. Then

Dc(C^m,α)⊆C^m,α  ⟺  c2m=1.D_c(\widehat C_{m,\alpha})\subseteq\widehat C_{m,\alpha}\iff c^{2m}=1.

This is the dilation half of the description (3) of the ambient Möbius symmetries of C^m,α\widehat C_{m,\alpha} in Theorem 2, tested on the whole sphere, ∞\infty included. It is also used for Remark 5.

Formalization Note: the Riemann sphere is the one-point compactification OnePoint ℂ, C^m,α\widehat C_{m,\alpha} is the topological closure in it, and DcD_c is defined pointwise on the sphere.

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.MvPolynomial.PDeriv
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.FieldTheory.Separable
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
import Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

open CurveSymmetry
set_option autoImplicit false
open MvPolynomial OnePoint
Formal statement
theorem CurveSymmetry.family_sphere_dilation_filter {m : ℕ} (hm : 0 < m) {α c : ℂ}
    (ha : α ≠ star α) (hα : ‖α‖ = 1) (hc : c ≠ 0) :
    (∀ p ∈ sphericalFamily m α, sphereDilation c p ∈ sphericalFamily m α) ↔
      c ^ (2 * m) = 1 := by sorry
Source
C. Perassi, Sharp symmetry bounds for real algebraic curves (note): lemma of the formalization, for Theorem 2, 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/FamilySphereDilation.lean (C. Perassi)

View graph