ResNet-34 at TRUE BATCH-NORM — the whole net's forward and graph (T1-forward, T2)

ResNet34RenderPC.lean (retired 2026-09-19) stated ResNet-34's whole-net ℝ forward and typed graph at per-example BatchNorm (bnPerChannelTensor3, reduce [2,3]). That is the world of resnet34_fwd.mlir and the Imagenette SGD trainer, and every tier built on it is true and correctly paired with those bytes. It is NOT the world of resnet34_sgd_train_step.mlir, resnet34in_mom256_train_step.mlir or any of the Adam/momentum steps, which reduce [0,2,3] — one mu/var per channel across the batch, the one op that couples examples. Those are the artifacts the quoted ImageNet accuracies come from.

This file re-states the ladder at bnBatchLA (= the proven bnBatchTensor4 at the network's left-assoc index). formalization.yaml 4e records the decision and planning/archive/proofs_tier_to_paper_nets.md section 4 the work packages.

What is new here, and what is not

⭐⭐ Nothing about the blocks is new. ResNet34BackB0.lean already carries the batched stages (cbReluB, cbReluStridedB, projStridedB, and projB from EfficientNetRenderPC.lean), their _at VJPs and their backward-graph faithfulness, all at bnBatchLA. What was missing is the level above: a net-level ℝ forward, a net-level forward graph, and the faithfulness tying them. This file is that enumeration.

⚠ Padding is symmetric at every stride-2 site, as ResNet-34's render emits and as the PyTorch-origin convention requires (.convStrided, NOT .convStridedXla — B0's stem is the XLA-SAME one and the two tokens have identical types). scripts/convention_audit.py checks this at the artifact tier and nothing checks it here, so it is stated: stem 7x7/s2, the three downsample conv1s and the three 1x1 projections are all flatConvStride2.

⚠ The stem pool is 3x3/s2 (maxPool3s2Flat), not 2x2. Same type, different function; the render carried .maxPool until 2026-08-04 and nothing failed.

Conventions this net runs at

depth	[3,4,6,3] basic blocks, 64 to 512
BatchNorm	batch (bnBatchLA, reduce [0,2,3], width N*h*w)
activation	relu (one kink), TWO per block — the body's mid-relu and the post-residual one
stride-2 padding	symmetric at all seven sites
stem	7x7/s2 conv-bn-relu, then 3x3/s2 max-pool
head	GAP then dense, generic in the class count
artifacts	resnet34_sgd_train_step, resnet34_adam*, resnet34in_mom*

⭐ The head is generic in nCls, so one statement covers the 10-class Imagenette artifacts and the 1000-class resnet34in ones — the lesson MobileNetV2FullPaperEval.lean and B0's eval twin both paid for.

⚠ N stays a variable throughout. T1 and T2 carry no numerals, so the batch size does not need pinning here; it is pinned only where a Maps envelope turns a width into a rational (T4/T5), and the artifacts' N is the PER-REPLICA batch (64 on the data-parallel runs) because the collectives average gradients and no BatchNorm statistic is all-reduced.

structure Proofs.R34IdW (c : ℕ) : Type

Weights of one identity basic block: two 3x3 convs at width c, BatchNorm after each.

• W₁ : Kernel4 c c 3 3
• b₁ : Vec c
• ε₁ : ℝ
• γ₁ : Vec c
• β₁ : Vec c
• W₂ : Kernel4 c c 3 3
• b₂ : Vec c
• ε₂ : ℝ
• γ₂ : Vec c
• β₂ : Vec c

structure Proofs.R34DownW (ic oc : ℕ) : Type

Weights of one downsample basic block: strided 3x3 (ic -> oc, halves spatial), 3x3, and the 1x1 stride-2 option-B projection on the skip. BatchNorm after each of the three.

• W₁ : Kernel4 oc ic 3 3
• b₁ : Vec oc
• ε₁ : ℝ
• γ₁ : Vec oc
• β₁ : Vec oc
• W₂ : Kernel4 oc oc 3 3
• b₂ : Vec oc
• ε₂ : ℝ
• γ₂ : Vec oc
• β₂ : Vec oc
• Wp : Kernel4 oc ic 1 1
• bp : Vec oc
• εp : ℝ
• γp : Vec oc
• βp : Vec oc

structure Proofs.R34BWeights (nCls : ℕ) : Type

