Skip to content

Polynomial root stability

Fixed-degree stability of polynomial root-generated intermediate fields inside a common Krasner normed extension, including monic, normalized, and ordinary-coefficient versions with derived nearby separability, plus quantitative Newton lifting with convergence and resultant-controlled factorization over complete ultrametric normed fields, together with polynomial estimates for valuations in linearly ordered commutative value monoids with zero.

Quoted from the project description in formalization.yaml of FormalFrontier/polynomial-root-stability at commit efade497, Apache-2.0.

4 articles: 4 for headline results in its README whose declaration link names a declaration the scan finds in the linked file. Its other headline results are quoted where they stand.

Facts

From the repository and its formalization.yaml; the review and automation statements are quoted as written.

  • Repository: FormalFrontier/polynomial-root-stability, read at commit efade497 (2026-11-04).
  • Lean toolchain v4.34.0-rc2, Mathlib at 83abb3e7.
  • License: Apache-2.0.
  • Authors: Formal Frontier Agents.
  • Review status: “pending”.
  • Automation: agent; framework “Codex CLI”; tool setup “AI-assisted Lean proof development, mathematical examples and documentation with repository-pinned Lean and mathlib compilation.”
  • Automation notes: “Automated assistance is not a substitute for proof-term validation, mathematical review or source-correspondence review.”

Literature

The sources its formalization.yaml names, with their relationship to it.

  • Fixed-ambient-field root-generated-field stability (original-proof; other).
  • Cohomology of Number Fields, corrected second edition 2.3, Jürgen Neukirch, Alexander Schmidt, Kay Wingberg, Section 12.1.1; corrected edition 2.3, May 2020 (book; background).
  • Local Fields and Their Extensions, second edition, Ivan B. Fesenko, Sergei V. Vostokov, Chapter II, Section 1, Proposition 1.1 (p. 36), Corollary 3 (p. 37), Exercise 1 (p. 38) (book; background).

Builds on

No other Formal Frontier library.

Used by

Headline results

Quoted from the headline results in README.md of FormalFrontier/polynomial-root-stability at commit efade497, Apache-2.0.

Root-generated fields are locally constant at fixed degree. Fix normed fields K, L with a normed algebra structure L / K satisfying IsKrasner K L. For any nonzero separable polynomial f : K[X] that splits in L, there is a radius ε > 0 such that every polynomial g : K[X] with the same natDegree, also splitting in L, and with ‖g.coeff i - f.coeff i‖ < ε for every coefficient index i, is separable and generates exactly the same intermediate field over K as f. The ordinary-coefficient theorem applies without monicity and derives comparison nonzeroness internally.

There are also monic and scale-invariant normalized-coefficient versions of this result. The normalized version measures closeness after dividing each polynomial by its own leading coefficient and requires g ≠ 0 explicitly; do not interchange the normalized and ordinary coefficient bounds.

These results let downstream developments perturb coefficients while keeping the root-generated subfield fixed. The ambient extension and both splitting assumptions are inputs, not conclusions. Equality is between the subfields IntermediateField.adjoin K (f.rootSet L) and IntermediateField.adjoin K (g.rootSet L) inside that fixed L, not an equivalence of canonical splitting-field objects. Fixed degree is essential; no stability for arbitrary variable-degree families or nonseparable references is asserted. Mathlib supplies Krasner's lemma and polynomial-root continuity; this library combines them with finite-root estimates and coefficient normalization to obtain the stated local-constancy interfaces. See the historical root-field API reference and the generic checked-use clients.

TheoremPolynomial root scaling#

For a fixed polynomial p : R[X] over a topological semiring R, evaluation of Mathlib's root-scaling operation is jointly continuous by Polynomial.continuous_eval_scaleRoots: (t, z) ↦ (p.scaleRoots t).eval z. The polynomial is fixed; no continuity across changes of degree is asserted, and multiplication need not be commutative.

