Separating prime components makes their filtered dimensions additive up to a fixed degree shift.

theorem CCDN.minimalPrimeComponents_filtered_rank_lower {K : Type u_1} {σ : Type u_2} [Field K] [Finite σ] (I : Ideal (MvPolynomial σ K)) : ∃ (D : ℕ), ∀ (N : ℕ), ∑ P : ↥(minimalPrimeComponents I), Module.finrank K ↥(filteredCoordinateSpace (↑P) N) ≤ Module.finrank K ↥(filteredCoordinateSpace I (D + N))

The dimension comparison for the canonical finite set of minimal primes, with constructed separators.