Backward-graph faithfulness for the VERIFIED ResNet-34 basic block #

The ResNet-34 peer of EfficientNetBackB0.lean / MobileNetV2BackB0.lean: a backward StableHLO graph that denotes the proven VJP of the batched ResNet-34 basic block.

The basic block is relu ∘ residual(F) (identity block), with body F = (conv-bn) ∘ (conv-bn-relu) — a 3×3 conv → bn → relu, then a 3×3 conv → bn (no activation), and an identity skip, followed by an outer relu after the residual add. This last fact is the structural difference from the MobileNetV2/EfficientNet residual blocks (whose residual add is the block output): r34 wraps the residual add in one more relu.

The relu wrinkle (vs relu6 / swish) #

r34 uses relu (one kink, at 0): its VJP is only the pointwise reluHasVJPAt, conditioned on the smoothness hypothesis ∀ k, x k ≠ 0 at the pre-activation — simpler than relu6's two-sided x k ≠ 0 ∧ x k ≠ 6, but the same _at machinery (vjpCompAt + HasVJP.toHasVJPAt). Its per-op backward token is .selectPos (the mask if x>0 then dy else 0), whose denotation faithfulness is the already-proven (rfl) StableHLO.selectPos_faithful.

Because there are TWO relu kinks (the body's mid-relu AND the outer post-residual relu), the whole-block VJP and its backward-graph faithfulness are _at / hypothesis-threaded: one smoothness family at the body's mid-relu pre-activation, one at the outer relu's pre-activation residual(F)(x).

Structure #

The stages are defined in Foundation, not here: cbReluB (batched conv → bn → relu, the relu sibling of cbrB), cbReluStridedB and projStridedB, with their _at VJPs, the backward graph cbReluBackBatchedGraph + cbReluBackBatchedGraph_faithful (chaining selectPos_faithful + bnBatchLABack_faithful + convBackBatched_faithful), and the four CertLayers cbReluLayer / projLayer / cbReluStridedLayer / projStridedLayer, are in Foundation/Batched/StageLayers.lean; projB (conv → bn, no activation, the body's cbB) is in Foundation/Batched/Stages.lean; projBackBatchedGraph / projBackBatchedGraph_faithful are in Foundation/Batched/BackLinks.lean. This file holds the ResNet-34 assemblies:

• the body cbB ∘ cbReluB — its backward graph r34BodyBackBatchedGraph, the two stage graphs chained at their cumulative activations, certified through the block layer.
• r34BasicBlockBackBatchedGraph_faithful — the CAPSTONE: the whole batched ResNet-34 identity basic block backward graph (outer-relu selectPos ∘ residual-fan-in(body-back) + identity skip) denotes the proven relu ∘ residual(F) VJP (vjpCompAt(residualHasVJPAt(body), relu)), threaded through both relu smoothness hypotheses.
• r34BasicBlockLayer / r34DownBlockLayer compose the stage layers with CertLayer.comp, residual / residualProj and reluOut, and each body/block VJP and capstone here is that composite's .vjp / .faithful.

The strided/downsample block (relu ∘ residualProj(proj, F_s)) #

The downsample-block capstone (r34DownBlockBackBatchedGraph_faithful) reuses the strided batched-conv backward primitive convStridedBackBatched (StableHLO.Basic, the stride-2 analog of convBackBatched; convStridedBackBatched_faithful is in Foundation/Batched/BackLinks.lean). The body F_s = projB ∘ cbReluStridedB has a stride-2 conv1 (cbReluStridedB, the strided sibling of cbReluB) and a stride-1 conv2 (projB); the projection skip projStridedB is a stride-2 conv-bn. The whole block composes vjpCompAt(residualProjHasVJPAt(proj, F_s), relu) exactly like the identity block, but with the projection skip (residualProj, both paths nontrivial) instead of the identity skip (residual), and the strided convs in the body+skip.