ConvNeXt-T un-fused gradient nodes at the per-example index #
Three per-example lemmas that ConvNeXtFoldGB lifts over the batch: the per-channel layer-scale
γ gradient (layerScaleChGammaGrad_den) and the channel-LN γ/β gradients (chanLnGammaGrad_den,
chanLnBetaGrad_den). Each is den-faithful at the RAW gradient node, the one every optimizer
tail (AdamW, the clipped and weight-decayed variants, SGD) consumes. The fusion is rfl
(StableHLO.lean's *Sgd_eq_grad family), so each proof is its fused peer's in ConvNeXtFold
with the θ − lr· wrapper dropped. Every Adam artifact of this net renders from the batched chain;
its fold is ConvNeXtFoldGB.
Per-channel layer-scale γ GRADIENT denotes the certified gradient. The emitted lsGradCh
reduce dγ_c = Σ_{k : chanIdx k = c} x_k·dy_k IS the certified Jacobian of layerScaleChF
as a function of γ : Vec c, contracted with the cotangent.
Channel-LN γ GRADIENT denotes the certified γ gradient. All 22 spatial sites (1 stem + 18 block + 3 downsample).
Channel-LN β GRADIENT denotes the certified β gradient. The β gradient is the plain row
reduce, so the render uses the same rowDenseBiasGrad op ViT's LN β does.