Over any normed field K, suppose p : K[X] satisfies ∀ w, 1 ≤ ‖w‖ → p.eval w ≠ 0. If ‖t‖ ≤ ‖z‖ and z ≠ 0, then Polynomial.scaleRoots_eval_ne_zero_of_norm_le gives (p.scaleRoots t).eval z ≠ 0. In particular this applies when ‖t‖ ≤ 1 and ‖z‖ = 1. The outside condition holds for X over every normed field and for X - C (1/2) over ℂ; it implies p ≠ 0 by evaluation at 1. At parameter zero the scaled polynomial is p.leadingCoeff • X ^ p.natDegree, so nonzero constants are included without a positive-degree hypothesis. No completeness, algebraic-closure or nontrivial-norm assumption is needed.

Quoted from the headline results in README.md of FormalFrontier/polynomial-root-stability at commit efade497, Apache-2.0.

Lean

Read from the source at commit efade497, without running Lean.

Sources
LeanPolynomial.continuous_eval_scaleRoots

TheoremPolynomial scaling in valuation balls#

Let R : Type u be a commutative ring and Γ₀ : Type w a LinearOrderedCommMonoidWithZero, with independent universes, and let v : Valuation R Γ₀. For f : R[X], M : Γ₀ and a : R, assume ∀ n > 0, v (f.coeff n) ≤ M and v a ≤ 1; the constant coefficient is unrestricted. Set D = v (f.derivative.eval a) and B = {b | M * v (b - a) < D}. Valuation.map_eval_sub_eq_of_mul_map_sub_lt_map_derivative gives v (f.eval b - f.eval a) = D * v (b - a) for b ∈ B, and Valuation.map_derivative_eval_eq_of_mul_map_sub_lt_map_derivative gives v (f.derivative.eval b) = D there. For b, c ∈ B, Valuation.map_eval_sub_eval_eq_of_mul_map_sub_lt_map_derivative gives v (f.eval c - f.eval b) = D * v (c - b). Only Valuation.injOn_eval_of_mul_map_sub_lt_map_derivative additionally assumes v.supp = ⊥ to conclude Set.InjOn on B; value-zero displacement alone need not identify points. These estimates need no root, domain, field, Henselianity, completeness, rank-one or real-valued realization, normalization, uniformizer, value-one derivative or separate 0 < M assumption. Value inverses are not required; multiplication in Γ₀ by positive elements is strict and cancellative. No arbitrary-rank root-existence theorem is asserted. The estimates reuse Mathlib's valuation, Taylor and geometric-sum APIs.

Quoted from the headline results in README.md of FormalFrontier/polynomial-root-stability at commit efade497, Apache-2.0.

Lean

Read from the source at commit efade497, without running Lean.

Sources
LeanValuation.map_eval_sub_eq_of_mul_map_sub_lt_map_derivative

Local polynomial norm scaling

Let R be an ultrametric commutative seminormed ring with multiplicative seminorm. If f : R[X] satisfies ∀ n, ‖f.coeff n‖ ≤ M, ‖a‖ ≤ 1, and M * ‖b - a‖ < ‖f.derivative.eval a‖, then

‖f.eval b - f.eval a‖ = ‖f.derivative.eval a‖ * ‖b - a‖

The theorem Polynomial.norm_eval_sub_eq_of_mul_norm_sub_lt_norm_derivative requires no root, division, completeness or separated norm. Only the anchor a is assumed to lie in the unit ball; the bound on b follows from the hypotheses. Zero seminorm distance is allowed without identifying the points. The 3-adic Newton example instantiates this identity at a = 1 and b = 5 / 2 for X² - 4, with nonzero evaluation-difference norm and displacement norm both equal to 1 / 3.

