Documentation

LeanPool.CCDN.Projection.BoundedInfinityParameter

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.