ResNet-34's step TIE at TRUE BATCH-NORM — the un-fused, batched whole-net thread #

GradNodesB makes every parameter GRADIENT node of the batched ResNet-34 train step den-faithful for an arbitrary cotangent. This file removes the "arbitrary": each cotangent 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. r34IdBHasVJPAt / r34DownBHasVJPAt ARE the certified block backwards, so a block's input cotangent is a .backward application — and r34{BasicBlock,DownBlock}BackBatchedGraph_faithful already proves the emitted backward subgraph denotes exactly it. r34IdCotIn_eq_vjp and r34DownCotIn_eq_vjp below are that statement in the vocabulary this file threads, and they are what make the cross-block chain a composition of certified VJPs rather than a re-derivation.

The loss cotangent is the LABEL-SMOOTHED one, at a general target. ResNet34RenderB composes the head cotangent from six kit ops — softmaxRow → subB → scaleB → addVB → shiftB → divConstB, α baked at 0.1 and the ls0 variants at 0 — and the target arrives as the graph input %onehot, which under mixup or cutmix is a soft vector drawn on the host. Foundation/SmoothedLossCot.lean is that cotangent's lemma; the head fold below is stated at it, not at softmax − oneHot.

N is a binder. The capstone takes (N : Nat), exactly as efficientnet_net_tied does; the artifacts at 32 (resnet34_sgd/adam_train_step) or 64 (resnet34in_momdp64) are instances. The batch size is never pinned (the 224-px resolution and the 64…512 widths are literals).

The all-reduce. Every statement below is at one replica's gradient node. Every ResNet-34 data-parallel render (resnet34in_momdp64 among them) synchronises BatchNorm; its all-reduced gradients are ResNet34SyncStepTieB's r34_net_syncTiedB: this file's node at N := R·N.

Precision is a flag on the statement. The ImageNet run the book reports trains from resnet34in_momdp64bf16, whose conv weight gradients are the bf16 kinds (convWeightGradBBf16, …; Foundation.Bf16GradNodes). Every conv weight node below is stated on the renderers' switch — ConvWTiedBAt bf16 / ConvStridedWTiedBAt bf16 (Foundation.GradNodesBAt): bf16 := false is the f32 node, bf16 := true the bf16 one — and the capstone r34_net_tiedB takes bf16, so it reaches the bf16 artifacts' gradient nodes read over ℝ exactly as it reads the f32 ones (Bf16Erasure: at the identity rounding the bf16 kind denotes what its f32 peer does). BatchNorm, bias and dense nodes carry no flag because no render switches them. What the bf16 weight-gradient kinds do under sharding is DataParallel.SyncBf16; the data-parallel capstone is ResNet34SyncStepTieB at the same flag.

The parameter census is 110, not 146 #

ResNet34RenderB's writers default to convBias := false: the conv biases are gone from the signature (BatchNorm subsumes them, and He et al.'s .convBn has none), bound instead to the zero constants zeroBiasPrelude emits. So resnet34_sgd_train_step.mlir carries 110 SGD-updated tensors — stem 3 + 13 identity blocks × 6 + 3 downsample blocks × 9 + dense 2 — and 146 is the census at convBias := true. The bias conjuncts below are kept (they are one delegation each and they cover the flag), and they are about ops the committed artifacts do not emit. Nothing about this weakens a theorem: every fold is ∀-quantified over op instances, and bias = 0 is one of them.

Conventions, stated because nothing here checks them #

ResNet34RenderB.idBackGradB, node for node, from the block-output cotangent dyOut:

%da  = selectPosB(a)   %dn2 = bnBatchBack(g2, c2)   %dc2 = convBackBatched(W2)
%dr1 = selectPosB(n1)  %dn1 = bnBatchBack(g1, c1)   %dc1 = convBackBatched(W1)
%dx  = addVB(%dc1, %da)

and the eight parameter nodes read W1,b1 ← %dn1, g1,bt1 ← %dr1, W2,b2 ← %dn2, g2,bt2 ← %da. The four defs below are those four cotangents.

ResNet34RenderB.downBackGradB adds one branch to the identity block's chain:

%da  = selectPosB(a)   %dn2 = bnBatchBack(g2,c2)  %dc2 = convBackBatched(W2)
%dr1 = selectPosB(n1)  %dn1 = bnBatchBack(g1,c1)  %dc1 = convStridedBackBatched(W1)
%dnp = bnBatchBack(gp,cp)                          %dcp = convStridedBackBatched(Wp)
%dx  = addVB(%dc1, %dcp)

so bnₚ's γ/β read the SAME %da that bn₂'s do — both feed the one addVB — and the projection's Wp/bp read %dnp.

ResNet34RenderB, after the sixteen block backwards:

%dmp = maxPool3s2BackB(str)   %dsr = selectPosB(stn)   %dsn = bnBatchBack(sg, stc)

with sW,sb ← %dsn and sg,sbt ← %dsr.

Each conjunct is GradNodesB's ∀ cot 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)).

The two conv-BIAS conjuncts in each block are about conv{,Strided}BiasGradB, which the committed artifacts do NOT emit — both renders run convBias := false and bind the bias operand to zeroBiasPrelude's zero constant. They are kept because they cost one delegation each and they cover the flag.