An explicit bounded integer moment form avoids any prescribed finite set of nonzero directions. No separation of pairs is needed for this step.

theorem CCDN.momentCoordinate_homogeneous (K : Type u_1) [Field K] (n k : ℕ) : (momentCoordinate K n k).IsHomogeneous 1

The moment coordinate ∑ j, k ^ j * X j is homogeneous of degree one.

theorem CCDN.filtration_recurrence_of_infinity_avoidance {K : Type u_1} {L : Type u_2} {σ : Type u_3} [Field K] [Field L] [Algebra K L] [IsAlgClosed L] [Finite σ] (I : Ideal (MvPolynomial σ K)) (l : MvPolynomial σ K) (hl : l.IsHomogeneous 1) (hzero : ∀ z ∈ MvPolynomial.zeroLocus L (leadingInfinityIdeal I ⊔ Ideal.span {l}), z = 0) : ∃ (N : ℕ), ∀ m ≥ N, filteredCoordinateSpace I (m + 1) = filteredCoordinateSpace I m ⊔ Submodule.map (LinearMap.mulLeft K ((Ideal.Quotient.mk I) l)) (filteredCoordinateSpace I m)

Avoiding infinity gives the eventual recurrence of the original coordinate filtration.