ResNet-34's whole-net input-VJP at TRUE BATCH-NORM (T1, the VJP half) #

ResNet34FullB.lean states the batch-BN forward and its typed graph. This file gives that forward a certified HasVJPAt at the paper depth — the batched peer of what MobileNetV2FullVJP.lean does for MobileNetV2's seventeen bottlenecks, and the last piece of T1 in formalization.yaml 4e's port.

No new mathematics, and one new lemma one tier down #

Every block VJP is already proven at bnBatchLA: r34BasicBlockB_has_vjp_at and r34DownBlockB_has_vjp_at (ResNet34BackB0.lean) are exactly the two block shapes ResNet34FullB.lean's r34IdB / r34DownB unfold to. The eight bundle lemmas below are delegations in the EfficientNetFullB0 style.

⭐ The one thing that did not exist is batchMap_has_vjp_at (Foundation/BatchMapVJPAt.lean, written for this): r34's stem ends in batchMap N (maxPool3s2Flat 64 56 56) and a max-pool has no derivative at a tie, so the GLOBAL batchMap_has_vjp cannot lift it. The per-example pool VJP at a Vec point was already there (maxPool3s2Flat_has_vjp_at_vec), so 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 no-tie condition — bundled per block into R34IdSmoothAt / R34DownSmoothAt so the apex binds 18 smoothness bundles rather than 34 loose hypotheses, exactly as MobileNetV2FullVJP.lean bundles IVSmoothAt.

⚠ 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 batchMap_has_vjp_at consumes.

The running activations are named r34Pre1 … 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 resnet34ForwardB_full_eq_chain bridges it back to the committed nested-application forward.

⭐ N is a variable throughout: this tier carries no numerals.