First-order definability of Darmon points in number fields

For a given number field $K$, we give a $\mathrm{\forall }\mathrm{\exists }\mathrm{\forall }$-first order description of affine Darmon points over ${\mathbb{P}}_K^1$, and show that this can be improved to a $\mathrm{\forall }\mathrm{\exists }$-definition in a remarkable particular case. Darmon points, which are a geometric generalization of perfect powers, constitute a non-linear set-theoretical filtration between $K$ and its ring of $S$-integers, the latter of which can be defined with universal formulas, as has been progressively proven by Koenigsmann, Park, and Eisenträger & Morrison. We also show that our formulas are uniform with respect to all possible $S$, with a parameter-free uniformity, and we compute the number of quantifiers and a bound for the degree of the defining polynomial.