r34 Item A — the PER-CHANNEL-BN ResNet-34 forward graph (matches the render)

The ResNet-34 peer of MobileNetV2RenderPC.lean. StableHLO.lean's resnetFwdGraph is a representative (stem + 1 identity + 1 projection block + GAP + dense) using scalar bnF; the operational render (tests/TestResnet34Train.lean) emits per-channel BN, the full 16-block [3,4,6,3] net, a 7×7 strided stem and a maxpool. This file is the per-channel twin matching the render:

• per-channel building blocks cbrStridedPC (7×7 strided stem conv→bn→relu), rblkPC (identity basic block relu(F(x)+x)), rblkPStridedPC (downsample basic block relu(F_s(x)+proj_s(x)), with the 1×1 strided option-B projection skip) — per-channel bnPerChannelTensor3 mirrors of cbr/rblk/ rblkP (CNN.lean).
• per-block typed SHlo graphs idBlockGraphPC/downBlockGraphPC + their _faithful lemmas (den (block graph) = block forward (den input)), via bnPerChannelF_faithful/reluF_faithful/ flatConv(Strided)F_faithful/den_addV. The residual skip reuses the block-input subtree in both addV operands (tree-safe), as in resnetFwdGraph.

Part 2 (below) chains these into the full resnet34FwdGraphFullPC + resnet34Forward_full_pc + faithfulness at the render dims (3×224² → 7×7×512). Prerequisite for the structured render (Item B). No new tokens. 3-axiom clean.

@[reducible]

