The unit roundoff is nonnegative: err 1 gives |rnd 1 − 1| ≤ u.

The rounding of 0 is 0 (forced by the relative-error model at x = 0).

A rounded dot product against the all-zero vector is 0.

One rounding on top of an inherited error. If the operand a is within e of the exact b and |a| ≤ A, then fl(a) is within u·A + e of b — the step every rounded add/sub/mul/div close takes (each is M.rnd of the exact operation).

Rounding grows a magnitude by at most the factor 1 + u.

Rounded dot product forward error — |fl(x·y) − x·y| ≤ ((1+u)^(n+1) − 1)·Σᵢ|xᵢyᵢ|.

The classical bound (Higham §3.1), in the exact compounded form (no n·u < 1 side condition), for the left fold M.dot. (The classical bound holds for every summation order; only the left fold is formalized here.) The exponent is n+1 rather than the optimal n because dot rounds the seed addition with 0 too.

Mixed-precision dot forward error, decomposed. The leaf precision contributes only a flat per-leaf term (2·u_leaf + u_leaf²)·Σ|xᵢyᵢ| (NOT fan-in amplified); the fan-in amplification rides entirely on the accumulate precision as the Higham γ-factor ((1+u_acc)^(n+1) − 1). That separation is exactly why bf16-mixed is non-vacuous where pure bf16 is not: the 1/u fan-in wall sits at u_acc = 2⁻²⁴, not at the leaf precision.

dot_close_mixed folded to a single Σ|xᵢyᵢ| factor — the directly instantiable form. Bounds the leaf-rounded magnitudes by (1+u_leaf)², so the whole error is [γ_acc·(1+u_leaf)² + (2u_leaf + u_leaf²)]·Σ|xᵢyᵢ|. At bf16 leaf / fp32 accumulate (u_leaf = 2⁻⁸, u_acc = 2⁻²⁴, fan-in a few hundred) the bracket is ≈ the flat 2·2⁻⁸ ≈ 0.8% leaf term plus a negligible accumulate γ — the shipped-artifact budget.

Mixed-precision dense forward error. The leaf precision enters only through the flat dotMixed term; the accumulate precision rides the bias add and the fan-in γ. The bf16-mixed / fp8 dense layer falls out by setting L.u.

Rounded dense layer forward error, with inherited input error. If xt is within e of the real activation xa coordinatewise, then |M.dense W b xt j − dense W b xa j| ≤ denseErr W b xa e j.

dense_close at a fresh (unperturbed) input — the e = 0 face.

ReLU propagates error without amplification. No rounding term: max with 0 is exact in floating point, so the float net applies relu bare and the bridge only needs 1-Lipschitz-ness.

e^x − 1 ≤ x/(1−x) for 0 ≤ x < 1 — the exp analogue of the γ-form, from 1 − x ≤ e^(−x) alone; keeps the numeric head budget in norm_num country.

The classical γₖ bound: for k·u < 1, (1+u)^k − 1 ≤ k·u/(1 − k·u). Turns the compounded budgets into plain rational arithmetic at a concrete u (e.g. u32) — norm_num country, no big-power evaluation.

x ↦ x/(1−x) is monotone on [0, 1) — lets a u ≤ u32 hypothesis ride through the γ-form.

Replacing the power term and the inherited error in layerBudget by upper bounds gives an upper bound — the monotonicity step the numeric instantiations chain through.

ReLU never grows magnitudes.

Real dense-layer magnitude bound: |denseⱼ| ≤ layerAct m w β a.

denseErr under uniform magnitude bounds is at most the closed-form layerBudget.

γ-form at a concrete exponent and target, monotone through u ≤ u32.

Rounded product with inherited operand errors.

Rounded addition with inherited operand errors. fl(xt ⊕ yt) is within u·(|x| + ex + |y| + ey) + (ex + ey) of the exact x + y, given |xt − x| ≤ ex and |yt − y| ≤ ey. The additive peer of mul_close; the residual fan-in's float budget.

Rounded SGD update: fl(θ − fl(lr·gt)) is within sgdErr of the real step θ − lr·g. Two roundings plus the inherited gradient error.

The float-side kink condition. If the pre-activation error ez cannot flip any sign — ez < |zᵢ|, a quantitative margin, the float analogue of the suite's x k ≠ 0 off-the-kink hypotheses — then the float and real masks agree and the mask is 1-Lipschitz in the value.

Cotangent through one layer — mask(z, Wᵀ·c), float vs real. The transposed matvec is dense with zero bias, so the dot machinery is reused wholesale; under the quantitative margin the mask passes the layerBudget through unchanged.