The two-point theorem Polynomial.norm_eval_sub_eval_eq_of_mul_norm_sub_lt_norm_derivative gives ‖f.eval c - f.eval b‖ = ‖f.derivative.eval a‖ * ‖c - b‖ under the same assumptions on R, f, M, and a whenever both M * ‖b - a‖ < ‖f.derivative.eval a‖ and M * ‖c - a‖ < ‖f.derivative.eval a‖; the derivative factor remains at the original anchor a.

When R is a normed commutative ring, the same coefficient and anchor bounds give injectivity on this strict ball. The theorem Polynomial.injOn_eval_of_mul_norm_sub_lt_norm_derivative expresses this as Set.InjOn; the anchor need not be a root.

Root existence and bounds under coefficient perturbation

For an ultrametric commutative seminormed ring with multiplicative seminorm, assume ∀ n, ‖f.coeff n‖ ≤ M, ‖a‖ ≤ 1, f.eval x = 0, and g.eval y = 0. If M * ‖x - a‖ < ‖f.derivative.eval a‖ and M * ‖y - a‖ < ‖f.derivative.eval a‖, and ∀ n, ‖f.coeff n - g.coeff n‖ ≤ ε, then ‖f.derivative.eval a‖ * ‖x - y‖ ≤ ε. This is a bound on two given roots. No separation or completeness is needed; ε = 0 gives zero seminorm distance, not necessarily equality of roots.

For local root existence, set D = ‖f.derivative.eval a‖. In a complete ultrametric normed commutative ring with multiplicative norm, Polynomial.exists_root_of_norm_coeff_sub_le_of_isUnit takes the coefficient and anchor bounds, the root x of f, its strict ball inequality M * ‖x - a‖ < D, the coefficient-difference bound, M * ε < D ^ 2, and a unit original derivative. It constructs a root y of g in the same original strict derivative ball with D * ‖x - y‖ ≤ ε. Every root of g in that ball equals y, whether or not a scaled distance bound was supplied for it. No root of g is an input.

Over a complete ultrametric normed field, Polynomial.exists_root_of_norm_coeff_sub_le derives the derivative unit from the strict ball inequality, so only the six coefficient, anchor, original-root, strict-ball, difference, and smallness conditions are inputs. These existential conclusions are the root-construction and characterization API, not a chosen-root object: use the witness for existence and its uniqueness clause to identify any other root in the original ball. The ring construction requires inverse data in the form of a unit original derivative; it does not assert existence over all complete ultrametric normed rings without such data.

The same ℚ_[3] model with f = X² - 4, g = X² - 25/4, a = 1, and x = -2 has M = D = 1 and positive ε = 1/9. The constructed root is y = 5/2, and D * ‖x - y‖ = 1/9, so the bound is sharp. Zero perturbation is also supported: with g = f and ε = 0, the constructed root equals x. See coefficient perturbation.

TheoremRoot uniqueness in an ultrametric normed ring#

Let R be an ultrametric normed commutative ring with multiplicative norm, let f : R[X] satisfy ∀ n, ‖f.coeff n‖ ≤ M, and let y be a root with ‖y‖ ≤ 1. Then every root x satisfying M * ‖x - y‖ < ‖f.derivative.eval y‖ equals y. The criterion Polynomial.eq_of_eval_eq_zero_of_mul_norm_sub_lt_norm_derivative requires neither division nor completeness, and does not assume ‖x‖ ≤ 1: the derivative bound and the strict inequality imply that bound. The local norm scaling identity forces ‖x - y‖ = 0, and separation gives equality. The coefficient bound is arbitrary; it need not be one.

The 3-adic Newton example for X² - 4 at 1 uses this criterion to identify every source root in the strict radius-one ball with -2. The same example retains convergence under the embedding into the 3-adic complex field and uniqueness among all target roots in the target ball; the other root 2 lies on the excluded boundary.

Quoted from the headline results in README.md of FormalFrontier/polynomial-root-stability at commit efade497, Apache-2.0.

Lean

Read from the source at commit efade497, without running Lean.

