Whole-net MNIST-CNN forward rounding budget. The rounded forward is within an explicit closed-form layerBudget of the real conv→relu→conv→relu→maxpool→dense→relu→dense→relu→dense forward, per output logit — the binary32 forward-error bound for the Chapter-3 CNN.

Each weight layer threads identically: conv layers as dense at their fan-in (ic·kH·kW, then c·kH·kW), the dense head at c·h·w / d1; relu and maxpool pass error through exactly (no rounding, no amplification). The budget is the mlp_float_close_uniform nest extended to the CNN's six layers — norm_num-evaluable at a concrete net and magnitude profile.

Per-entry conv drift, slab-refined: a kernel perturbation moves the output entry (o, hi, wi) by at most a times the ℓ1 mass of the channel-o slab (each output reads only its own slab).

Per-entry conv drift against the TOTAL ℓ1 mass — the form the relu margins consume.

ℓ1 conv drift: summed over all output entries, the drift is at most (h·w)·a·‖e‖₁ — the spatial multiplicity h·w is the price of weight sharing (each kernel entry touches every spatial position).

Float pool-backward closeness. Under the pool margin the float post-relu argmax matches the real one (isArgmax_iff), so the pool's backward selector 𝟙[(ci,hi,wi) is its window's argmax]·(pooled cotangent) differs from the certified one only through the pooled cotangent value — an indicator pass-through (indicator ∈ {0,1}), the pool peer of reluMask_close. The two cotangent values ay (float) / ax (real) enter only via their closeness |ay − ax| ≤ e.

Folds the raw finProdFinEquiv encoding back into t3Idx.

The 3-dense head CE ∘ d₅ ∘ relu ∘ d₄ ∘ relu ∘ d₃ is differentiable at any point whose two ReLU pre-activations are off the kinks.

Loss input-gradient of the 3-dense head CE∘d₅∘relu∘d₄∘relu∘d₃ at the pooled vector — one pdiv_comp hop (peel dense W₃) on top of ce_head2_input_grad, exactly as ce_head2 was one hop on ce_head_relu. Note there is NO leading mask: the pool output feeds dense W₃ directly.

The whole head above the conv output — CE∘head3∘maxPoolFlat∘relu — is differentiable at any point with the relu₂ pre-activation off the kinks, no pool ties (POST-relu), and the two head masks off the kinks.

Loss input-gradient at the conv output — the key glue of the conv rung. The chain pdivs through the relu (mask) and the pool (frozen selector): at a smooth point the sum over pooled coordinates collapses to the single argmax term, so

∂(CE∘head3∘pool∘relu)/∂z₂[ci,hi,wi] = relu'(z₂[ci,hi,wi]) · 𝟙[(ci,hi,wi) is its window's argmax] · head3grad(window(ci,hi,wi)).

NB the pool acts on the POST-relu activation, so the smoothness and argmax conditions are stated on relu z₂, not z₂.

Closed form of the conv weight-map pdiv — extracted from the certified VJP (conv2dWeightGradHasVJP) by contracting its .correct field against a basis vector. Kernel entry (o,cc,kh,kw) touches output (co,hi,wi) iff co = o, with coefficient the padded input read convPad. NB the right-hand side does not mention v: the weight map is affine, so its Jacobian is point-free — this is what lets the gradient difference along a step segment collapse to the head drift alone.

The conv weight gradient is the spatial dot Σ_{hi,wi} convPad · cot (the contraction conv2d_weight_pdiv certifies as ∂L/∂W_{o,cc,kh,kw}), re-expressed as a flat Fin (h·w) dot of the padded-input window against the cotangent slab — the form the float dot rounds.

The conv bias gradient is the spatial sum Σ_{hi,wi} cot.

Rounded conv weight update. The float update fl(Wₒ,cc,kh,kw − fl(lr·fl(convPadWin · cotWin))) — the conv weight gradient is a correlation, a dot over the h·w spatial positions — is within sgdErr of the real step W − lr·(Σ_{hi,wi} convPad·cot), the dot's Higham γ (fan-in h·w) as the gradient-error slot. Reuses the generic dotSgd_step_close; the cotangent is supplied (the loss-head exp accuracy lives in cotErr).

Rounded conv bias update — the bias gradient is the spatial sum Σ cot, so the rounded update reduces to sumSgd_step_close.

Numeric conv-weight-step capstone at the committed MNIST-CNN dims (Item C). The Chapter-3 conv2 is 32→32, 3×3, at 28×28 (the conv output grid, before maxpool), so the weight gradient is a dot over 28·28 = 784 spatial positions. At binary32 (u ≤ 2⁻²⁴), lr = 1/10, kernel |W| ≤ 3/5 (the trained-magnitude bound, matching the MLP capstone), every rounded conv2 weight SGD entry is within (a·g)/250 + 10⁻⁷ of the certified real step — where a bounds the conv2-input activation and g the conv2 cotangent magnitude.