Every ResNet-34 parameter: stem (7x7/s2, 3->64) + the [3,4,6,3] basic blocks + dense head. Generic in the class count.

• sW : Kernel4 64 3 7 7
• sb : Vec 64
• sε : ℝ
• sγ : Vec 64
• sβ : Vec 64
• a0 : R34IdW 64
• a1 : R34IdW 64
• a2 : R34IdW 64
• d2 : R34DownW 64 128
• b0 : R34IdW 128
• b1 : R34IdW 128
• b2 : R34IdW 128
• d3 : R34DownW 128 256
• c0 : R34IdW 256
• c1 : R34IdW 256
• c2 : R34IdW 256
• c3 : R34IdW 256
• c4 : R34IdW 256
• d4 : R34DownW 256 512
• e0 : R34IdW 512
• e1 : R34IdW 512
• Wd : Mat 512 nCls
• bd : Vec nCls

@[reducible]

noncomputable def Proofs.r34IdB (N h w : ℕ) {c : ℕ} (p : R34IdW c) : Vec (N * (c * h * w)) → Vec (N * (c * h * w))

Batched identity basic block relu(F(x) + x), F = projB . cbReluB. The outer relu after the residual add is ResNet's structural difference from MobileNetV2/EfficientNet, whose residual add IS the block output — and it is why every r34 block carries TWO smoothness clauses.

Equations

• Proofs.r34IdB N h w p = Proofs.relu (N * (c * h * w)) ∘ Proofs.residual (Proofs.projB N p.W₂ p.b₂ p.ε₂ p.γ₂ p.β₂ ∘ Proofs.StableHLO.cbReluB N p.W₁ p.b₁ p.ε₁ p.γ₁ p.β₁)

@[reducible]

noncomputable def Proofs.r34DownB (N h w : ℕ) {ic oc : ℕ} (p : R34DownW ic oc) : Vec (N * (ic * (2 * h) * (2 * w))) → Vec (N * (oc * h * w))

Batched downsample basic block relu(F_s(x) + proj_s(x)): body strided-conv1 then conv2, skip a 1x1 stride-2 projection. Both stride-2 sites are SYMMETRIC padding.

Equations

• One or more equations did not get rendered due to their size.

@[reducible]

noncomputable def Proofs.r34StemB (N h w : ℕ) {ic oc : ℕ} (Ws : Kernel4 oc ic 7 7) (bs : Vec oc) (εs : ℝ) (γs βs : Vec oc) : Vec (N * (ic * (2 * (2 * h)) * (2 * (2 * w)))) → Vec (N * (oc * h * w))

Batched stem: 7x7/s2 conv -> bn -> relu, then He et al.'s 3x3/s2 max-pool.

Equations

• Proofs.r34StemB N h w Ws bs εs γs βs = Proofs.StableHLO.batchMap N (Proofs.maxPool3s2Flat oc h w) ∘ Proofs.StableHLO.cbReluStridedB N Ws bs εs γs βs

@[reducible]

noncomputable def Proofs.r34HeadB (N h w : ℕ) {c nCls : ℕ} (Wd : Mat c nCls) (bd : Vec nCls) : Vec (N * (c * h * w)) → Vec (N * nCls)

Batched head: global average pool, then the dense classifier.

Equations

• Proofs.r34HeadB N h w Wd bd = Proofs.StableHLO.batchMap N (Proofs.dense Wd bd) ∘ Proofs.StableHLO.batchMap N (Proofs.globalAvgPoolFlat c h w)

theorem Proofs.r34HeadB_apply (N h w : ℕ) {c nCls : ℕ} (Wd : Mat c nCls) (bd : Vec nCls) (v : Vec (N * (c * h * w))) : r34HeadB N h w Wd bd v = StableHLO.batchMap N (dense Wd bd) (StableHLO.batchMap N (globalAvgPoolFlat c h w) v)

ResNet-34's GAP-and-dense tail, APPLIED.

