The explicit Euler parameters exhaust all polynomial pairs satisfying the degree and Euler-contraction constraints.

theorem CCDN.exists_eulerBivariatePair {F : Type u_1} [Field F] (k : ℕ) (p q : Polynomial (Polynomial F)) (hp : bivariateTotalDegree p ≤ k + 1) (hq : bivariateTotalDegree q ≤ k + 1) (he : bivariateTotalDegree ((bivariateEulerContraction F) (p, q)) ≤ k + 1) : ∃ (u : EulerPairSpace F k), (eulerBivariatePair F k) u = (p, q)

Every pair of bivariate polynomials of total degree at most k + 1 whose radial contraction also has total degree at most k + 1 comes from an element of EulerPairSpace F k.