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

ResNet34FoldB.lean (4.1e) 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.

It replaced the per-example ResNet34TiePoC.lean (deleted 2026-09-08: no committed artifact exercised it once resnet34_train_step.mlir was retired), and four things about it are different in kind.

⭐⭐ The block cotangents are NOT derived here. The per-example close (ResNet34ChainClose.lean, deleted 2026-09-08) spelled per-block cotangent vectors out by hand, because no whole-block VJP existed when it was written. 4.1d's r34IdB_has_vjp_at / r34DownB_has_vjp_at 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. T3 carries no numerals, so nothing here pins the batch.

⛔ The all-reduce, since 4d piece 2 (2026-09-07). In resnet34in_momdp64 each *GradB node feeds allReduceMeanF — the collective as an AST node whose den is the replica MEAN of the per-replica gradient nodes; until then emitGradAllReduce, emitted text and a declared carve-out outside the SHlo AST. Every statement below is at the PER-REPLICA gradient node; DataParallelNode.lean composes it with the mean and the tail. For the sync-BN data-parallel render (2026-09-21) ResNet34SyncStepTieB.lean is the whole step: its r34_net_syncTiedB says each all-reduced gradient IS this file's node at N := R·N.

⛔ The parameter census is 110, not the 146 the per-example tie named #

resnet34TrainStepFaithfulV and ResNet34RenderB both 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 per-example resnet34_train_step.mlir carried the same 110 and was retired the same day by 4c leg 1.) 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 ResNet34FoldB's ∀ cot fold instantiated at the cotangent the render's chain delivers, so nothing here is a new proof: the bundles are the §1 fold 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.