Both a and g are a-posteriori / measured quantities (the conv input and back-propagated cotangent are not intrinsically ≤ 1, unlike the softmax−onehot loss head), supplied as hypotheses — the same worst-case→ measured hand-off as the forward δ. The decimal rate 1/250 ≈ 0.4% is dominated by lr·γ₇₈₅ (the gradient's Higham error at learning-rate scale): the conv weight step is as accurate as the gradient itself, no worse.

Numeric conv-BIAS-step capstone at the committed MNIST-CNN dims — the bias peer of mnist_cnn_convW_step_float_budget. The conv2 bias gradient is the spatial SUM ∑ₛ cotWin cot o over the 28·28 = 784 conv-output positions (no input window, so no a factor — the bias Jacobian is the bare channel indicator). At binary32 (u ≤ 2⁻²⁴), lr = 1/10, |b| ≤ 3/5, every rounded conv2 bias SGD entry is within g/250 + 10⁻⁷ of the certified real step — where g bounds the conv2 cotangent magnitude. The same 1/250 rate as the weight step (it is lr·γ₇₈₅, the gradient's Higham error at learning-rate scale), with a·g ↦ g — the bias step is as accurate as the gradient, no worse.

The loss-of-conv2-kernel map is differentiable wherever the relu₂ pre-activation is off the kinks, no pool window ties (POST-relu), and the two head pre-activations are off the kinks.

The loss gradient through a parameter map into a c×h×w activation — the chain rule (pdiv_comp) with the flat activation index split into its triple: Z's Jacobian row contracted with the head's input gradient. Each conv rung's gradAt closed form is this, the conv Jacobian (conv2d_weight_pdiv / conv2d_bias_pdiv) and the head gradient.

Closed form of the conv2 loss gradient at any four-margin point — the chain rule through the conv weight map (gradAt_comp_t3) with the pool-collapsed head gradient (pool_relu_input_grad) and the point-free conv weight Jacobian (conv2d_weight_pdiv). The conv-layer peer of mlp_input_loss_gradAt; the spatial triple sum (vs the MLP's Kronecker collapse) is weight sharing.

The unmasked peer of reluMask_dense_transpose_eq: a bare Wᵀ contraction ∑ₖ Wₗₖ·cₖ = dense (transpose W) 0 c l. The pool feeds dense W₃ with no leading ReLU mask, so the W₃ contraction in the certified conv-2 gradient collapses through this, where the masked W₄/W₅ contractions collapse through reluMask_dense_transpose_eq. NB this is generic in (W, c), so fire it only where the goal has no other matrix contraction (e.g. the spatial ∑ convPad·cot) — see head3_cot_reluMask.

The 3-dense head cotangent in dense/reluMask form. The raw nested ∑ₗ W₃·(𝟙[z₃]·∑_q W₄·(𝟙[z₄]·∑_k W₅·(softmax−onehot))) that pool_relu_input_grad / cnn_conv2_loss_gradAt leave at the pooled vector u equals dense W₃ᵀ 0 (mask z₃ (dense W₄ᵀ 0 (mask z₄ (dense W₅ᵀ 0 (softmax−onehot))))) — the two masked contractions via reluMask_dense_transpose_eq, the unmasked W₃ via dense_transpose_eq. Stated head-locally (no spatial sum) so the generic dense_transpose_eq fires only on the W₃ row. The head peer the conv grad-close bounds against via dense_close (W₃) and cot_step_close (W₄/W₅).

The certified conv-2 loss gradient, head restated in dense/reluMask form — the conv peer of mlp_input_loss_gradAt_reluMask. The two head Wᵀ contractions (under the d₄/d₃ ReLU masks) collapse via reluMask_dense_transpose_eq, the unmasked W₃ contraction via dense_transpose_eq; the conv-output ReLU mask 𝟙[z₂>0] and the pool argmax selector are kept explicit (their float closeness is handled by reluMask_close and MaxPool2MarginQ.poolBack_close). The whole conv gradient is then packaged as the spatial dot ∑ₛ convPadWin·cotWin (convWeightGrad_eq_dot) — the exact quantity the FloatModel gradient's conv-weight dot rounds, so the conv grad-close bounds against this.

Scalar ReLU-mask freeze — the (if z>0 then 1 else 0)·x peer of reluMask_close. Under the sign margin ez < |z| the float and real masks agree, so the masked value is 1-Lipschitz in x. The conv-output ReLU mask 𝟙[z₂>0] in the conv-2 grad-close sits on a scalar cell (not a Vec), so it needs this rather than the vector reluMask_close.

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.

cnnConv2CotMag is nonnegative.

cnnConv2CotBudget is nonnegative for nonnegative input magnitude/rounding and layer bounds.