Prove2Me

The lowest-degree part of aXm+bYm+XY(cXm+dYm)aX^m+bY^m+XY(cX^m+dY^m) is aXm+bYmaX^m+bY^m, and atm+bat^m+b is separable

Proved
CurveSymmetry.fourTermForm_tangent_data

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

algebraic-geometrycurve-symmetry-leaneuclidean-geometry

Let m≥1m\ge1 be an integer, let a,b∈Ca,b\in\mathbb C be nonzero and c,d∈Cc,d\in\mathbb C arbitrary, and let F(X,Y)=aXm+bYm+XY (cXm+dYm)∈C[X,Y]F(X,Y)=aX^m+bY^m+XY\,(cX^m+dY^m)\in\mathbb C[X,Y]. For n≥0n\ge0 let FnF_n be the homogeneous component of FF of degree nn.

Then:

  1. Fn=0F_n=0 for every n<mn<m;
  2. Fm=aXm+bYmF_m=aX^m+bY^m;
  3. aXm+bYm≠0aX^m+bY^m\ne0;
  4. the one-variable polynomial atm+b∈C[t]at^m+b\in\mathbb C[t] is separable, i.e. it has mm distinct roots.

In short,

Fn=0  (n<m),Fm=aXm+bYm≠0,atm+b separable.F_n=0\ \ (n<m),\qquad F_m=aX^m+bY^m\ne0,\qquad at^m+b\ \text{separable}.

So the origin is an mm-fold point of F=0F=0 whose tangent cone aXm+bYmaX^m+bY^m consists of mm distinct lines. Applied to PαP_\alpha, where (a,b)=(α,αˉ)(a,b)=(\alpha,\bar\alpha), and to its equation um+vm+uv(αˉum+αvm)u^m+v^m+uv(\bar\alpha u^m+\alpha v^m) in the coordinates u=1/Xu=1/X, v=1/Yv=1/Y, it gives the tangent cones αXm+αˉYm\alpha X^m+\bar\alpha Y^m and um+vmu^m+v^m of Lemma 4 at (0,0)(0,0) and (∞,∞)(\infty,\infty), both ordinary mm-fold points.

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

open CurveSymmetry
set_option autoImplicit false
open MvPolynomial
Formal statement
theorem CurveSymmetry.fourTermForm_tangent_data {m : ℕ} (hm : 0 < m) {a b : ℂ}
    (ha : a ≠ 0) (hb : b ≠ 0) (c d : ℂ) :
    (∀ n < m, homogeneousComponent n (fourTermForm m a b c d) = 0) ∧
      homogeneousComponent m (fourTermForm m a b c d) = binaryForm m a b ∧
      binaryForm m a b ≠ 0 ∧
      Polynomial.Separable (Polynomial.C a * Polynomial.X ^ m + Polynomial.C b) := by sorry
Source
C. Perassi, Sharp symmetry bounds for real algebraic curves (note): lemma of the formalization, for proof of Lemma 4, p. 3; Lemma 4, 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/FamilyCharts.lean (C. Perassi)

View graph