A formal plane parameterization with a free coordinate has exactly the curve equation as its kernel. The proof uses the section-image rank bound and arbitrarily many independent powers of the formal parameter.

theorem CCDN.exists_faithful_formal_plane_branch {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (z : Fin 2 → K) (j : Fin 2) (hz : (MvPolynomial.eval z) f = 0) (hj : (MvPolynomial.eval z) ((MvPolynomial.pderiv j) f) ≠ 0) : ∃ (ψ : MvPolynomial (Fin 2) K →ₐ[K] PowerSeries K), (∀ (h : MvPolynomial (Fin 2) K), PowerSeries.constantCoeff (ψ h) = (MvPolynomial.eval z) h) ∧ ψ (MvPolynomial.X j.rev - MvPolynomial.C (z j.rev)) = PowerSeries.X ∧ ∀ (h : MvPolynomial (Fin 2) K), ψ h = 0 ↔ f ∣ h

Every nonsingular point on an irreducible plane curve gives a faithful formal branch, with the original point as its constant evaluation.