ResNet-50's step TIE — the un-fused, batched whole-net thread #

GradNodesB's op-kind folds (GradNodeB.*GradB_den) make every parameter GRADIENT node of ResNet-50's batched train step den-faithful for an ARBITRARY cotangent. This removes the "arbitrary": each is pinned to the one the emitted backward chain delivers, so the whole train step is den-composed forward → loss → backward with no free activation and no symbolic cotangent.

The block cotangents are NOT derived here. ResNet50FullBVJP.lean's r50{Id,Proj,Down}BHasVJPAt ARE the certified block backwards, and ResNet50BackB0.lean's r50{Bottleneck,ProjBlock,DownBlock}BackBatchedGraph_faithful family already proves the emitted backward subgraph denotes exactly them. The three *CotIn_eq_vjp lemmas below are that statement in this file's vocabulary, so the cross-block chain is a composition of certified VJPs rather than a re-derivation — as in ResNet34StepTieB and MobileNetV2's step tie.

THE LOSS COTANGENT IS A BINDER, and for this net it had to be. ResNet-34's and MobileNetV2's capstones compute g internally from smoothedLossCotGraph. ResNet-50 ships BOTH losses: bce := false artifacts carry the six-op label-smoothed softmax chain and bce := true ones — including resnet50in160_lambaccdp8x64wxclipbce — carry BCE-with-logits' three-op chain. So r50_net_tiedB takes g as a binder and the two loss corollaries instantiate it: r50_lossCot_is_smoothedCE_grad and r50_lossCot_is_bce_grad.

The block ties carry no conv-bias conjunct, and the stem and head ties are ResNet-34's. ResNet50RenderB has no convBias flag at all — its zb bakes false — so no conv-bias gradient op is emitted, and the bottleneck ties have no bias conjunct. The stem tie is ResNet-34's ResNet34TieB.r34StemTiedB, whose conv-bias conjunct is true at bias = 0 but not exercised, so the stem contributes 3 exercised slots of 4. ResNet34TieB.r34HeadTiedB is generic in {c nCls} and r34HeadCotBlk in the same, so the head is reused verbatim at 2048 channels — as r34HeadB itself is in resnet50ForwardBFull.

The emitted chain, node for node #

ResNet50RenderB.bnkIdBackGradB, from the block-output cotangent dyOut:

%da  = selectPosB(a)     %dn3 = bnBatchBack(g3, c3)   %dc3 = convBackBatched(W3)
%dr2 = selectPosB(n2)    %dn2 = bnBatchBack(g2, c2)   %dc2 = convBackBatched(W2)
%dr1 = selectPosB(n1)    %dn1 = bnBatchBack(g1, c1)   %dc1 = convBackBatched(W1)
%dx  = addVB(%dc1, %da)

and the nine parameter nodes read W1 ← %dn1, g1/bt1 ← %dr1, W2 ← %dn2, g2/bt2 ← %dr2, W3 ← %dn3, g3/bt3 ← %da. Off by one on any of those and the gradient is silently wrong; the render's own comment records the same trap on the stochastic-depth cotangent.

The projection blocks add %dnp = bnBatchBack(gp, cp, %da) and %dcp = convBack(Wp), and their fan-in is addVB(%dc1, %dcp) — both branches nontrivial.

Scope #

One add_comm per projection form. The render emits addVB(body, projection) where residualProj proj body adds proj + body, so r50{Proj,Down}CotIn_eq_vjp carry a commutation. The identity block needs none. Same seam resnet50FwdGraphBFull_faithful has, for the same reason.

ONE REPLICA. Every statement here is at one replica's gradient node. Every ResNet-50 data-parallel render (resnet50in160_lambaccdp8x64wxclipbce among them) synchronises BatchNorm; its all-reduced gradients are ResNet50SyncStepTieB's r50_net_syncTiedB: this file's node at N := R·N. The 8× accumulation sits between the gradient and the optimizer as momVNextF at (μ := akeep), and the LAMB tail is lamb_triple_faithful — both certified, neither part of this file.

Precision is a flag on the statement. The ImageNet runs the book reports train from resnet50in_momdp64bf16 and resnet50in160_lambaccdp4x128wxclipbcebf16, whose conv weight gradients are the bf16 kinds (convWeightGradBBf16, …). Every conv weight node below is stated on the renderers' switch — ConvWTiedBAt bf16 / ConvStridedWTiedBAt bf16 (Foundation.GradNodesBAt): false the f32 node, true the bf16 one — and r50_net_tiedB takes bf16, so it reaches those runs' gradient nodes read over ℝ exactly as it reads the f32 ones (Bf16Erasure, as ResNet34StepTieB). BatchNorm and dense nodes carry no flag; the data-parallel capstone is ResNet50SyncStepTieB at the same flag.

No smoothness hypothesis in the capstone, exactly as r34's and mnv2's: the folds are ∀ cot statements instantiated at explicitly constructed cotangents. The relu-kink and positivity conditions enter ONLY in the three *CotIn_eq_vjp lemmas, which say those cotangents ARE the certified whole-net backward. N and q are both binders.

References #

• You et al. 2020, Large Batch Optimization for Deep Learning: Training BERT in 76 minutes (LAMB). https://arxiv.org/abs/1904.00962
• Wightman, Touvron, Jégou 2021, ResNet strikes back (RSB A3: BCE, LAMB recipe). https://arxiv.org/abs/2110.00476

Each conjunct is a GradNodeB op-kind fold instantiated at the cotangent the render's chain delivers, so nothing here is a new proof: the bundles are GradNodesB's folds with the freedom removed. reassocB bridges the conv/relu index N·(c·h·w) to the BatchNorm parameter ops' N·(c·(h·w)). There are NO conv-bias conjuncts: ResNet50RenderB has no convBias flag, so those ops are never emitted and every slot here is exercised by the artifact.