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

r50_net_tiedB says each of the 161 parameter gradient nodes denotes its layer's parameter Jacobian contracted with the cotangent the emitted backward chain threads to it, from a loss cotangent g it takes as a binder; the r50*CotIn_eq_vjp lemmas say the block-input cotangents are certified VJP backwards. r50_net_lossGrad composes them: for any loss L of the logits whose gradient at the net's output is g, every node is ∂L/∂θ of the WHOLE net with that one parameter varied. The two losses the artifacts ship discharge hL:

• r50_net_lossGrad_smoothedCE — the bce := false artifacts: L = smoothedBatchLoss, g the six-op label-smoothed chain (smoothedBatchLoss_grad).
• r50_net_lossGrad_bce — the bce := true artifacts, resnet50in160_lambaccdp8x64wxclipbce among them: L = bceBatchLoss, the mean over B×K, g the three-op chain (bceBatchLoss_grad).

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 resnet50in_momdp64bf16 and resnet50in160_lambaccdp4x128wxclipbcebf16, the book's ImageNet runs, emit, read over ℝ at the identity rounding (Bf16Erasure), and bf16 := false the f32 artifacts'. The drop-path forwards (*drop*) are outside this statement. Sync-BN data parallelism is reached by composition: r50_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. ResNet34ParamGrad's three layers, with R34's stem and head bundles reused verbatim (the stem and head ARE R34's functions at R50's widths):

• Per block kind (at variable widths): the loss read at an identity / stride-1 projection / strided projection bottleneck's output, pulled back one certified stage at a time by ParamGradNodes' pull-backs, so each internal activation's gradient is the chain's own cotangent. The bundles r50IdLossTiedB / r50ProjLossTiedB / r50DownLossTiedB state the block's nodes against Φ, the loss as a function of the block's weight record — the same slots as r50IdTiedB / r50ProjTiedB / r50DownTiedB, no conv bias (ResNet50RenderB emits none).
• Per net: the loss read after each block (r50Suf*), its gradient pulled back through the sixteen certified bottleneck VJPs, and Φ identified with the whole net at updated weights (r50_factor_*), each a standalone theorem.

Hypotheses. R50PosB (every BN ε > 0), R50LossSmoothAtB (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); for the smoothed loss also every example's target summing to one and 0 < nCls. The BCE corollary takes no hypothesis on the target.

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 R50SmoothAtB rejects them, but the tied cells are the same function of the stem's weights, so the loss IS differentiable in the parameters. R50LossSmoothAtB 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): r50_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.