The cifar8-BN step tie at BATCH statistics — the un-fused, batched gradient nodes #

Cifar8BnTieG.cifar8Bn_train_step_tiedG ties the per-image renders (cifar8w_bn_*, BN over [2,3], one x : Tensor3 at a time). The artifacts planning/cifar-batch-bn-rerender.md builds — cifar8wb_bbn_{sgd,mom,adam,bf16…}_train_step.mlir, from Proofs/Codegen/CnnBbnRender.lean — are the same 38 parameters with every BatchNorm reducing over [0,2,3]: the batch is coupled, so there is no per-example statement to make. This file states those artifacts' gradient nodes at the batched vocabulary ResNet-34's tie uses (Foundation/GradNodesB, GradNodesBAt, Batched/BackLinks): all 38 parameter tensors, each *GradB node denoting the certified batched Σ_n gradient at the layer's input and the cotangent the rendered backward chain delivers.

What is tied, and how the chain is written #

The chain is the render's, node for node, in CnnBbnRender.lean's emission order:

sm    = softmaxRow(logits)            g    = scaleB(1/B, subB(sm, %onehot))
dyA   = selectPosB(ha, denseRowBack(Wb, g))        dy9 = selectPosB(h9, denseRowBack(Wa, dyA))
dx9   = denseRowBack(W9, dy9)
dac8  = maxPoolBackB(ac8, dx9)        dbn8 = selectPosB(bn8, dac8)      dhc8 = bnBatchBack(g8, hc8, dbn8)
dac7  = convBackBatched(W8, dhc8)     dbn7 = selectPosB(bn7, dac7)      dhc7 = bnBatchBack(g7, hc7, dbn7)
dpool3 = convBackBatched(W7, dhc7)    dac6 = maxPoolBackB(ac6, dpool3)  …

Every forward activation is the den of the forward node the render emits (batchOp (convAt bf16 …), bnBatchF, batchOp relu, batchOp maxPool, batchOp dense), and every cotangent is the den of the backward node — except the BatchNorm link, which is bnInB (the network-layout twin of den bnBatchBack; BackLinks.bnInB_eq_den_bnBatchBack is the identity, and bnInB_eq_bnBackB says it is the certified bnBatchLA VJP). So the statement is about exactly the values the artifact computes, with no symbolic cotangent and no free activation.

What is NOT stated here (the second half ResNet-34's tie has and this net does not yet): that this chain IS the certified whole-net backward — r34IdCotIn_eq_vjp's analogue, which needs the batched-BN cifar8 forward's HasVJPAt and the per-link _eq_vjp lemmas. Each link's den theorem exists (den_maxPoolBackB, den_convBackBatched_eq_cInB, bnInB_eq_bnBackB, the relu mask by rfl), so that half is composition work, listed in the planning note. Numerically the gap is covered by tests/TestCifar8BbnGradCheck.lean and tests/cifar8_bbn_jax_ref.py.

N is a binder, bf16 is a flag. The bf16 artifacts' conv forward, input-VJP and weight gradient are the bf16 kinds; the capstone takes bf16 and reaches them through ConvWTiedBAt (Bf16Erasure: at the identity rounding the bf16 kind denotes its f32 peer). BatchNorm, bias and dense nodes carry no flag because no render switches them.

The loss cotangent is the plain mean softmax-CE's, at a general target t (the graph input %onehot): g = (softmax(logits) − t) / B, as the render composes it from softmaxRow, subB and scaleB. There is no label smoothing in the cifar8 recipe.

The rows := 1 head. The render's head backward uses denseRowBack (rows := 1) and softmaxRow (m := 1), whose operands are typed N * (1 * n); 1 * n is not n definitionally, so the head cotangents are re-indexed with castB1 / unB1 (Nat.one_mul), exactly the reshape the emitted text performs between those nodes and their neighbours.