noncomputable def Proofs.resnet34ForwardB_full (N : ℕ) {nCls : ℕ} (w : R34BWeights nCls) (x : Vec (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) : Vec (N * nCls)

The full batch-BN ResNet-34 forward, N*(3*224*224) -> N*nCls. The batched peer of the retired per-example forward; nested-application form, as efficientnetForwardB_full and mobilenetv2ForwardB_full both are, so the T6 tie can peel it one block at a time.

Equations

• One or more equations did not get rendered due to their size.

def Proofs.StableHLO.r34IdGraphB (p epsStr : String) (N h w : ℕ) {c : ℕ} (pw : R34IdW c) (e : SHlo (N * (c * h * w))) : SHlo (N * (c * h * w))

Identity basic-block graph: relu(addV(bn(conv(relu(bn(conv e)))), e)). The skip reuses the block-input subtree e in both addV operands, as the render does.

Equations

• One or more equations did not get rendered due to their size.

theorem Proofs.StableHLO.r34IdGraphB_faithful (p epsStr : String) (N h w : ℕ) {c : ℕ} (pw : R34IdW c) (e : SHlo (N * (c * h * w))) : den (r34IdGraphB p epsStr N h w pw e) = r34IdB N h w pw (den e)

def Proofs.StableHLO.r34DownGraphB (p epsStr : String) (N h w : ℕ) {ic oc : ℕ} (pw : R34DownW ic oc) (e : SHlo (N * (ic * (2 * h) * (2 * w)))) : SHlo (N * (oc * h * w))

Downsample basic-block graph: relu(addVB(projection, body)) — projection first, matching residualProj proj body. Both branches read the block-input subtree e; both stride-2 convs are .convStrided (symmetric padding).

Equations

• One or more equations did not get rendered due to their size.

theorem Proofs.StableHLO.r34DownGraphB_faithful (p epsStr : String) (N h w : ℕ) {ic oc : ℕ} (pw : R34DownW ic oc) (e : SHlo (N * (ic * (2 * h) * (2 * w)))) : den (r34DownGraphB p epsStr N h w pw e) = r34DownB N h w pw (den e)

def Proofs.StableHLO.r34StemGraphB (epsStr : String) (N h w : ℕ) {ic oc : ℕ} (Ws : Kernel4 oc ic 7 7) (bs : Vec oc) (εs : ℝ) (γs βs : Vec oc) (e : SHlo (N * (ic * (2 * (2 * h)) * (2 * (2 * w))))) : SHlo (N * (oc * h * w))

Stem graph: 7x7/s2 conv -> bn -> relu -> 3x3/s2 max-pool.

Equations

• One or more equations did not get rendered due to their size.

theorem Proofs.StableHLO.r34StemGraphB_faithful (epsStr : String) (N h w : ℕ) {ic oc : ℕ} (Ws : Kernel4 oc ic 7 7) (bs : Vec oc) (εs : ℝ) (γs βs : Vec oc) (e : SHlo (N * (ic * (2 * (2 * h)) * (2 * (2 * w))))) : den (r34StemGraphB epsStr N h w Ws bs εs γs βs e) = r34StemB N h w Ws bs εs γs βs (den e)

def Proofs.StableHLO.r34HeadGraphB (N h w : ℕ) {c nCls : ℕ} (Wd : Mat c nCls) (bd : Vec nCls) (e : SHlo (N * (c * h * w))) : SHlo (N * nCls)

Head graph: GAP then dense.

Equations

• One or more equations did not get rendered due to their size.

theorem Proofs.StableHLO.r34HeadGraphB_faithful (N h w : ℕ) {c nCls : ℕ} (Wd : Mat c nCls) (bd : Vec nCls) (e : SHlo (N * (c * h * w))) : den (r34HeadGraphB N h w Wd bd e) = r34HeadB N h w Wd bd (den e)

def Proofs.StableHLO.resnet34FwdGraphB_full (N : ℕ) (epsStr : String) {nCls : ℕ} (w : R34BWeights nCls) (e : SHlo (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) : SHlo (N * nCls)

The full batch-BN ResNet-34 forward graph. Block prefixes are the render's (s1b0/d2/s2b0/... ), so the typed graph diffs against resnet34_fwd's batched peers name for name.

Equations

• One or more equations did not get rendered due to their size.

theorem Proofs.StableHLO.resnet34FwdGraphB_full_faithful (N : ℕ) (epsStr : String) {nCls : ℕ} (w : R34BWeights nCls) (e : SHlo (N * (3 * (2 * (2 * 56)) * (2 * (2 * 56))))) : den (resnet34FwdGraphB_full N epsStr w e) = resnet34ForwardB_full N w (den e)

⭐ T2 for ResNet-34 at batch BN: the typed graph denotes the whole-net forward. One rw per block over the eighteen per-kind faithfulness lemmas.