Maximal standard-monomial orthants construct algebraically independent original coordinates of cardinality equal to Hilbert dimension.

theorem CCDN.exists_hilbert_dimension_independent_coordinates {K : Type u_1} {σ : Type u_2} [Field K] [Fintype σ] [LinearOrder σ] (I : Ideal (MvPolynomial σ K)) (hI : I ≠ ⊤) : ∃ (U : Set σ), Nat.card ↑U = (filteredHilbertPolynomial I).natDegree ∧ AlgebraicIndependent K fun (i : ↑U) => (Ideal.Quotient.mk I) (MvPolynomial.X ↑i)

The independent coordinates are constructed from a maximal standard orthant, with exactly the degree of the Hilbert polynomial.