Rational certificates for the Erlang loss recursion ($b_0=1,b_j=a{b}_{j-1}/(j+a{b}_{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.