The printed coefficient-sum bound for the ambient Noether forms. Coefficient extraction from plane parameters costs no additional factor.

The sharp printed coefficient-sum bound for the plane Noether minors: each entry has l1 norm at most d, hence the order d²−1 determinant has l1 norm at most d^(3d²−3).

theorem CCDN.ambientNoetherForm_coefficientL1_le (σ : Type u_1) [Fintype σ] [DecidableEq σ] (k : ℕ) (rows : Fin ((k + 2) ^ 2 - 1) → ℕ × ℕ) (cols : Fin ((k + 2) ^ 2 - 1) → EulerColumns k) (m : PlaneParameters σ →₀ ℕ) : (ambientNoetherForm σ k rows cols m).l1Norm ≤ (k + 2) ^ (3 * (k + 2) ^ 2 - 3) * (Fintype.card (Sym σ (k + 2)) * 3 ^ (k + 2)) ^ ((k + 2) ^ 2 - 1)

The exact coefficient-sum bound, in terms of the number of original degree-d homogeneous monomials.