The MNIST CNN — every parameter gradient node IS the loss's derivative, at real MNIST #

cnn_train_step_tied_certified ties each of the ten SGD updates to the certified per-layer Jacobian contracted with the cotangent the emitted chain threads to it, and leaves open whether that cotangent is the loss gradient below the output. cnn_net_lossGrad closes it: the un-fused *Grad node of each layer, at the chain cotangent, is the gradient of the loss in that parameter (HasGradAt), for any loss L of the logits with gradient g there; cnn_net_lossGrad_CE instantiates it at the softmax cross-entropy the render emits. The fused *Sgd ops are θ − lr· these nodes (SmallParamGrad.convWeightSgd_eq_grad and its peers).

The pool's clause is stated for the parameters, not the image. On real MNIST almost every image has a 2×2 window whose positive maximum sits at two cells, because the two cells read identical input (a constant background patch): the net has no derivative in its input there, and the pool none in its activation. But two such cells are the same function of the conv weights (CnnPoolTwin, implied by identical two-layer receptive fields, cnnPoolTwin_of_convPatchEq2), so along any parameter the pooled ReLU is the gather at a fixed selection (SmallParamGrad.maxPool_relu_eventuallyEq_sel), and the loss IS differentiable in the parameters. CnnLossSmoothAt allows exactly those ties. The probe scripts/probes/mnist_pool_twin_probe.py checks this clause on the MNIST test set.

Which cotangent. At a tied window the pool's backward must pick one cell. The rendered select_and_scatter (select = GE) does: it routes each window's cotangent to the window's first maximal cell, the gather's adjoint. The capstone is stated at any selection σ naming a maximum of every window (cnnChainCotW2Sel, SmallParamGrad.PoolSelDom). The step tie's cnnChainCotW2 reads the pool backward as maxPoolBackDenote, which routes to the first argmax (maxPool2Argmax), so it IS cnnChainCotW2Sel at that selection, at every point (cnnChainCotW2_eq_sel); SmallParamGrad.poolSelDom_argmax discharges the selection clause there.

How. The loss read at the logits is pulled back through the dense head (SmallParamGrad.hasGradAt_dense, SmallParamGrad.hasGradAt_relu), through the pool as the gather at σ (SmallParamGrad.hasGradAt_gatherRelu; at the point itself the pool IS that gather), then through the convs (SmallParamGrad.hasGradAt_conv). Each conv node is the gather model's parameter gradient, moved to the real net by the germ (HasGradAt.congr_of_eventuallyEq).

Hypotheses. Odd kernels (the rendered conv backward is the conv VJP there), and CnnLossSmoothAt: every ReLU off its kink, and every pool window dead or tied only between twins. Scope. One example (the emitted module batch-contracts; den is per-example).