I'm ready to more forward on this one.  I've improved the assertions, explanations, and variable names.  I also added references to show that the foundations are firm.  After tens of millions of trials, I haven't found a single misrounding.  I can't prove "correctly rounded" but am content with "highly accurate".  The speed is comparable to what we had in 3.7, so I think it is a net win all around.