noncomputable def Proofs.cbrStridedPC {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (b : Vec oc) (ε : ℝ) (γ β : Vec oc) : Vec (ic * (2 * h) * (2 * w)) → Vec (oc * h * w)

7×7 strided stem conv → bn → relu, per-channel BN.

Equations

• Proofs.cbrStridedPC W b ε γ β = Proofs.relu (oc * h * w) ∘ Proofs.bnPerChannelTensor3 oc h w ε γ β ∘ Proofs.flatConvStride2 W b

@[reducible]

noncomputable def Proofs.rblkPC {c h w kH₁ kW₁ kH₂ kW₂ : ℕ} (W₁ : Kernel4 c c kH₁ kW₁) (b₁ : Vec c) (ε₁ : ℝ) (γ₁ β₁ : Vec c) (W₂ : Kernel4 c c kH₂ kW₂) (b₂ : Vec c) (ε₂ : ℝ) (γ₂ β₂ : Vec c) : Vec (c * h * w) → Vec (c * h * w)

Identity basic block relu(F(x) + x), F = (bn∘conv) ∘ (relu∘bn∘conv), per-channel BN.

Equations

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

@[reducible]

noncomputable def Proofs.rblkPStridedPC {ic oc h w kH₁ kW₁ kH₂ kW₂ kHp kWp : ℕ} (W₁ : Kernel4 oc ic kH₁ kW₁) (b₁ : Vec oc) (ε₁ : ℝ) (γ₁ β₁ : Vec oc) (W₂ : Kernel4 oc oc kH₂ kW₂) (b₂ : Vec oc) (ε₂ : ℝ) (γ₂ β₂ : Vec oc) (Wp : Kernel4 oc ic kHp kWp) (bp : Vec oc) (εp : ℝ) (γp βp : Vec oc) : Vec (ic * (2 * h) * (2 * w)) → Vec (oc * h * w)

Downsample basic block relu(F_s(x) + proj_s(x)): body bn∘conv ∘ relu∘bn∘conv_strided (ic→oc, halves spatial), projection bn∘conv_strided (1×1 stride-2 option-B skip). Per-channel BN.

Equations

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

@[reducible]

noncomputable def Proofs.idFwd {c h w : ℕ} (ε : ℝ) (W₁ : Kernel4 c c 3 3) (b₁ γ₁ β₁ : Vec c) (W₂ : Kernel4 c c 3 3) (b₂ γ₂ β₂ : Vec c) : Vec (c * h * w) → Vec (c * h * w)

Identity-block ℝ-forward at shared ε (the partial application rblkPC takes).

Equations

• Proofs.idFwd ε W₁ b₁ γ₁ β₁ W₂ b₂ γ₂ β₂ = Proofs.rblkPC W₁ b₁ ε γ₁ β₁ W₂ b₂ ε γ₂ β₂

@[reducible]

noncomputable def Proofs.downFwd {ic oc h w kHp kWp : ℕ} (ε : ℝ) (W₁ : Kernel4 oc ic 3 3) (b₁ γ₁ β₁ : Vec oc) (W₂ : Kernel4 oc oc 3 3) (b₂ γ₂ β₂ : Vec oc) (Wp : Kernel4 oc ic kHp kWp) (bp γp βp : Vec oc) : Vec (ic * (2 * h) * (2 * w)) → Vec (oc * h * w)

Downsample-block ℝ-forward at shared ε.

kHp kWp is the projection kernel and is generic; the body convs stay 3×3, which is what He et al. specify. It was pinned at 3×3 here until 2026-07-30, when §2k found the render's projection is a 3×3 where the paper's option-B shortcut is 1×1 — the whole point of the binder is that switching the two is an argument, not a proof edit.

Equations

• Proofs.downFwd ε W₁ b₁ γ₁ β₁ W₂ b₂ γ₂ β₂ Wp bp γp βp = Proofs.rblkPStridedPC W₁ b₁ ε γ₁ β₁ W₂ b₂ ε γ₂ β₂ Wp bp ε γp βp

noncomputable def Proofs.resnet34Forward_full_pc (ε : ℝ) (Ws : Kernel4 64 3 7 7) (bs γs βs : Vec 64) (a0W1 : Kernel4 64 64 3 3) (a0b1 a0g1 a0t1 : Vec 64) (a0W2 : Kernel4 64 64 3 3) (a0b2 a0g2 a0t2 : Vec 64) (a1W1 : Kernel4 64 64 3 3) (a1b1 a1g1 a1t1 : Vec 64) (a1W2 : Kernel4 64 64 3 3) (a1b2 a1g2 a1t2 : Vec 64) (a2W1 : Kernel4 64 64 3 3) (a2b1 a2g1 a2t1 : Vec 64) (a2W2 : Kernel4 64 64 3 3) (a2b2 a2g2 a2t2 : Vec 64) (d2W1 : Kernel4 128 64 3 3) (d2b1 d2g1 d2t1 : Vec 128) (d2W2 : Kernel4 128 128 3 3) (d2b2 d2g2 d2t2 : Vec 128) (d2Wp : Kernel4 128 64 1 1) (d2bp d2gp d2tp : Vec 128) (b0W1 : Kernel4 128 128 3 3) (b0b1 b0g1 b0t1 : Vec 128) (b0W2 : Kernel4 128 128 3 3) (b0b2 b0g2 b0t2 : Vec 128) (b1W1 : Kernel4 128 128 3 3) (b1b1 b1g1 b1t1 : Vec 128) (b1W2 : Kernel4 128 128 3 3) (b1b2 b1g2 b1t2 : Vec 128) (b2W1 : Kernel4 128 128 3 3) (b2b1 b2g1 b2t1 : Vec 128) (b2W2 : Kernel4 128 128 3 3) (b2b2 b2g2 b2t2 : Vec 128) (d3W1 : Kernel4 256 128 3 3) (d3b1 d3g1 d3t1 : Vec 256) (d3W2 : Kernel4 256 256 3 3) (d3b2 d3g2 d3t2 : Vec 256) (d3Wp : Kernel4 256 128 1 1) (d3bp d3gp d3tp : Vec 256) (c0W1 : Kernel4 256 256 3 3) (c0b1 c0g1 c0t1 : Vec 256) (c0W2 : Kernel4 256 256 3 3) (c0b2 c0g2 c0t2 : Vec 256) (c1W1 : Kernel4 256 256 3 3) (c1b1 c1g1 c1t1 : Vec 256) (c1W2 : Kernel4 256 256 3 3) (c1b2 c1g2 c1t2 : Vec 256) (c2W1 : Kernel4 256 256 3 3) (c2b1 c2g1 c2t1 : Vec 256) (c2W2 : Kernel4 256 256 3 3) (c2b2 c2g2 c2t2 : Vec 256) (c3W1 : Kernel4 256 256 3 3) (c3b1 c3g1 c3t1 : Vec 256) (c3W2 : Kernel4 256 256 3 3) (c3b2 c3g2 c3t2 : Vec 256) (c4W1 : Kernel4 256 256 3 3) (c4b1 c4g1 c4t1 : Vec 256) (c4W2 : Kernel4 256 256 3 3) (c4b2 c4g2 c4t2 : Vec 256) (d4W1 : Kernel4 512 256 3 3) (d4b1 d4g1 d4t1 : Vec 512) (d4W2 : Kernel4 512 512 3 3) (d4b2 d4g2 d4t2 : Vec 512) (d4Wp : Kernel4 512 256 1 1) (d4bp d4gp d4tp : Vec 512) (e0W1 : Kernel4 512 512 3 3) (e0b1 e0g1 e0t1 : Vec 512) (e0W2 : Kernel4 512 512 3 3) (e0b2 e0g2 e0t2 : Vec 512) (e1W1 : Kernel4 512 512 3 3) (e1b1 e1g1 e1t1 : Vec 512) (e1W2 : Kernel4 512 512 3 3) (e1b2 e1g2 e1t2 : Vec 512) (Wd : Mat 512 10) (bd : Vec 10) : Vec (3 * 224 * 224) → Vec 10

The full per-channel ResNet-34 forward (render dims 3×224² → 7×7×512).

Equations

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

def Proofs.StableHLO.idBlockGraphPC (p epsStr : String) {c h w : ℕ} (W₁ : Kernel4 c c 3 3) (b₁ : Vec c) (ε₁ : ℝ) (γ₁ β₁ : Vec c) (W₂ : Kernel4 c c 3 3) (b₂ : Vec c) (ε₂ : ℝ) (γ₂ β₂ : Vec c) (e : SHlo (c * h * w)) : SHlo (c * h * w)

Identity-block forward graph: relu(addV(bn∘conv∘relu∘bn∘conv, skip)); the skip reuses the block-input subtree e.

Equations

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

def Proofs.StableHLO.downBlockGraphPC (p epsStr : String) {ic oc h w kHp kWp : ℕ} (W₁ : Kernel4 oc ic 3 3) (b₁ : Vec oc) (ε₁ : ℝ) (γ₁ β₁ : Vec oc) (W₂ : Kernel4 oc oc 3 3) (b₂ : Vec oc) (ε₂ : ℝ) (γ₂ β₂ : Vec oc) (Wp : Kernel4 oc ic kHp kWp) (bp : Vec oc) (εp : ℝ) (γp βp : Vec oc) (e : SHlo (ic * (2 * h) * (2 * w))) : SHlo (oc * h * w)

Downsample-block forward graph: relu(addV(body, projection)), body strided conv1 + conv2, projection a kHp×kWp strided conv; both read the block-input subtree e.

Equations

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

theorem Proofs.StableHLO.idBlockGraphPC_faithful (p epsStr : String) {c h w : ℕ} (W₁ : Kernel4 c c 3 3) (b₁ : Vec c) (ε₁ : ℝ) (γ₁ β₁ : Vec c) (W₂ : Kernel4 c c 3 3) (b₂ : Vec c) (ε₂ : ℝ) (γ₂ β₂ : Vec c) (e : SHlo (c * h * w)) : den (idBlockGraphPC p epsStr W₁ b₁ ε₁ γ₁ β₁ W₂ b₂ ε₂ γ₂ β₂ e) = rblkPC W₁ b₁ ε₁ γ₁ β₁ W₂ b₂ ε₂ γ₂ β₂ (den e)

Identity block faithfulness. den (idBlockGraphPC … e) = rblkPC … (den e).

theorem Proofs.StableHLO.downBlockGraphPC_faithful (p epsStr : String) {ic oc h w kHp kWp : ℕ} (W₁ : Kernel4 oc ic 3 3) (b₁ : Vec oc) (ε₁ : ℝ) (γ₁ β₁ : Vec oc) (W₂ : Kernel4 oc oc 3 3) (b₂ : Vec oc) (ε₂ : ℝ) (γ₂ β₂ : Vec oc) (Wp : Kernel4 oc ic kHp kWp) (bp : Vec oc) (εp : ℝ) (γp βp : Vec oc) (e : SHlo (ic * (2 * h) * (2 * w))) : den (downBlockGraphPC p epsStr W₁ b₁ ε₁ γ₁ β₁ W₂ b₂ ε₂ γ₂ β₂ Wp bp εp γp βp e) = rblkPStridedPC W₁ b₁ ε₁ γ₁ β₁ W₂ b₂ ε₂ γ₂ β₂ Wp bp εp γp βp (den e)

Downsample block faithfulness. den (downBlockGraphPC … e) = rblkPStridedPC … (den e).

def Proofs.StableHLO.resnet34FwdGraphFullPC (epsStr : String) (ε : ℝ) (Ws : Kernel4 64 3 7 7) (bs γs βs : Vec 64) (a0W1 : Kernel4 64 64 3 3) (a0b1 a0g1 a0t1 : Vec 64) (a0W2 : Kernel4 64 64 3 3) (a0b2 a0g2 a0t2 : Vec 64) (a1W1 : Kernel4 64 64 3 3) (a1b1 a1g1 a1t1 : Vec 64) (a1W2 : Kernel4 64 64 3 3) (a1b2 a1g2 a1t2 : Vec 64) (a2W1 : Kernel4 64 64 3 3) (a2b1 a2g1 a2t1 : Vec 64) (a2W2 : Kernel4 64 64 3 3) (a2b2 a2g2 a2t2 : Vec 64) (d2W1 : Kernel4 128 64 3 3) (d2b1 d2g1 d2t1 : Vec 128) (d2W2 : Kernel4 128 128 3 3) (d2b2 d2g2 d2t2 : Vec 128) (d2Wp : Kernel4 128 64 1 1) (d2bp d2gp d2tp : Vec 128) (b0W1 : Kernel4 128 128 3 3) (b0b1 b0g1 b0t1 : Vec 128) (b0W2 : Kernel4 128 128 3 3) (b0b2 b0g2 b0t2 : Vec 128) (b1W1 : Kernel4 128 128 3 3) (b1b1 b1g1 b1t1 : Vec 128) (b1W2 : Kernel4 128 128 3 3) (b1b2 b1g2 b1t2 : Vec 128) (b2W1 : Kernel4 128 128 3 3) (b2b1 b2g1 b2t1 : Vec 128) (b2W2 : Kernel4 128 128 3 3) (b2b2 b2g2 b2t2 : Vec 128) (d3W1 : Kernel4 256 128 3 3) (d3b1 d3g1 d3t1 : Vec 256) (d3W2 : Kernel4 256 256 3 3) (d3b2 d3g2 d3t2 : Vec 256) (d3Wp : Kernel4 256 128 1 1) (d3bp d3gp d3tp : Vec 256) (c0W1 : Kernel4 256 256 3 3) (c0b1 c0g1 c0t1 : Vec 256) (c0W2 : Kernel4 256 256 3 3) (c0b2 c0g2 c0t2 : Vec 256) (c1W1 : Kernel4 256 256 3 3) (c1b1 c1g1 c1t1 : Vec 256) (c1W2 : Kernel4 256 256 3 3) (c1b2 c1g2 c1t2 : Vec 256) (c2W1 : Kernel4 256 256 3 3) (c2b1 c2g1 c2t1 : Vec 256) (c2W2 : Kernel4 256 256 3 3) (c2b2 c2g2 c2t2 : Vec 256) (c3W1 : Kernel4 256 256 3 3) (c3b1 c3g1 c3t1 : Vec 256) (c3W2 : Kernel4 256 256 3 3) (c3b2 c3g2 c3t2 : Vec 256) (c4W1 : Kernel4 256 256 3 3) (c4b1 c4g1 c4t1 : Vec 256) (c4W2 : Kernel4 256 256 3 3) (c4b2 c4g2 c4t2 : Vec 256) (d4W1 : Kernel4 512 256 3 3) (d4b1 d4g1 d4t1 : Vec 512) (d4W2 : Kernel4 512 512 3 3) (d4b2 d4g2 d4t2 : Vec 512) (d4Wp : Kernel4 512 256 1 1) (d4bp d4gp d4tp : Vec 512) (e0W1 : Kernel4 512 512 3 3) (e0b1 e0g1 e0t1 : Vec 512) (e0W2 : Kernel4 512 512 3 3) (e0b2 e0g2 e0t2 : Vec 512) (e1W1 : Kernel4 512 512 3 3) (e1b1 e1g1 e1t1 : Vec 512) (e1W2 : Kernel4 512 512 3 3) (e1b2 e1g2 e1t2 : Vec 512) (Wd : Mat 512 10) (bd : Vec 10) (x : Vec (3 * 224 * 224)) : SHlo 10

Whole per-channel-BN ResNet-34 forward graph at the render dims (3×224² → 7×7×512): 7×7 strided stem (flatConvStridedF) → bn → relu → maxPoolF → [3,4,6,3] basic blocks (each via idBlockGraphPC/downBlockGraphPC) → GAP → dense. Per-channel BN throughout, matching the render. The per-channel twin of resnetFwdGraph, at full depth.

Equations

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

theorem Proofs.StableHLO.resnet34FwdGraphFullPC_faithful (epsStr : String) (ε : ℝ) (Ws : Kernel4 64 3 7 7) (bs γs βs : Vec 64) (a0W1 : Kernel4 64 64 3 3) (a0b1 a0g1 a0t1 : Vec 64) (a0W2 : Kernel4 64 64 3 3) (a0b2 a0g2 a0t2 : Vec 64) (a1W1 : Kernel4 64 64 3 3) (a1b1 a1g1 a1t1 : Vec 64) (a1W2 : Kernel4 64 64 3 3) (a1b2 a1g2 a1t2 : Vec 64) (a2W1 : Kernel4 64 64 3 3) (a2b1 a2g1 a2t1 : Vec 64) (a2W2 : Kernel4 64 64 3 3) (a2b2 a2g2 a2t2 : Vec 64) (d2W1 : Kernel4 128 64 3 3) (d2b1 d2g1 d2t1 : Vec 128) (d2W2 : Kernel4 128 128 3 3) (d2b2 d2g2 d2t2 : Vec 128) (d2Wp : Kernel4 128 64 1 1) (d2bp d2gp d2tp : Vec 128) (b0W1 : Kernel4 128 128 3 3) (b0b1 b0g1 b0t1 : Vec 128) (b0W2 : Kernel4 128 128 3 3) (b0b2 b0g2 b0t2 : Vec 128) (b1W1 : Kernel4 128 128 3 3) (b1b1 b1g1 b1t1 : Vec 128) (b1W2 : Kernel4 128 128 3 3) (b1b2 b1g2 b1t2 : Vec 128) (b2W1 : Kernel4 128 128 3 3) (b2b1 b2g1 b2t1 : Vec 128) (b2W2 : Kernel4 128 128 3 3) (b2b2 b2g2 b2t2 : Vec 128) (d3W1 : Kernel4 256 128 3 3) (d3b1 d3g1 d3t1 : Vec 256) (d3W2 : Kernel4 256 256 3 3) (d3b2 d3g2 d3t2 : Vec 256) (d3Wp : Kernel4 256 128 1 1) (d3bp d3gp d3tp : Vec 256) (c0W1 : Kernel4 256 256 3 3) (c0b1 c0g1 c0t1 : Vec 256) (c0W2 : Kernel4 256 256 3 3) (c0b2 c0g2 c0t2 : Vec 256) (c1W1 : Kernel4 256 256 3 3) (c1b1 c1g1 c1t1 : Vec 256) (c1W2 : Kernel4 256 256 3 3) (c1b2 c1g2 c1t2 : Vec 256) (c2W1 : Kernel4 256 256 3 3) (c2b1 c2g1 c2t1 : Vec 256) (c2W2 : Kernel4 256 256 3 3) (c2b2 c2g2 c2t2 : Vec 256) (c3W1 : Kernel4 256 256 3 3) (c3b1 c3g1 c3t1 : Vec 256) (c3W2 : Kernel4 256 256 3 3) (c3b2 c3g2 c3t2 : Vec 256) (c4W1 : Kernel4 256 256 3 3) (c4b1 c4g1 c4t1 : Vec 256) (c4W2 : Kernel4 256 256 3 3) (c4b2 c4g2 c4t2 : Vec 256) (d4W1 : Kernel4 512 256 3 3) (d4b1 d4g1 d4t1 : Vec 512) (d4W2 : Kernel4 512 512 3 3) (d4b2 d4g2 d4t2 : Vec 512) (d4Wp : Kernel4 512 256 1 1) (d4bp d4gp d4tp : Vec 512) (e0W1 : Kernel4 512 512 3 3) (e0b1 e0g1 e0t1 : Vec 512) (e0W2 : Kernel4 512 512 3 3) (e0b2 e0g2 e0t2 : Vec 512) (e1W1 : Kernel4 512 512 3 3) (e1b1 e1g1 e1t1 : Vec 512) (e1W2 : Kernel4 512 512 3 3) (e1b2 e1g2 e1t2 : Vec 512) (Wd : Mat 512 10) (bd : Vec 10) (x : Vec (3 * 224 * 224)) : den (resnet34FwdGraphFullPC epsStr ε Ws bs γs βs a0W1 a0b1 a0g1 a0t1 a0W2 a0b2 a0g2 a0t2 a1W1 a1b1 a1g1 a1t1 a1W2 a1b2 a1g2 a1t2 a2W1 a2b1 a2g1 a2t1 a2W2 a2b2 a2g2 a2t2 d2W1 d2b1 d2g1 d2t1 d2W2 d2b2 d2g2 d2t2 d2Wp d2bp d2gp d2tp b0W1 b0b1 b0g1 b0t1 b0W2 b0b2 b0g2 b0t2 b1W1 b1b1 b1g1 b1t1 b1W2 b1b2 b1g2 b1t2 b2W1 b2b1 b2g1 b2t1 b2W2 b2b2 b2g2 b2t2 d3W1 d3b1 d3g1 d3t1 d3W2 d3b2 d3g2 d3t2 d3Wp d3bp d3gp d3tp c0W1 c0b1 c0g1 c0t1 c0W2 c0b2 c0g2 c0t2 c1W1 c1b1 c1g1 c1t1 c1W2 c1b2 c1g2 c1t2 c2W1 c2b1 c2g1 c2t1 c2W2 c2b2 c2g2 c2t2 c3W1 c3b1 c3g1 c3t1 c3W2 c3b2 c3g2 c3t2 c4W1 c4b1 c4g1 c4t1 c4W2 c4b2 c4g2 c4t2 d4W1 d4b1 d4g1 d4t1 d4W2 d4b2 d4g2 d4t2 d4Wp d4bp d4gp d4tp e0W1 e0b1 e0g1 e0t1 e0W2 e0b2 e0g2 e0t2 e1W1 e1b1 e1g1 e1t1 e1W2 e1b2 e1g2 e1t2 Wd bd x) = resnet34Forward_full_pc ε Ws bs γs βs a0W1 a0b1 a0g1 a0t1 a0W2 a0b2 a0g2 a0t2 a1W1 a1b1 a1g1 a1t1 a1W2 a1b2 a1g2 a1t2 a2W1 a2b1 a2g1 a2t1 a2W2 a2b2 a2g2 a2t2 d2W1 d2b1 d2g1 d2t1 d2W2 d2b2 d2g2 d2t2 d2Wp d2bp d2gp d2tp b0W1 b0b1 b0g1 b0t1 b0W2 b0b2 b0g2 b0t2 b1W1 b1b1 b1g1 b1t1 b1W2 b1b2 b1g2 b1t2 b2W1 b2b1 b2g1 b2t1 b2W2 b2b2 b2g2 b2t2 d3W1 d3b1 d3g1 d3t1 d3W2 d3b2 d3g2 d3t2 d3Wp d3bp d3gp d3tp c0W1 c0b1 c0g1 c0t1 c0W2 c0b2 c0g2 c0t2 c1W1 c1b1 c1g1 c1t1 c1W2 c1b2 c1g2 c1t2 c2W1 c2b1 c2g1 c2t1 c2W2 c2b2 c2g2 c2t2 c3W1 c3b1 c3g1 c3t1 c3W2 c3b2 c3g2 c3t2 c4W1 c4b1 c4g1 c4t1 c4W2 c4b2 c4g2 c4t2 d4W1 d4b1 d4g1 d4t1 d4W2 d4b2 d4g2 d4t2 d4Wp d4bp d4gp d4tp e0W1 e0b1 e0g1 e0t1 e0W2 e0b2 e0g2 e0t2 e1W1 e1b1 e1g1 e1t1 e1W2 e1b2 e1g2 e1t2 Wd bd x

Full per-channel-BN ResNet-34 forward faithfulness. den (resnet34FwdGraphFullPC …) = resnet34Forward_full_pc …, chaining the per-block faithful lemmas + stem/maxpool/GAP/dense. The "text = render of a proven graph" forward half at the render's per-channel BN.