A simple root over the constant field lifts to a formal power series root. Newton iteration and coefficient stabilization prove existence.

theorem CCDN.exists_formal_simple_root {K : Type u_1} [Field K] (f : Polynomial (PowerSeries K)) (b : K) (hroot : Polynomial.eval b (Polynomial.map PowerSeries.constantCoeff f) = 0) (hder : Polynomial.eval b (Polynomial.map PowerSeries.constantCoeff (Polynomial.derivative f)) ≠ 0) : ∃ (g : PowerSeries K), PowerSeries.constantCoeff g = b ∧ Polynomial.eval g f = 0

Every simple root of the constant polynomial lifts to a formal root.

theorem CCDN.formal_simple_root_unique {K : Type u_1} [Field K] (f : Polynomial (PowerSeries K)) (b : K) (hder : Polynomial.eval b (Polynomial.map PowerSeries.constantCoeff (Polynomial.derivative f)) ≠ 0) {g h : PowerSeries K} (hg : PowerSeries.constantCoeff g = b) (hh : PowerSeries.constantCoeff h = b) (hfg : Polynomial.eval g f = 0) (hfh : Polynomial.eval h f = 0) : g = h

The simple formal branch is unique among roots with the chosen constant.