ResNet-34's whole-net input-VJP at TRUE BATCH-NORM #

ResNet34FullB.lean states the batch-BN forward and its typed graph. This file gives that forward a certified HasVJPAt at the paper depth — the peer of what MobileNetV2FullBVJP.lean does for MobileNetV2's seventeen bottlenecks.

No new mathematics, and one lemma one tier down #

Every block VJP is already proven at bnBatchLA: r34BasicBlockBHasVJPAt and r34DownBlockBHasVJPAt (ResNet34BackB0.lean) are exactly the two block shapes ResNet34FullB.lean's r34IdB / r34DownB unfold to. The bundle lemmas below are delegations in the EfficientNetFullB0 style, and the whole net is those blocks' CertLayers composed.

The one lemma this needs below the net is batchMapHasVJPAt (Foundation/BatchMapVJPAt.lean): r34's stem ends in batchMap N (maxPool3s2Flat 64 56 56) and a max-pool has no derivative at a tie, so the GLOBAL batchMapHasVJP cannot lift it. With the per-example pool VJP at a Vec point (maxPool3s2FlatHasVJPAtVec), the batched pool is two lines.

The hypothesis budget #

Pointwise (HasVJPAt), not global, and necessarily. relu is kinked. And r34 carries two kink clauses per block, not one: the body's mid-relu AND the post-residual outer relu. That outer relu is ResNet's structural difference from MobileNetV2/EfficientNet, whose residual add IS the block output. Sixteen blocks therefore carry 32 clauses, plus the stem's relu and the stem pool's condition (every window's maximum at one position, or the window all zero) — bundled per block into R34IdSmoothAt / R34DownSmoothAt, and those 18 bundles into one R34SmoothAtB (the positivity bundles into R34PosB), so the apex binds two hypotheses, exactly as MobileNetV2FullBVJP.lean's MNV2SmoothAtB / MNV2PosB.

The pool's condition is per example (∀ r : Fin N, MaxPool3s2Smooth … on that example's row), because a tie is a property of one image's window, not of the batch. That is the shape batchMapHasVJPAt consumes.

The running activations are named r34Pre0 … r34Pre16 so each bundle can be STATED at the activation entering its block without a sixteen-deep nested application inline; r34Pre16 doubles as the trunk, and resnet34ForwardBFull_eq_chain bridges it back to the committed nested-application forward.

N is a variable throughout: the batch size is never pinned (the 224-px resolution and the 64…512 widths are literals).