Definable Eventual Equalizers

The solutions of algebraic differential equations in certain valued differential fields, including the differential field of transseries, can be analyzed using a Newton diagram method.

In this paper, we show that (eventual) equalizers, a crucial part of this process, can be obtained uniformly and definably from the coefficients of the input differential polynomials.

We also obtain similar definability results for a certain compositional conjugation which is used repeatedly as an intermediate simplification step.