T3 §1 fold for ResNet-34 at TRUE BATCH-NORM — the UN-FUSED gradient ops #

ResNet34Fold.lean makes every parameter output of the per-example SGD train step den-faithful. This is its batched peer, and one thing about it is different in kind.

⛔ r34's batched render emits *GradB, not *SgdB. Every batched ResNet-34 train step — resnet34_sgd_train_step, the Adam family, resnet34in_mom256 and its data-parallel peers — emits the RAW gradient and hands it to an optimizer tail (adamMNextF/adamVNextF, heavy-ball, plain SGD). The fused θ − lr·∂Loss/∂θ op only appears in renders whose optimizer is SGD-inline, which EfficientNet's is and r34's batched one is not. Every den = certified lemma in the repo before this file is stated at the fused form, so none of them applies here.

⭐ That makes this tier better, not worse. A statement about the gradient covers every optimizer variant at once: sgd, mom, momdp64, adam and adamdp128 all consume the same *GradB node, so one lemma per op kind certifies the whole family. ⚠ The bf16 twins do NOT: a bf16 render emits *GradBBf16, its own kind, folded in Foundation/Bf16GradNodes.lean. It is also the form ConvNeXt's psW carve-out already had to take for a different reason (a hand-written SGD wrap).

⭐ And no new mathematics: the *SgdB peers were already proven, and the fusion is rfl. StableHLO.lean's *SgdB_eq_grad family (convWeightSgdB_eq_grad, …) says each fused op IS θ − lr· applied to the un-fused one, all by rfl, and its own docstring says it exists to "unblock a batched resnet34_adam_train_step rendered from Proofs/ — the blocker was the fusion, never Adam." So the eight lemmas below are the per-example VJP bridge under Σ_n with no θ − lr· wrapper, and EfficientNetFold.lean's fused lemmas are them through *SgdB_eq_grad.

⚠ Symmetric padding, not XLA-SAME. The strided lemmas here are about convStridedWeightGradB / convStridedBiasGradB, whose den is flatConvStride2_*; B0's peers are about the convStridedXla* ops and flatConvStride2Xla_*. The two op families have identical types and identical emitted shapes, so nothing but the certificate distinguishes them — and r34 is the PyTorch-origin net, so symmetric is the shipped phase.

Honest residual (the boundary every fold carries) #

• The cotangents are free variables cot — each lemma is ∀ cot, so it holds at the actual backward-chain cotangent without naming it. Pinning each to the emitted residual-backward subgraph is the §1a tie, and is ResNet34StepTieB.lean.