I love the colouring approach, that's same approach I use when explaining/analysing binary search. One advantage of this approach that was not explicitly mentioned is that the behaviour is clear and well-defined when the target element appears multiple times, unlike some implementations where it is unspecified which occurrence will be found. Minor point: I prefer to negate the predicate, i.e. "is_red" instead of "is_green". Then the definition of the binary_search is "return the first index for which the predicate returns true", which I find more natural.

But the three if-statements for the base cases are horrible and completely unnecessary!

We can't initialise `left` to 0 because that might violate the invariant (it is possible that `is_green(arr[0])` will return False). However, we can initialise `left` to -1 (!) if we define `is_green(arr[-1])` to be True, and make sure to never actually compute `is_green(arr[-1])`. (Note when I say `arr[-1]` I am referring to the fictional element before the first element, not the element specified by Python's negative index rules.)

Similarly, we can initialise `right` to `len(arr)` if we define `is_green(arr[len(arr)])` to be False.

So the first line becomes

    left, right = -1, len(array)

and the three if-statements can be deleted.

This uses an exclusive-exclusive range, which can be a little unsettling for people used to inclusive-exclusive ranges. But I think the elegance of the invariants totally justifies it.

Another reason I prefer exclusive-exclusive over inclusive-exclusive for this is that it makes the rounding in `(left + right) // 2` consistent with the "uniqueness" of the middle. An array with 3 items has a unique middle (index 1), while an array with 4 items has two "middles" (index 1 and index 2). With an inclusive-exclusive range, the rounding does not reflect this: when the size is 3, `(0 + 3) / 2` gives 1.5 (which must be truncated to give the correct index); when the size is 4, `(0 + 4) / 2` gives 2.0 (which arbitrarily picks index 2). It bothers me that the case with a unique middle involves rounding (which must be done in the correct direction!) and the case with no unique middle returns a misleadingly exact result. With an exclusive-exclusive range on the other hand, it all works nicely: when the size is 3, `(-1 + 3) / 2` gives 1.0 (which is the unique middle); and when the size is 4, `(-1 + 4) / 2` gives 1.5 (which can be rounded up or down to get the two "middles").