Sources
LeanPolynomial.eq_of_eval_eq_zero_of_mul_norm_sub_lt_norm_derivative

Quantitative Newton lifting

For a complete ultrametric normed field K, a polynomial f : K[X] with ∀ n, ‖f.coeff n‖ ≤ 1, and ‖a₀‖ ≤ 1, the hypothesis ‖f.eval a₀‖ < ‖f.derivative.eval a₀‖² gives an integral root at exact distance ‖f.eval a₀‖ / ‖f.derivative.eval a₀‖, with derivative-norm stability and uniqueness in the open initial-derivative-radius ball. The statement also includes convergence of the explicit iterates f.newtonMap^[n] a₀, integrality of all iterates, nonzero denominators and derivative-norm stability at every iterate. No monicity, characteristic-zero, nontrivial-norm, or norm-one derivative hypothesis is imposed. This formulation uses a real-valued norm, not an arbitrary higher-rank valuation.

The theorem Polynomial.exists_root_tendsto_iterate_newtonMap uses coefficient-controlled ultrametric estimates and Mathlib’s Banach fixed point theorem. On the closed ball of radius δ / d, where δ is the initial error and d the initial derivative norm, the Newton map has contraction constant δ / d². The proof includes zero initial error and trivially normed fields. The field-target quotient formula and boundary examples use the stock polynomial Newton map and function iteration. The independent 2-adic input calculation uses X² - 17 at 1, with nonzero error of norm 1 / 16 and derivative of norm 1 / 2, a nonunit in ℤ_[2]. Its further convergence client applies the general theorem; the input calculation is independent of the root-existence proof. The private p-adic compatibility clients recover the complete existing Hensel interface for arbitrary commutative-semiring coefficients and the p-adic polynomial distance estimate, without calling the old root-existence theorem or adding a duplicate public API. The X² - 1 boundary calculation shows that uniqueness cannot use the closed derivative-radius ball.

TheoremQuantitative resultant-controlled factorization#

Let K be a complete ultrametric normed field, and let f, g₀, h₀ : K[X]. Write m = g₀.natDegree, n = h₀.natDegree, e = f - g₀ * h₀, δ = e.supNorm and r = ‖g₀.resultant h₀‖, using the natural-degree resultant. Assume g₀.supNorm ≤ 1, h₀.supNorm ≤ 1, e.degree < (m + n : WithBot ℕ) and δ < r². Then Polynomial.exists_factorization_of_supNorm_lt_resultant_sq gives f = g * h, preserving each initial factor's degree and leading coefficient. The corrections have degrees strictly less than m and n, both factors have sup norm at most one, and both correction sup norms are at most δ / r.

There is no monicity, norm-one-leading-coefficient, characteristic-zero, discreteness, nontrivial-norm or positive-factor-degree assumption. The strict degree bounds use WithBot ℕ, so degree less than zero forces the zero polynomial. In particular, both constant initial factors force zero error, and zero error returns the initial factors. The proof uses the initial Sylvester inverse, finite coefficient coordinates and Mathlib's Banach fixed-point theorem.

The 5-adic example uses g₀ = 5X² + 2, h₀ = 5X² + 7 and f = g₀h₀ + 5⁹X. Its independently proved inputs give r = 5⁻⁴, δ = 5⁻⁹ and correction bounds 5⁻⁵. The full-output client produces degree-two factors with leading coefficients 5 and these correction bounds. The leading coefficients and resultant are nonunits in the valuation integer ring, not in the field.

Quoted from the headline results in README.md of FormalFrontier/polynomial-root-stability at commit efade497, Apache-2.0.

Lean

Read from the source at commit efade497, without running Lean.

Sources
LeanPolynomial.exists_factorization_of_supNorm_lt_resultant_sq

Main results

Its formalization.yaml lists 9 main results, and the scan finds 9 of them declared in the file the yaml gives; they are on their own page, not made articles.

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.