$\operatorname{circPoly}$ is nonzero in the coplanar non-collinear case

Proved

NearEnemy.circPoly_ne_zero_of_coplanar

by mysticflounder · Sep 18, 2026 · Mathlib 0df444a (Lean v4.33.1)

circumsphere-polynomialcoplanaritynear-enemypolynomial-method

Let $a,b,c,e$ be points in EuclideanSpace ℝ ι with $a \neq b$ and $a \neq e$ , such that neither $\{a,b,c\}$ nor $\{b,c,e\}$ is collinear, and such that $e - a$ lies in the linear span of $\{b-a, c-a\}$ (i.e. the four points are coplanar through $a$ ). Then

\operatorname{circPoly}(a,b,c,e) \neq 0.

This is the planar (codimension-reduced) nonvanishing lemma for the cosphericality polynomial: even when the quadruple is confined to a plane, the two non-collinearity hypotheses keep the polynomial nonzero. It covers the coplanar case in the stratification used to show a generic projection kills all cospherical quadruples.

Preamble

import Mathlib
import Definitions.Def_NearEnemyDefs

universe u_1
open scoped RealInnerProductSpace
open scoped Classical
open MvPolynomial
variable {V : Type*} [NormedAddCommGroup V] [InnerProductSpace ℝ V]
variable {ι : Type*} [Fintype ι]
open NearEnemy

Formal statement

theorem NearEnemy.circPoly_ne_zero_of_coplanar {a b c e : EuclideanSpace ℝ ι}
    (hab : a ≠ b) (hae : a ≠ e)
    (habc : ¬ Collinear ℝ ({a, b, c} : Set (EuclideanSpace ℝ ι)))
    (hbce : ¬ Collinear ℝ ({b, c, e} : Set (EuclideanSpace ℝ ι)))
    (hdep : e - a ∈ Submodule.span ℝ ({b - a, c - a} :
      Set (EuclideanSpace ℝ ι))) :
    circPoly a b c e ≠ 0 := by sorry

Source

Prior art: Lund-Sheffer-de Zeeuw, Bisector energy and few distinct distances, SoCG 2015, LIPIcs vol. 34, 537-552, DOI 10.4230/LIPIcs.SOCG.2015.537, footnote 1 on p. 538, state that E(P) = 2n(n-1) when every pair of distinct points has a distinct perpendicular bisector, with the count of trivial quadruples that proves the floor (this footnote is not in arXiv:1411.6868v1); the asymptotic floor E(P) = Omega(n^2) is in their section 3.4. The generic planar projection that is injective, keeps general position and transports distances is Erdos-Furedi-Pach-Ruzsa, The grid revisited, Discrete Math. 111 (1993), proof of Theorem 3.1. Formalized in https://github.com/mysticflounder/lean-formalizations/blob/dd46c17a2a034d7bfa0df02e7f77834d35592864/lean/LeanFormalizations/Geometry/Euclidean/NearEnemyTheorem.lean#L1377-L1530

View graph

circPoly⁡\operatorname{circPoly}circPoly is nonzero in the coplanar non-collinear case

$\operatorname{circPoly}$ is nonzero in the coplanar non-collinear case