Explicit closed forms from polynomial factors, including repeated factors. These supply reducibility obstructions for the differential matrix.

theorem CCDN.derivative_bivariateCoefficientDerivative {F : Type u_1} [Field F] (p : Polynomial (Polynomial F)) : Polynomial.derivative ((bivariateCoefficientDerivative F) p) = (bivariateCoefficientDerivative F) (Polynomial.derivative p)

The inner and outer derivatives of a bivariate polynomial commute.

theorem CCDN.bivariate_factor_closed_form {F : Type u_1} [Field F] (g h : Polynomial (Polynomial F)) : (bivariateCoefficientDerivative F) (h * Polynomial.derivative g) * (g * h) - h * Polynomial.derivative g * (bivariateCoefficientDerivative F) (g * h) = Polynomial.derivative (h * (bivariateCoefficientDerivative F) g) * (g * h) - h * (bivariateCoefficientDerivative F) g * Polynomial.derivative (g * h)

The logarithmic differential of a factor gives a closed form for the whole product after clearing its denominator.

theorem CCDN.factor_numerator_not_scalar_gradient {R : Type u_1} [CommRing R] [IsDomain R] (g h : Polynomial R) (hg : 0 < g.degree) (hgh : IsCoprime g h) (hgg : IsCoprime g (Polynomial.derivative g)) (hh : Polynomial.derivative h ≠ 0) (a : R) : h * Polynomial.derivative g ≠ Polynomial.C a * Polynomial.derivative (g * h)

For coprime factors with a separable first factor and nonzero second derivative, the factor's logarithmic numerator cannot be a scalar multiple of the derivative of the product. This works in any characteristic.

theorem CCDN.bivariate_power_factor_closed_form {F : Type u_1} [Field F] (g h : Polynomial (Polynomial F)) (k : ℕ) : (bivariateCoefficientDerivative F) (g ^ k * h * Polynomial.derivative g) * (g ^ (k + 2) * h) - g ^ k * h * Polynomial.derivative g * (bivariateCoefficientDerivative F) (g ^ (k + 2) * h) = Polynomial.derivative (g ^ k * h * (bivariateCoefficientDerivative F) g) * (g ^ (k + 2) * h) - g ^ k * h * (bivariateCoefficientDerivative F) g * Polynomial.derivative (g ^ (k + 2) * h)

The repeated-factor construction works for every multiplicity at least two, with no restriction on the characteristic or the multiplicity.

theorem CCDN.power_factor_numerator_not_scalar_gradient {R : Type u_1} [CommRing R] [IsDomain R] (g h : Polynomial R) (k : ℕ) (hg : 0 < g.degree) (hgh : IsCoprime g h) (hgg : IsCoprime g (Polynomial.derivative g)) (a : R) : g ^ k * h * Polynomial.derivative g ≠ Polynomial.C a * Polynomial.derivative (g ^ (k + 2) * h)

For a nonconstant separable g coprime to h, the numerator g ^ k * h * g' is not a scalar multiple of the derivative of g ^ (k + 2) * h; cancellation exposes its extra pole.