Binary tree To Red-Black tree
Well, apparently my answer was wrong. The algorithm, at least. The theorem seems to be okay, if a little unreadable.

More in line with that proof, the algorithm should be

if n is root,   # as before
    n.color = black
    n.black-quota = n.height / 2, rounded up.
    # black-quota could start at any value between n.height/2 and n.min-height

else if n.parent is red,   # as before
    n.color = black
    n.black-quota = n.parent.black-quota.

else (n.parent is black)
    n.black-quota = n.parent.black-quota - 1

    # check that the subtree isn't totally uncolorable
    if n.min-height &lt; n.black-quota then
        error "shortest path was too short"

    # use red only if the subtree is not colorable (as a tree), with given quota
    if n.height &lt;= n.black-quota*2  then
        n.color = black

    else
        n.color = red


What I meant by the last condition is that 17 is red for the sole reason that you can't color it black i.e. $b(17) \notin [\frac{1}{2}h(17), m(17)]$.

Hopefully that works. Thanks for pointing out the error!