What stays true: invariants and reduction

Ask of any loop you write: what is true at the top of every iteration, no matter how many iterations have run before? Most solvers cannot answer. The ones who can — who can state the loop’s invariant — know their bound updates are correct without testing every case, because the invariant is the proof.

The reasoning replays make this the keystone move. The Binary Search replay states it plainly: at the start of every call, if the target exists in the list, it is within the inclusive interval from left to right. Everything else in binary search — the halving, the bound updates, the -1 return — is bookkeeping in service of that one sentence.

Why the invariant outruns the test cases

A test suite shows the loop works on the cases you thought of. An invariant shows the loop works on every case, including the ones you did not. The difference matters at the boundaries — mid + 1 versus mid, <= versus < — where off-by-one bugs live and where test suites are weakest.

Check the bound updates against the invariant instead:

• You proved nums[mid] < target, so the target cannot be at mid or before → lo = mid + 1 keeps the invariant.
• You proved nums[mid] > target, so the target cannot be at mid or after → hi = mid - 1 keeps it.
• The window shrinks every iteration → the loop terminates.

Four lines, each justified. No test run required — and if a future edit breaks one of them, the invariant tells you which line it broke.

Reduction: the other thing that stays true

The replay’s reduce move pairs with the invariant. Binary search reduces “find the target in a sorted list” to “narrow an interval” — a problem you already know how to think about. The reduction is also an invariant at the problem level: the target, if present, is always inside the current window. When the window is honest, the answer is inside it; when the loop ends, its absence is proven, not guessed.

Learning to see reductions changes what a new problem feels like. “Find the peak in a mountain array” reduces to binary search on the slope direction. “Find the first bad version” reduces to binary search on a predicate. The surface changes; the invariant is the same sentence with new nouns.

The move, stated once

Before the loop: write the invariant in one sentence (“if it exists, it is in [lo, hi]”). After each update: one sentence proving the invariant survived. At termination: one sentence translating the invariant into the answer. If any of the three sentences will not come, the loop is not ready — and the replay’s job is to make you write them until they come easily.

The rest of the series

The invariant is the backbone of phase two in the series overview. With the plan proven, what remains is execution and review: Committing and looking back.