Elementary distance polynomial from power sums
DefinitionEsgk_DistanceNewtonElementaryPolynomialalgebrageometrypolynomials
This forms the plane polynomial obtained by applying the Newton elementary-symmetric recursion to the power-sum polynomials of squared distances in a finite configuration.
Definition code
-- Extracted dependency interfaces and their necessary proofs.
import Definitions.Def_Esgk_DistanceNewtonPowerSumPolynomial
import Definitions.Def_Esgk_DistanceSquaredMissingMultiset
import Definitions.Def_Esgk_Foundation
import Definitions.Def_Esgk_NewtonElementaryFromPowerSums
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 EuclideanGeometry PachDeZeeuw.Algebraic
variable {n : ℕ}
def distanceNewtonElementaryPolynomial (p : Config n) (m : ℕ) : PlanePoly :=
newtonElementaryFromPowerSums (fun t ↦ distanceNewtonPowerSumPolynomial p t) m
end Esgk