Float Drift — measured vs proved
Every floating-point operation nudges the result by up to u (one ULP). Over n operations the drift you can prove — every nudge aligned — grows like n·u. The drift unbiased rounding actually delivers grows like √n·u, about √n times smaller, because the nudges cancel in a random walk. Flip the rounding mode and watch the measured slope swing between 1 and ½.
measured slope 0.43≈ ½ → √n, the stochastic winat n=4000, the proved bound is 63× the stochastic drift
…and under cancellation, the relative bound dies but the absolute one holds
Compute x·y − z·w with x·y ≈ z·w. As they cancel, the relative error explodes toward ∞ — but the absolute forward-error bound (the fold behind AbsoluteBridge.lean) never breaks. That is why the proofs carry an absolute bound, not a relative one.