Exact evaluation rank when all homogeneous vanishing relations are multiples of the defining equation, and the resulting auxiliary-polynomial dichotomy.

theorem CCDN.integer_homogeneous_evaluation_rank_eq {n d M t : ℕ} (f : MvPolynomial (Fin (n + 1)) ℤ) (hf : f.IsHomogeneous d) (hf0 : f ≠ 0) (hdM : d ≤ M) (points : Fin t → Fin (n + 1) → ℤ) (hzero : ∀ (i : Fin t), (MvPolynomial.eval (points i)) f = 0) (hrel : ∀ (g : MvPolynomial (Fin (n + 1)) ℤ), g.IsHomogeneous M → (∀ (i : Fin t), (MvPolynomial.eval (points i)) g = 0) → f ∣ g) : ((evaluationMatrix (homogeneousMonomials n M) points).map Int.cast).rank + (n + (M - d)).choose (M - d) = (n + M).choose M

The no-auxiliary hypothesis over the integers forces the exact rational rank of the integer evaluation matrix.

theorem CCDN.ternary_homogeneous_dimension (M : ℕ) : 2 * (2 + M).choose M = (M + 2) * (M + 1)

Twice the dimension of ternary forms, without natural-number division.

theorem CCDN.plane_homogeneous_rank_identity {s d M : ℕ} (hdM : d ≤ M) (hr : s + (2 + (M - d)).choose (M - d) = (2 + M).choose M) : 2 * s + d ^ 2 = d * (2 * M + 3)

Closed form of the exact rank for plane projective curves.

theorem CCDN.plane_homogeneous_rank_bounds {s d M : ℕ} (hd : 0 < d) (hdM : d ≤ M) (hr : s + (2 + (M - d)).choose (M - d) = (2 + M).choose M) : 0 < s ∧ d * M ≤ 2 * s ∧ s ≤ d * (M + 1)

Elementary rank bounds sufficient to compare the plane rank with d*M.