In case it’s useful for anyone else (as it took me a second to convince myself) - here’s the argument for why this validity check ensures there is no height h where agreeing[h+1] < (agreeing[h] - at[h]) * \frac{1}{2}. Let’s call this invalidity condition (1).
Assume the validity check passes, but there are some heights where (1) occurs. Let h be the lowest of such heights. Let x be the “current set of validators” under consideration at the step that considers h in the validity check (x is at first 1, then \frac{1}{2}, then \frac{1}{4}, etc). Thus, as agreeing[h+1] < (agreeing[h] - at[h]) * \frac{1}{2}, clearly h is the largest height such that at least \frac{x}{2} agrees. But as the validity check passes, we have that agreeing[h+1] \ge (agreeing[h] - at[h]) * \frac{1}{2}. However, this is clearly a contradiction with (1). Thus, no such height h can exist where agreeing[h+1] < (agreeing[h] - at[h]) * \frac{1}{2}.