Pair separation for two samples on a maximally circular curve

Proved

Esgk.maximallyCircular_twoSamplePairSeparation

by mysticflounder · Oct 16, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsgeometry

Let $G$ be an irreducible real plane polynomial of degree $d$ , with real zero set $C$ . Assume that $G$ is not a circle factor and is maximally circular: its local order at each of the two complex circular points at infinity is $d/2$ .

For any two finite samples $S_1,S_2\subset C$ , there are exceptional sets $\Delta_i\subset S_i\times S_i$ , for $i=1,2$ , satisfying

|\Delta_i|\le 8d^2|S_i|.

Within each sample, any two distinct retained pairs $(a,b),(a',b')\in(S_i\times S_i)\setminus\Delta_i$ have a finite common distance locus

\bigl\{(x,y)\in C\times C: \|x-a\|^2=\|y-b\|^2,\quad \|x-a'\|^2=\|y-b'\|^2\bigr\}.

The two conclusions hold simultaneously and separately within the two samples. The samples may be empty or overlap. No assertion is made about a pair from one sample compared with a pair from the other.

Preamble

import Definitions.Def_Esgk_DistanceNewtonFactorSaturation
import Definitions.Def_Esgk_IrreduciblePlaneDistanceImageInfiniteCorrespondence
import Definitions.Def_Esgk_IrreduciblePlaneFunctionField
import Definitions.Def_Esgk_PlaneCircleFactor
import Definitions.Def_LeanFormalizations_PachDeZeeuw_AlgebraicPrelim

open Esgk
open PachDeZeeuw.Algebraic (PlanePoly PlaneCurveZeroSet)
open IrreduciblePlanePolynomial

Formal statement

theorem Esgk.maximallyCircular_twoSamplePairSeparation
    {G : PlanePoly} (hGirreducible : Irreducible G)
    (hmax : IsMaximallyCircular G) (hnotCircle : ¬ IsCircleFactor G)
    (S₁ S₂ : Finset PachDeZeeuw.Algebraic.Point2)
    (hS₁ : (S₁ : Set PachDeZeeuw.Algebraic.Point2) ⊆ PlaneCurveZeroSet G)
    (hS₂ : (S₂ : Set PachDeZeeuw.Algebraic.Point2) ⊆ PlaneCurveZeroSet G) :
    ∃ (Δ₁ : Finset (S₁ × S₁)) (Δ₂ : Finset (S₂ × S₂)),
      Δ₁.card ≤ 8 * G.totalDegree ^ 2 * S₁.card ∧
      Δ₂.card ≤ 8 * G.totalDegree ^ 2 * S₂.card ∧
      (∀ ij, ij ∉ Δ₁ → ∀ kl, kl ∉ Δ₁ → ij ≠ kl →
        (twoPairDistanceCommonZeroSet
          ⟨G, hGirreducible⟩
          (ij.1 : PachDeZeeuw.Algebraic.Point2) (kl.1 : PachDeZeeuw.Algebraic.Point2)
          (ij.2 : PachDeZeeuw.Algebraic.Point2) (kl.2 : PachDeZeeuw.Algebraic.Point2)).Finite) ∧
      (∀ ij, ij ∉ Δ₂ → ∀ kl, kl ∉ Δ₂ → ij ≠ kl →
        (twoPairDistanceCommonZeroSet
          ⟨G, hGirreducible⟩
          (ij.1 : PachDeZeeuw.Algebraic.Point2) (kl.1 : PachDeZeeuw.Algebraic.Point2)
          (ij.2 : PachDeZeeuw.Algebraic.Point2) (kl.2 : PachDeZeeuw.Algebraic.Point2)).Finite) := by sorry

View graph