t ↦ 1/√t is Lipschitz on [ε, ∞) with constant 1/(2·ε·√ε) = 1/(2ε^{3/2}). Proof: the algebraic identity 1/√a − 1/√b = (b−a)/((√b+√a)·√a·√b), then the ε-floor bounds the denominator below by 2ε√ε. The keystone for pushing a variance-rounding error through the BN inverse-stddev.

BN inverse-stddev budget at the OPERATING POINT (a-posteriori). The general form of bnIstd_close (below): the 1/√ Lipschitz floor is a variance lower bound V ≤ σ²+ε (both float and real), not the ε-floor. rsqrt_lipschitz is floor-agnostic, so the bound becomes ers/√V + evar/(2V√V) — and since the measured σ² is O(1) (never near 0), V ≈ σ²+ε ≫ ε makes this ~(σ²/ε)^{3/2} tighter than the ε-floor bnIstd_close (empirically ~10⁷× on the CIFAR-BN probe, scripts/certs/cifar_bn_margin_probe.py). A conditional bound under hVfv, hVbn, hrs, hclose; apart from bnIstd_close (its V = ε case) nothing in the repo applies it.

BN inverse-stddev rounding budget (the keystone). Model the GPU inverse-stddev by a supplied fistd with relative accuracy ers (|fistd t − 1/√t| ≤ ers·(1/√t)), evaluated at the rounded fvarε ≥ ε (the float σ²+ε, within evar of the real σ²+ε). Then the float istd is within ers/√ε + evar/(2ε√ε) of the certified bnIstd. The first term is the rsqrt accuracy lifted to the ε-floor; the second is the variance rounding pushed through rsqrt_lipschitz. The BN analog of the softmax exp-accuracy handoff; bnIstd_close_at at the floor V = ε.

BN forward closeness, normalize chain. Given the mean within emean and the inverse-stddev within eistd of the certified values (the latter from bnIstd_close), plus magnitude bounds (|xᵢ−μ| ≤ D, |istd| ≤ S, |γ| ≤ G, |β| ≤ Bbnd), the rounded BN forward output is within bnNormBudget of the real bnForward per coordinate. The output half of the per-example BN bridge; compose with bnIstd_close (istd) and the mean/var Higham budgets.

The mean reduction's budget, parameterised by the REDUCTION'S OWN SPEC. bnMean_close below is this at fsum := M.sum, the concrete LEFT FOLD — and a GPU does not reduce left to right, so a number stated through that instance is about a program we do not ship. This form takes any fsum whose forward error meets a fan-in γn (hypothesis hsc). Classically every summation order satisfies such a bound: sequential summation is the worst of them at γ = (1+u)^{n+1} − 1, and a tree's is (1+u)^{⌈log₂n⌉+1} − 1. That the shipped kernel's reduction meets hsc is the hypothesis, not proved here; given it, the proof is bnMean_close's with one hypothesis substituted.

Note: Only the SUM is parameterised. The division by the exact width is M.div, one rounding, and there is nothing to model about it.

BN mean rounding budget. The float mean fl((Σx)/n) (rounded sum, then a rounded division by the exact n) is within u·(1+u)^{n+1}·A + ((1+u)^{n+1}−1)·A of the real bnMean, under |xᵢ| ≤ A. Standard: sum_close's fan-in γ plus one division rounding. Note: Stated at the concrete left fold M.sum; bnMean_close_of above is the form that covers the kernels we ship.

BN variance rounding budget. The float variance (rounded centered squares, rounded sum, rounded /n) is within bnVarBudget of the real bnVar, given the mean within emean and the centered bound |xᵢ−μ| ≤ D. The coupled Higham reduction: each centered term inherits emean (via mul_close), then a fan-in γ sum and a division rounding — the variance peer of bnMean_close.

Per-example BN forward closeness (assembled). The float BN forward at the rounded mean fl((Σx)/n) and the GPU inverse-stddev fistd fvarε is within bnNormBudget of the certified bnForward, with the mean error discharged by bnMean_close, the inverse-stddev error by the bnIstd_close keystone (the rsqrt accuracy + rsqrt_lipschitz), and the normalize chain by bnForward_close_of. fvarε's closeness to σ²+ε (hvar) is taken as a hypothesis; FloatModel.bnVar_close supplies a variance budget in the rounded-sum form.