Finite-precision generation of hypersurface local quotients. Generator counts equal the layer dimensions; for plane curves each weight needs at most μ generators.

Homogeneous generators lifted from the origin-adic layers of a plane equation, with the number at every weight bounded by its multiplicity.

theorem CCDN.exists_origin_truncation_generators {K : Type u_1} [Field K] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) K) : ∃ (r : ℕ → ℕ) (g : (k : ℕ) → Fin (r k) → MvPolynomial (Fin (n + 1)) K), (∀ (k : ℕ), r k = Module.finrank K ↥(originLayer f k)) ∧ (∀ (k : ℕ) (j : Fin (r k)), (g k j).IsHomogeneous k) ∧ ∀ (N : ℕ) (u : MvPolynomial (Fin (n + 1)) K), ∃ (c : (k : Fin N) → Fin (r ↑k) → K), u - ∑ k : Fin N, ∑ j : Fin (r ↑k), c k j • g (↑k) j ∈ Ideal.span {f} ⊔ MvPolynomial.idealOfVars (Fin (n + 1)) K ^ N

In every ambient dimension, the numbers of homogeneous generators are exactly the dimensions of the origin-adic layers.

theorem CCDN.exists_plane_truncation_generators {K : Type u_1} [Field K] {μ : ℕ} (f : MvPolynomial (Fin 2) K) (hf : f ∈ MvPolynomial.idealOfVars (Fin 2) K ^ μ) (hμ : (MvPolynomial.homogeneousComponent μ) f ≠ 0) : ∃ (r : ℕ → ℕ) (g : (k : ℕ) → Fin (r k) → MvPolynomial (Fin 2) K), (∀ (k : ℕ), r k ≤ μ) ∧ (∀ (k : ℕ) (j : Fin (r k)), (g k j).IsHomogeneous k) ∧ ∀ (N : ℕ) (u : MvPolynomial (Fin 2) K), ∃ (c : (k : Fin N) → Fin (r ↑k) → K), u - ∑ k : Fin N, ∑ j : Fin (r ↑k), c k j • g (↑k) j ∈ Ideal.span {f} ⊔ MvPolynomial.idealOfVars (Fin 2) K ^ N

Finite-precision weighted generators for any plane equation of multiplicity μ.