Finite normalized charts give a bounded integral moment parameter avoiding every nonzero infinity direction.
theorem
CCDN.exists_bounded_infinity_parameter
{K : Type u_1}
{L : Type u_2}
[Field K]
[Field L]
[Algebra K L]
[CharZero L]
{n : ℕ}
(I : Ideal (MvPolynomial (Fin n) K))
(d : ℕ)
(hdegree : HasFilteredCurveDegree I d)
:
∃ k ≤ n ^ 2 * d, ∀ z ∈ MvPolynomial.zeroLocus L (leadingInfinityIdeal I ⊔ Ideal.span {momentCoordinate K n k}), z = 0
The first coordinate can be chosen with an explicit bound n²*d on its integer moment parameter. The overlap between normalized charts is harmless.