ResNet-34 — every parameter gradient node IS the loss's derivative in that parameter #

r34_net_tiedB says each of the 146 parameter gradient nodes denotes its layer's parameter Jacobian contracted with the cotangent the emitted backward chain threads to it; the *CotIn_eq_vjp lemmas say the block-input cotangents are certified VJP backwards; and r34_lossCot_is_smoothedCE_grad identifies the loss cotangent row by row. r34_net_lossGrad composes them: at the same cotangents, the loss of the WHOLE net with that one parameter varied is differentiable in it and every node is its gradient (HasGradAt), for any loss L of the logits with gradient g there; r34_net_lossGrad_smoothedCE instantiates it at the batched label-smoothed cross-entropy (smoothedBatchLoss) the renders emit.

Scope. One replica, at either precision: every conv weight node is stated on the renderers' switch (convWeightGradBAt bf16 id …, Foundation.GradNodesBAt), so bf16 := true is the bf16 kind resnet34in_momdp64bf16, the book's ImageNet run, emits, read over ℝ at the identity rounding (Bf16Erasure), and bf16 := false the f32 artifacts'. Sync-BN data parallelism is reached by composition: r34_net_syncTiedB says each all-reduced gradient is this net's tied node at N := R·N, which this file's capstone makes the loss's gradient at the global batch.

How. Three layers, each generic where it can be:

• Per node kind (ParamGradNodes): a node is ∂G/∂θ whenever its cotangent is the gradient of G — the loss read at that op's output — there (HasGradAt).
• Per block kind (this file, at variable widths): the loss read at the block output, pulled back one certified stage at a time by ParamGradNodes' pull-backs (hasGradAt_relu, hasGradAt_bnBatchLA, hasGradAt_conv, the skip's hasGradAt_addConst), so each internal activation's gradient is the chain's own cotangent. The stem goes through the argmax gather instead (r34StemGCg_hasGradAt). The bundles r34IdLossTiedB / r34DownLossTiedB / r34StemLossTiedB / r34HeadLossTiedB state all of a block's nodes against Φ, the loss as a function of that block's weight record.
• Per net: the loss read after each block (r34Suf*), its gradient pulled back through the sixteen certified block VJPs (r34IdB_hasGradAt_comp, r34DownB_hasGradAt_comp), and Φ identified with the whole net at updated weights (r34_factor_*) — each a standalone rfl; inside the capstone the same identity is a kernel deep recursion at the literal widths.

Hypotheses. R34PosB (every BN ε > 0), R34LossSmoothAtB (every relu off its kink and every stem-pool window dead, or its maximum at one position up to cells reading identical input patches, at the real activations), and L's gradient g at the logits; the smoothed-CE corollary discharges that from every example's target summing to one and 0 < nCls.

The stem pool's clause is stated for the parameters, not the image. Real batches have stem-pool windows whose positive maximum sits at two positions, because two cells read identical input patches (flat image regions). There the net has no derivative in the image, so the input VJP's R34SmoothAtB rejects them, but the tied cells are the same function of the stem's weights, so the loss IS differentiable in the parameters. R34LossSmoothAtB allows exactly those ties (StemPoolTwinAt at StemConvTwin), and the stem's parameter nodes are proved through the argmax gather they reduce to (r34StemPool_param_germ). At a tied window the render's pool backward (select_and_scatter with a GE select) sends the cotangent to the window's first maximal cell, and so does the denotation maxPool3s2BackB (its reindex reads windowArgmax, the first maximum). Every pool selector (IsMaxPool3s2SelectB) gives the same four stem gradients (r34Stem_select_grads_eq): r34_net_lossGrad_stemSelect states the stem's nodes at any of them. The probe script scripts/probes/stem_pool_smooth_probe.py checks the stem's clauses on real batches.