Archimedean determinant bounds retaining each monomial's own degree. Their exponent is the sum of column degrees, not rank times the cutoff.

theorem CCDN.weighted_evaluation_det_log_bound {n s : ℕ} (mon : Fin s → Fin n →₀ ℕ) (z : Fin s → Fin n → ℤ) {B : ℝ} (hB : 1 ≤ B) (hz : ∀ (i : Fin s), InBox (z i) B) (hne : (evaluationMatrix mon z).det ≠ 0) : Real.log |↑(evaluationMatrix mon z).det| ≤ Real.log ↑s.factorial + (∑ j : Fin s, ↑(Finsupp.degree (mon j))) * Real.log B

A nonzero integer determinant has the sharp sum-of-degrees logarithmic upper bound.