The batch-statistics cifar8-BN backward chain IS the certified whole-net VJP #

Cifar8BbnStepTieB.cifar8Bbn_train_step_tiedB ties the thirty-eight gradient NODES of the cifar8wb_bbn_* train steps: each denotes the layer's Jacobian contracted with the cotangent the rendered backward chain hands it. That theorem takes the cotangents as the chain delivers them. This file is the other half — that the chain delivers the right ones: the backward chain those artifacts render, read in the BackLinks vocabulary the node tie uses (reluMaskB, bnBackB, cInB, the per-example pool scatter, rowDenseBackFlat), IS the backward of the certified VJP of the whole batched forward, relu ∘ dense ∘ relu ∘ dense ∘ dense ∘ pool ∘ (conv → BN → relu)² ∘ …, at every batch size N. ResNet-50's r50InputGradB_eq_r34B_full_vjp is the statement this one mirrors; what ResNet-50 does with sixteen opaque bottleneck witnesses, this net does with seventeen concrete CertLayers, because every stage of it is a layer the suite already certifies.

How it is built #

• maxPool2Layer — the batched 2×2/s2 max pool as a CertLayer: batchMapHasVJPAt over the per-example maxPoolFlatHasVJPAt', certified where every example's windows attain their max once (MaxPool2Smooth), its graph the render's .maxPoolBackB, faithful by batchMapAux_eq_batchMapHasVJPAt with each row's tie rfl. The 2×2 peer of HeadLayers' 3×3/s2 stem pool.
• cifar8BbnLayer — the net: eight cbReluLayers (conv → true BN → relu) and four pools in four stages, then denseLayer, reluOut, denseLayer, reluOut, denseLayer. CertLayer.comp does the composition proof; this file only names the layers.
• Cifar8BbnSmoothAt — the smooth-point hypotheses, one per kink: eight pre-relu activations off zero, four pools with unique window maxima, two head pre-activations off zero, each stated at a NAMED running activation (c8A1 … c8RA) so the .ok discharge stays one comp_ok_of per layer.
• cifar8BbnInputGradB — the chain, written out; cifar8BbnBHasVJPAt_backward says the layer's VJP backward is that chain, cifar8BbnInputGradB_correct reads it as ∑ pdiv … * dy, and cifar8BbnLayer_fwd says the layer's forward is the committed composite cifar8BbnForwardB.

Scope #

A smooth-point statement at one precision: the conv nodes are the f32 kinds, as in ResNet-50's whole-net tie (the bf16 artifacts' gradient nodes are Cifar8BbnStepTieB's, on the renderers' bf16 switch at the identity rounding). One device: cifar8wb_bbn has no data-parallel render. It is about the INPUT cotangent chain; the thirty-eight parameter gradients are the node tie's, and that each of them is the loss's derivative in its parameter is Cifar8BbnParamGrad.lean (cifar8Bbn_net_lossGrad).

The running activations, one def each, in forward order. Stage k runs at spatial 2^(5-k)·h, written as the explicit 2 * (…) nest the render's types use.