Backward-graph faithfulness for the VERIFIED ResNet-50 bottleneck block #

The R50 peer of ResNet34BackB0.lean, and the step planning/archive/mnv4_verified.md §8 calls <blk>BackBatchedGraph + <blk>BackBatchedGraph_faithful — the two theorems that make the render's backward the certified one. R50 shipped a trained number (89.86%, Imagenette) off a certified renderer with no whole-net backward at all; this file is that gap.

⚠⚠ WHAT §8 GOT WRONG — "R50 is one step from done" was measured against the WRONG phase 1 #

§8 records R50's block-level VJP as ✓ (ResNet50BlocksCertified.lean, retired 2026-09-19) and concludes the job is only (2) + (3). That certificate is real, but it is for the per-channel, non-batched forms — bblkPC / bblkPProjPC / bblkPStridedPC are built from bnPerChannelTensor3 and plain flatConv, with no N. The backward-graph vocabulary is batched: bnBatchLA, batchMap, convBackBatched. Grepped before starting: there is no batched R50 block VJP anywhere in the repo. So phase 1 had to be redone in the batched world here, exactly as §8 says MNv4 needs — R50 was two steps from done, not one.

⭐ It was still cheap, and for the reason §1 of the R50 file already gives: every stage this needs already exists. ResNet34BackB0 builds its own batched stages rather than lifting the PC ones, and those stages are generic in {ic oc h w kH kW}, so R50 reuses all four verbatim:

Zero new stages, zero new SHlo ops, zero new VJP obligations. The bottleneck's third conv is one more CertLayer.comp, and the whole file is composition — §6's "a family from one constructor" landing on R50's backward the way §3i records it landing on MNv4's.

The three forms, and why the third exists #

R34 never needed the third: its stage 1 is ic = oc = 64, so block 0 is an identity block. R50's stage 1 goes 64 → 256 at stride 1 — the channels change so it needs a projection, the resolution does not so that projection is not strided. ⚠ r50DownBlock cannot be substituted for it: its type reads Vec (N * (ic * (2*h) * (2*w))) → Vec (N * (oc * h * w)), so the halving is in the signature and the substitution is a shape error. Reaching for the identity form instead is the dangerous one — an identity skip where a projection belongs is well-typed only if ic = oc.

⚠ THE STRIDE IS ON THE 3×3, NOT THE LEADING 1×1 #

r50DownBody puts cbReluStridedB on the second conv. That is ResNet v1.5 / torchvision, which is what jax/MainResnet50Imagenet.lean trains. The v1 placement (stride on the leading 1×1) compiles, trains and descends — and is a different net (§3's trap, and VerifiedSpec.lean:46 records it costing ~0.5 pt of top-1). The leading 1×1 therefore runs at the INPUT resolution (2*h)×(2*w) and carries mid channels there until W₂ decimates.

Relu, and why every statement here is _at #

R50 is relu throughout, so — per §8's design note — the VJPs are pointwise and hypothesis-threaded via vjp_comp_at, never the global form. A bottleneck has three kinks, not the basic block's two: the two interior relus (h_s1, h_s2) and the outer post-residual relu (h_out). The per-op backward token is .selectPos, whose faithfulness is the already-proven selectPos_faithful.

Structure #

• r50BodyBackBatchedGraph — the stride-1 bottleneck body projB ∘ cbReluB ∘ cbReluB's backward graph (r50DownBodyBackBatchedGraph is its strided peer).
• r50BottleneckBackBatchedGraph_faithful — CAPSTONE 1, the identity block relu ∘ residual(F).
• r50ProjBlockBackBatchedGraph_faithful — CAPSTONE 2, relu ∘ residualProj(projB, F), the form with no R34 analogue.
• r50DownBlockBackBatchedGraph_faithful — CAPSTONE 3, the strided projection block relu ∘ residualProj(projStridedB, F_s).

Each block is a CertLayer (r50BottleneckLayer, r50ProjBlockLayer, r50DownBlockLayer) composed from ResNet34BackB0's stage layers, and each capstone is that layer's faithful.