First-order definability of Darmon points in number fields

For a given number field $K$, we give a $\forall\exists\forall$-first order description of affine Darmon points over $\mathbb{P}^1_K$, and show that this can be improved to a $\forall\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\"ager & 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.