A local Bézout bound on formal vanishing orders. It gives injective jets on low-degree functions and verifies the jet condition in Frobenius noncancellation for irreducible plane curves.

theorem CCDN.powerSeries_quotient_powers_independent {K : Type u_1} [Field K] (g : PowerSeries K) (N : ℕ) (hvan : PowerSeries.X ^ N ∣ g) : LinearIndependent K fun (i : Fin N) => (Ideal.Quotient.mkₐ K (Ideal.span {g})) (PowerSeries.X ^ ↑i)

If X ^ N divides the power series g, then the images of 1, X, …, X ^ (N - 1) in the quotient by g are linearly independent.

theorem CCDN.formal_plane_vanishing_order_bound {K : Type u_1} [Field K] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (ψ : MvPolynomial (Fin 2) K →ₐ[K] PowerSeries K) (hψ : ψ f = 0) (j : Fin 2) (a : K) (hparam : ψ (MvPolynomial.X j - MvPolynomial.C a) = PowerSeries.X) (g : MvPolynomial (Fin 2) K) (hnd : ¬f ∣ g) {N : ℕ} (hvan : PowerSeries.X ^ N ∣ ψ g) : N ≤ f.totalDegree * g.totalDegree

If a proper degree-m section vanishes to order N on a formal plane branch, then N<=d*m. The parameter map and its equation are maps.

theorem CCDN.formal_plane_frobenius_relation_trivial {K : Type u_1} {ι : Type u_2} [Field K] [Fintype ι] (p r : ℕ) [Fact (Nat.Prime p)] [CharP K p] (f : MvPolynomial (Fin 2) K) (hf : Irreducible f) (ψ : MvPolynomial (Fin 2) K →ₐ[K] PowerSeries K) (hψ : ψ f = 0) (j : Fin 2) (a : K) (hparam : ψ (MvPolynomial.X j - MvPolynomial.C a) = PowerSeries.X) {D : ℕ} (hD : f.totalDegree * D < p ^ r) (h : ι → MvPolynomial (Fin 2) K) (hd : ∀ (i : ι), (h i).totalDegree ≤ D) (hi : LinearIndependent K fun (i : ι) => (Ideal.Quotient.mkₐ K (Ideal.span {f})) (h i)) (g : ι → PowerSeries K) (hrel : ∑ i : ι, ψ (h i) * g i ^ p ^ r = 0) (i : ι) : g i = 0

Frobenius coefficients cannot cancel a low-degree basis on a formal plane branch. The numerical condition is d*D<p^r.