MLP forward extraction (Chapter 2). The rounded 3-layer MLP is within the layer-2 denseErr budget (at inherited error e₁) of the real MLP — the same dense/relu composition whose train step is certified in MlpTrainStep.lean. The hypotheses h₀/h₁ uniformize the per-coordinate layer-0/1 budgets into e₀/e₁; at any concrete net they are discharged by finite max over the d₁ (resp. d₂) coordinates.

MLP forward extraction, uniform-magnitude budgets. mlp_float_close with the e₀/e₁ uniformization discharged once and for all from coordinatewise magnitude bounds |Wᵢ| ≤ wᵢ, |bᵢ| ≤ βᵢ, |x| ≤ a. The budget is a closed form in the dims and magnitudes — evaluable by norm_num at a concrete net.

Numeric capstone at the committed MNIST-MLP dims and TRAINED magnitudes (the MainMnistMlpVerified.lean net: 784→512→512→10; |W| ≤ 3/5 covers the measured max|W| = 0.52 of a real 12-epoch 97.8% run — He init already exceeds the prettier 1/32 in its tails). For any rounding model at binary32 accuracy (u ≤ 2⁻²⁴), every rounded logit is within 5100 of the exact-real logit — the worst-case logit magnitude at these bounds is ≈4.5·10⁷, so ≈10⁻⁴ relative, the same relative scale as at small weights. All three layer budgets discharge by norm_num through the γ-form; no big-power evaluation.

Measured on the live run (scripts/certs/margin_probe.py): actual logit drift ≤ 1.6·10⁻⁵ — the ≈3·10⁸ gap between the worst-case bound and reality is the worst-case-composition blow-up (307·e Lipschitz amplification per layer at these magnitudes), the quantitative case for a-posteriori certificates past toy depth.

The MLP's first two rounded layers from a fresh input: layer 0's pre-activation (and its ReLU) within E₀ = layerBudget … a 0, the real layer-0 activation within A₁ = layerAct d₀ w₀ β₀ a, and layer 1's pre-activation within layerBudget … A₁ E₀ — the forward prefix every step capstone below starts from.

Rounded output-layer weight update (W₂). The float update fl(W₂ᵢⱼ − fl(lr·fl(ã₂ᵢ·gtⱼ))) — outer-product gradient from the stored float forward activation, as the rendered trainer computes it — is within an explicit budget of the real step W₂ᵢⱼ − lr·(a₂ᵢ·gⱼ). The real target is Mat.outer a₂ g i j = emitWeightGrad's entry, the quantity mlp_layer2_weight_grad_bridge proves equal to the pdiv-Jacobian contraction — so this chains the float step to the certified gradient. Takes the output cotangent gt ≈ g as a hypothesis; softmax_ce_cot_close discharges it with eg := cotErr u eexp δ n.

Rounded output-layer bias update (b₂) — the bias gradient is the cotangent (emitBiasGrad), so this is sgd_step_close directly.

Rounded hidden-layer weight update (W₁), through the backward chain. The float cotangent ct₁ = mask(pt₁, W₂ᵀ·gt) — computed from the rendered pre-activation and the rounded transposed matvec, exactly the structure of the rendered backward — is within layerBudget of the real c₁ = mask(p₁, W₂ᵀ·g) (the mlpCotOut1 closed form), given the quantitative margin E₁ < |p₁ᵢ| at every layer-1 pre-activation: the forward rounding error must not flip a ReLU. Then the update is within sgdErr of the real W₁ᵢⱼ − lr·(a₁ᵢ·c₁ⱼ), the quantity mlp_layer1_weight_grad_bridge certifies. W₀/b₁/b₀ are the same instantiation one mask deeper.

Rounded hidden bias update (b₁) — the gradient is the layer-1 cotangent itself (emitBiasGrad), so this is the cotangent chain followed by sgd_step_close.

Rounded input-layer weight update (W₀) — the cotangent crosses BOTH masks, so both quantitative margins are required; the activation operand is the raw input x, identical in both nets (zero inherited error). The real target W₀ᵢⱼ − lr·(xᵢ·c₀ⱼ) is the certified layer-0 step (mlp_layer0_weight_grad_bridge).

Rounded input bias update (b₀) — the layer-0 cotangent directly.

Numeric gradient capstone at the committed dims and TRAINED magnitudes (784→512→512→10, |W| ≤ 3/5 covering the measured max|W| = 0.52): binary32 accuracy (u ≤ 2⁻²⁴), lr = 1/10, |b|, |x| ≤ 1, |g| ≤ 1 (a softmax−onehot cotangent is always in [−1,1]), cotangent taken exact — then every rounded W₂ SGD entry is within 5/4 of the certified real step.

The budget decomposes honestly: ~1.2 of it is lr·E₁·|g| — the forward budget riding through the gradient at learning-rate scale — while fresh backward rounding contributes only ~2·10⁻³. The gradient step is as accurate as the forward pass, no worse. Measured on the live run (scripts/certs/margin_probe.py): actual W₂ step deviation ≤ 7.5·10⁻⁹ — the worst-case-vs-measured gap is the a-posteriori case in numbers.

Numeric head budget at the committed MNIST output (n = 10): for any model at binary32 accuracy, exp accurate to eexp ≤ 10⁻⁶ (an assumed accuracy for GPU exp, not measured in the repo), and float logits within δ = 1/100 of real, the rounded softmax−onehot cotangent is within 21/1000 of the certified gradient — almost all of it the e^(2δ) − 1 ≈ 2δ logit-perturbation term; the head's own rounding contributes < 4·10⁻⁶.

δ = 1/100 is an a-posteriori-style hypothesis: the worst-case forward logit budget (≈5100 at trained magnitudes) makes e^(2δ) − 1 vacuous, so a useful head budget needs the measured logit error — exactly the hand-off point from worst-case to a-posteriori analysis. Empirically validated (scripts/certs/margin_probe.py): measured drift on a real 12-epoch run is ≤ 1.6·10⁻⁵, 600× inside the 1/100 hypothesis.

The worst-case E4M3 per-logit budget at the MNIST-linear dims (784→n; E4M3 leaf u_leaf ≤ 2⁻⁴, fp32 accumulate u_acc ≤ 2⁻²⁴; pixels |x| ≤ 1, trained |W| ≤ 3/5, |b| ≤ 1): every E4M3-mixed logit is within 61 of the exact-ℝ logit. The leaf term (2·2⁻⁴ ≈ 12.5%)·∑|xW| dominates (the fp32 fan-in γ at 784 is ≈5·10⁻⁵, negligible) — this is the worst-case, all-errors- aligned figure. The demo (scripts/demos/mnist_e4m3_demo.py) measures the actual drift at max|Δlogit| = 0.38 (errors cancel), the a-posteriori B; both feed argmax_preserved.

Verified E4M3 MNIST-linear argmax preservation. For the certified linear classifier at E4M3 leaf precision / fp32 accumulate, pixels |x| ≤ 1, trained |W| ≤ 3/5, |b| ≤ 1: whenever the exact-ℝ logit margin at the top class k exceeds 2·61 = 122, the E4M3-mixed forward keeps k as the strict argmax — provably the same prediction. Depth-1 makes the single-matmul bound the end-to-end bound, so this is the one realistic fp8 case with an honest accuracy guarantee (no vacuous depth compounding). The 122 is the worst-case threshold; with the demo's measured B = 0.38 the same argmax_preserved covers the >0.76-margin inputs — empirically 92.89% of the MNIST test set (scripts/demos/mnist_e4m3_demo.py). fp32 ≈ exact-ℝ (within u_acc), so the demo's fp32 margins are the relevant quantity.