Rounded sum forward error — ((1+u)^(n+1) − 1)·Σ|xᵢ| for the left fold M.sum (exponent n+1 because the seed addition with 0 rounds).

|softmax − oneHot| ≤ 1 — the magnitude of every softmax-CE head cotangent: softmax lies in [0, 1] and a one-hot entry is 0 or 1.

Softmax perturbation, elementary ratio form: a coordinatewise logit error δ moves every softmax output by at most e^(2δ) − 1. Proved by sandwiching softmax(z̃) ∈ [e^(−2δ), e^(2δ)]·softmax(z) with bare exp monotonicity — no mean-value theorem.

cotErr is nonnegative (it bounds an absolute value) — under eexp ≥ 0, δ ≥ 0, and the denominator condition smRho < 1. The cot_step_close precondition for any backward grad-close that runs the softmax−onehot head.

Float softmax vs real softmax at the same logits (part A): the rounded exp/sum/div head is within u·(1+κ) + κ absolutely, where κ = (eexp + ρ)/(1 − ρ) compounds the exp accuracy and the sum rounding. The sandwich is the same ratio argument as softmax_perturb — division-perturbation never appears.

The rounded softmax−onehot cotangent is within cotErr of the certified real gradient softmax(z) − onehot — the pdiv-certified ∂(crossEntropy)/∂logits (softmaxCE_grad). This discharges the g̃ ≈ g hypothesis of the mlp_*_step_float_close capstones: eg := cotErr u eexp δ n, where δ bounds the float-vs-real logits (worst case: the forward layerBudget; in practice: an a-posteriori measured value, since e^(2δ) − 1 is only sharp for small δ).

Argmax preservation under a bounded logit perturbation. If every coordinate of the perturbed logits z' is within B of the reference logits z, and z's strict top-1 margin at k exceeds 2B (z k − z i > 2B for every other class i), then k is still the strict argmax of z'. The depth-1 honest fp8 claim: a B-accurate matmul cannot flip the prediction on a >2B-margin input. B is a hypothesis, so the statement holds both for the proven worst-case bound (dense_close_mixed) and for any measured a-posteriori drift — the demo's empirical B = max|Δlogit| plugs into the same theorem. Conditional like the suite's quantitative ReLU margins.

Mixed-precision dense forward error, uniform-magnitude budget. Under |Wᵢⱼ| ≤ w, |bⱼ| ≤ β, |xᵢ| ≤ a, every E4M3-mixed logit is within the closed-form denseMixedBudget of the exact-ℝ logit — evaluable by norm_num at a concrete net.

Monotone upper bound for denseMixedBudget, keeping the (1+uacc)^(m+1) power abstract: replace the accumulate by U ≥ uacc, the fan-in γ-factor by g ≥ (1+uacc)^(m+1)−1, and the two leaf pieces by P ≥ (1+uleaf)², Q ≥ 2·uleaf+uleaf². The result has no power left, so a concrete instance (e.g. m = 784) evaluates by norm_num without unfolding the 785-fold npow — the layerBudget_le_of analogue for the two-roundoff budget.

dotMixed with an exact leaf (u_leaf = 0) is the plain rounded dot. The fp32 specialization: no input rounding ⇒ dot_close_mixed collapses to dot_close (the leaf term 2·0 + 0² = 0 vanishes, the leaf-rounded magnitudes become the real ones). Confirms the two-roundoff budget is a genuine generalization of the single-u budget, not a reparametrization.

|a| ≤ C + e from |a − b| ≤ e and |b| ≤ C — lifts a closeness + a base magnitude to a float magnitude (the float cotangent bound from the real bound plus the drift).

Float dot against a perturbed cotangent — the conv-2 grad-close's final contraction (the conv peer of the MLP's scalar mul_close: a dot, because of weight sharing). M.dot A B̃ (exact left operand A, float cotangent B̃) vs the certified ∑ Aᵢ·Bᵢ splits into the Higham dot rounding on A·B̃ (dot_close, fan-in n) plus the per-entry cotangent drift |B̃ᵢ − Bᵢ| ≤ eB. With |Aᵢ| ≤ a and |B̃ᵢ| ≤ Ct, the bound is closed-form and norm_num-evaluable.

Float sum against a perturbed summand — the conv-BIAS grad-close's final reduction, the M.sum peer of dot_perturbed_close (no left operand A: the bias Jacobian is the bare channel indicator, so the contraction is a plain reduction, not a dot). M.sum B̃ vs the certified ∑ Bᵢ splits into the Higham sum rounding on B̃ (sum_close, fan-in n) plus the per-entry drift |B̃ᵢ − Bᵢ| ≤ eB. With |B̃ᵢ| ≤ Ct the bound is closed-form.