ResNet-50's T3 §1a TIE — the un-fused, batched whole-net thread #

ResNet34FoldB.lean's op-kind folds (ResNet34PoCB.*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. With T1 and T2 that is ResNet-50's T3, and it makes this the third net whose train-step tie is about the artifact its quoted accuracy comes from.

⭐⭐ The block cotangents are NOT derived here. ResNet50FullBVJP.lean's r50{Id,Proj,Down}B_has_vjp_at 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 — the economy ResNet-34's 4.2a and MobileNetV2's 4.2c both took.

⭐⭐ 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_lambaccdp8x64bce, where the 76.66% comes from — carry BCE-with-logits' three-op chain. So r50_net_tiedB takes g as a hypothesis and the two loss corollaries instantiate it: r50_lossCot_is_smoothedCE_grad and r50_lossCot_is_bce_grad. That is 4b's "the head takes g as a BINDER" made necessary rather than merely tidier.

⭐ The stem tie is three nodes, not four, and the head tie is ResNet-34's. ResNet50RenderB has no convBias flag at all — its zb bakes false — so no conv-bias gradient op is ever emitted and there is nothing to keep "to cover the flag", unlike r34's and MobileNetV2's ties. ResNet34TieB.r34HeadTiedB is generic in {c nCls} and r34HeadCotBlk in the same, so the head is reused verbatim at 2048 channels — as r34HeadB itself was in T1.

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.

Honest residual #

⚠ 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 T2's graph faithfulness has, for the same reason.

⛔ ONE REPLICA. In resnet50in160_lambaccdp8x64bce every gradient node feeds allReduceMeanF — the collective as an AST node since 4d piece 2 (2026-09-07), until then emitted text outside the AST — so every statement here is at the per-replica gradient node and Foundation/DataParallelNode.lean composes it with the replica mean (§4d). 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.

⚠ 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.

Each conjunct is a ResNet34PoCB op-kind 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)). ⛔ 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.