Rational certificates for the Erlang loss recursion (source code)

= Rational certificates for the Erlang loss recursion
{title2=$b_0=1,\quad b_j=ab_{j-1}/(j+ab_{j-1})$}

For rational <offered load>, every step of the stable recursion for the <Erlang loss formula> is rational. Comparing the final numerator and denominator with rational thresholds therefore certifies signs without floating-point uncertainty. Opposite certified signs of a continuous fixed-point residual imply a root by the <intermediate value theorem>; several alternating intervals can prove multiple <Erlang fixed points> under <alternative routing>.