Each row and Euler column uses at most one coefficient of the defining equation, with integer multiplier bounded by its degree.
theorem
CCDN.universalEulerMatrix_sparse
(k : ℕ)
(row : ℕ × ℕ)
(col : EulerColumns k)
:
universalEulerMatrix k row col = 0 ∨ ∃ (i : EulerLowIndex (k + 2)) (c : ℤ),
|c| ≤ ↑(k + 2) ∧ universalEulerMatrix k row col = MvPolynomial.C c * MvPolynomial.X i
An entry is zero or a single coefficient variable with multiplier of absolute value at most the defining equation's degree.