> I don't think a Euclidean domain is quite the right thing for I because there's no obvious total order, and I think you need a total order to state the sortedness precondition on the array contents. Also, lots of Euclidean domains (like ℚ or ℝ) are dense and therefore could lead you to nonterminating recursion. And it isn't obvious to me that "mid" requires so much structure from I.

I think you may be confusing integral domains (https://en.wikipedia.org/wiki/Integral_domain) with Euclidean domains (https://en.wikipedia.org/wiki/Euclidean_domain). Although any field is a Euclidean domain, the structure is not very useful (what I am used to calling the norm, but Wikipedia calls the Euclidean function, may be taken to be identically 0, and the remainder from every division may also be taken to be 0). But anyway, I was just free associating (no pun (https://en.wikipedia.org/wiki/Associative_property) intended).

I certainly agree that one can create a structure that encodes the algebra of binary search, and, at a casual glance, your definition looks good to me. I meant only that such a structure seems unlikely to do much more than to encode binary search (unlike, say, affine spaces, which are useful in a very broad variety of settings for which they have not been purpose-built) … although of course any mathematical structure, howsoever abstract or specialised, will find other uses if enough people get interested in it.