The finite linear system producing Frobenius auxiliary coefficients. A strict dimension inequality gives a nontrivial solution.

theorem CCDN.exists_planeFrobenius_coefficients {K : Type u_1} {ι : Type u_2} {κ : Type u_3} [Field K] [Fintype ι] [Fintype κ] (f : MvPolynomial (Fin 2) K) (j : Fin 2) (h : ι → MvPolynomial (Fin 2) K) (b : κ → MvPolynomial (Fin 2) K) {D A N : ℕ} (hd : ∀ (i : ι), (h i).totalDegree ≤ D) (hb : ∀ (k : κ), (b k).totalDegree ≤ A) (hbi : LinearIndependent K fun (k : κ) => (Ideal.Quotient.mkₐ K (Ideal.span {f})) (b k)) (hdim : ∑ r : Fin N, Module.finrank K ↥(filteredCoordinateSpace (Ideal.span {f}) (D + A + ↑r * f.totalDegree)) < Fintype.card ι * Fintype.card κ) : ∃ (a : ι → MvPolynomial (Fin 2) K), (∀ (i : ι), (a i).totalDegree ≤ A) ∧ (∃ (i : ι), ¬f ∣ a i) ∧ ∀ r < N, f ∣ ∑ i : ι, (⇑(planeTangent f j))^[r] (h i) * a i

Independent bounded-degree coefficient classes and more unknowns than constraints yield bounded-degree auxiliary coefficients.