A low-degree algebraic relation detects differential constants. If t'=1, no nonzero polynomial in t of degree below the characteristic can have differential-constant coefficients and vanish. Applied to a bivariate relation, this gives constant descent directly from elimination.

Bounded-degree differential constants, in characteristic zero or above the degree. In positive characteristic the degree restrictions are essential. These lemmas isolate the constant-descent step in Gao's differential criterion; they do not supply the resultant bounds for residues or a Bertini theorem.

theorem CCDN.differential_constant_mem_base_of_relation {F : Type u_1} {L : Type u_2} [Field F] [IsAlgClosed F] [Field L] [Algebra F L] [Differential L] (hbase : ∀ (a : F), ((algebraMap F L) a)′ = 0) (t x : L) (ht : t′ = 1) (hx : x′ = 0) (R : Polynomial (Polynomial F)) (hR : R ≠ 0) (hchar : CharZeroOrGT L R.natDegree) (hroot : Polynomial.eval t (Polynomial.map (Polynomial.aeval x).toRingHom R) = 0) : x ∈ (algebraMap F L).range

A differential constant satisfying a nonzero bivariate relation of t-degree below the characteristic (or in characteristic zero) lies in the algebraically closed base. The inner variable represents the constant; the outer variable represents t.