The finite lexicographic lift tie-break is coherent

Expand the determinant polynomial in [F3] along its lifted-height column. It has constant coefficient equal to the original determinant and one perturbation term for each row; the coefficient of the query row's perturbation is its cofactor, which is $O_d$ up to sign. By [A1] this coefficient is nonzero, so the polynomial is not identically zero.

The exponents $2^{r_i}$ are distinct because the ranks in [F3] are distinct across the fixed universe [F1]. Thus no two perturbation terms have the same exponent and their nonzero coefficients cannot cancel. The sign selected by the procedure is exactly the sign of the first nonzero coefficient in this one polynomial, so it is a well-defined sign of one common lifted tuple, not a separate choice for each predicate.

If the original determinant is nonzero, its constant coefficient is the unique term of exponent $0$, while all perturbation exponents are positive; therefore the first nonzero coefficient is the original determinant and its sign is unchanged. If the original determinant is zero, step 1.1 shows a nonzero tie polynomial and step 2.1 gives its unique first coefficient. The finite set $U$ supplies one fixed rank assignment for every tuple, so the signs are coherent and the procedure uses no arbitrary epsilon choice.