Maximal circularity predicate for a plane polynomial
DefinitionEsgk_DistanceNewtonFactorSaturationalgebraic-geometrycomplex-analysispolynomials
This predicate requires the two local orders at the complex circular points to equal half of the polynomial's total degree.
Definition code
-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_Esgk_PlaneCircularLocalOrderDegree
import Definitions.Def_LeanFormalizations_PachDeZeeuw_AlgebraicPrelim
import Mathlib
/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Adam McKenna
-/
noncomputable section
namespace Esgk
open PachDeZeeuw.Algebraic
def IsMaximallyCircular (G : PlanePoly) : Prop :=
2 * planeCircularLocalOrderI G = G.totalDegree ∧
2 * planeCircularLocalOrderJ G = G.totalDegree
variable {n : ℕ}
end Esgk