The polynomials vanishing at a point of a circle with a transcendental coordinate

Proved

Transcendence.circle_vanishing_ideal

by carlok · Sep 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

commutative-algebradiaz-modulus-leantranscendence

Let $K$ be a subfield of $\mathbb{C}$ and $\rho \in K$ non-zero. Let $(x, y) \in \mathbb{C}^{2}$ lie on the circle $x^{2} + y^{2} = \rho$ , with $y$ transcendental over $K$ . Then for every $P \in K[X_0, X_1]$ ,

P(x, y) = 0 \iff X_0^{2} + X_1^{2} - \rho \ \text{divides}\ P.

So every plane curve defined over $K$ that passes through $(x, y)$ contains the whole circle.

Preamble

import Mathlib

Formal statement

namespace Transcendence

theorem circle_vanishing_ideal {K : Subfield ℂ} {x y : ℂ} {ρ : K} (hρ : ρ ≠ 0)
    (hxy : x ^ 2 + y ^ 2 = (ρ : ℂ)) (hy : Transcendental K y) (P : MvPolynomial (Fin 2) K) :
    MvPolynomial.aeval ![x, y] P = 0 ↔
      (MvPolynomial.X 0 ^ 2 + MvPolynomial.X 1 ^ 2 - MvPolynomial.C ρ) ∣ P := by
  sorry

end Transcendence

Source

Standard. Formal proof: Diaz modulus mission, 25 September 2026 (C. Perassi); extracted from the proof of DiazModulus.candidate_vanishing_ideal, which is the case K = Q̄, (x, y) = (Re u, Im u).

View graph