The Euler-constrained closed-form operator has full rank d^2-1 for irreducible bivariate equations of full outer degree in characteristic zero.

noncomputable def CCDN.eulerBivariatePair (R : Type u_1) [CommRing R] (k : ℕ) : EulerPairSpace R k →ₗ[R] Polynomial (Polynomial R) × Polynomial (Polynomial R)

The explicit Euler pair, in the nested polynomial ring used by the closed-form classification.

Equations

• CCDN.eulerBivariatePair R k = (CCDN.bivariatePolynomialEquiv R).toLinearMap.prodMap (CCDN.bivariatePolynomialEquiv R).toLinearMap ∘ₗ CCDN.eulerPairCoordinates R k

noncomputable def CCDN.eulerClosedFormOperator {R : Type u_1} [CommRing R] (k : ℕ) (f : Polynomial (Polynomial R)) : EulerPairSpace R k →ₗ[R] Polynomial (Polynomial R)

Closed-form operator on exactly d^2-1 explicit polynomial parameters.

Equations

• CCDN.eulerClosedFormOperator k f = CCDN.closedFormOperator f ∘ₗ CCDN.eulerBivariatePair R k

theorem CCDN.eulerClosedFormOperator_injective_of_constant_leading {F : Type u_1} [Field F] [CharZero F] [IsAlgClosed F] (k : ℕ) (f : Polynomial (Polynomial F)) (hf : Irreducible f) (a : F) (ha : a ≠ 0) (hl : f.leadingCoeff = Polynomial.C a) (hdeg : f.natDegree = k + 2) : Function.Injective ⇑(eulerClosedFormOperator k f)

Over an algebraically closed field of characteristic zero, the Euler closed-form operator of an irreducible f of outer degree k + 2 whose outer leading coefficient is a nonzero constant is injective. Scalar normalization changes neither the domain nor injectivity.