The Euler constraint removes the gradient kernel from the bivariate closed-form criterion. This supplies the injective operator needed for Noether minors of degree d^2-1.

noncomputable def CCDN.bivariateEulerContraction (R : Type u_1) [CommRing R] : Polynomial (Polynomial R) × Polynomial (Polynomial R) →ₗ[R] Polynomial (Polynomial R)

Contraction with the radial vector field; the outer variable is x.

Equations

• One or more equations did not get rendered due to their size.

theorem CCDN.bivariate_euler_closed_form_eq_zero {F : Type u_1} [Field F] [CharZero F] [IsAlgClosed F] (f p q : Polynomial (Polynomial F)) (hf : Irreducible f) (hm : f.Monic) (hd : 0 < f.natDegree) (hpdeg : p.degree < f.degree) (hqdeg : q.degree < f.degree) (hclosed : (closedFormOperator f) (p, q) = 0) (heuler : ((bivariateEulerContraction F) (p, q)).coeff f.natDegree = 0) : p = 0 ∧ q = 0

The closed form is zero once its radial contraction has no top outer coefficient. The positive characteristic-zero degree makes Euler's factor nonzero.