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

ResNet50FullB.lean states the batch-BN forward at the [3,4,6,3] bottleneck ladder. This file gives that forward a certified HasVJPAt — the last piece of T1 for the largest hole in the Proofs tier (planning/archive/proofs_tier_to_paper_nets.md §3.5(a)).

No new mathematics, and nothing new one tier down #

Every block VJP is already proven at bnBatchLA: r50BottleneckB_has_vjp_at, r50ProjBlockB_has_vjp_at and r50DownBlockB_has_vjp_at (ResNet50BackB0.lean) are exactly the three shapes r50IdB / r50ProjB / r50DownB unfold to. The bundle lemmas below are delegations in ResNet34FullBVJP.lean's style.

⭐ And unlike ResNet-34's, this file needed no new Foundation lemma. r34's T1 was blocked on batchMap_has_vjp_at (4.1c) for its stem pool. ResNet-50 has the same stem — and reuses r34StemB_has_vjp_at verbatim, so that lemma is spent rather than re-derived. The head is ResNet-34's too (r34HeadB_has_vjp, GLOBAL: GAP and dense are smooth and each is batchMap of a per-example op, so no hypothesis appears).

The hypothesis budget #

⚠ Pointwise (HasVJPAt), not global, and necessarily. relu is kinked. ⛔ And a BOTTLENECK carries THREE kink clauses, where ResNet-34's basic block carries two: the two interior relus and the post-residual OUTER relu. Sixteen blocks give 48 clauses, plus the stem's relu and the stem pool's no-tie condition — bundled per block into R50IdSmoothAt / R50ProjSmoothAt / R50DownSmoothAt so the apex binds 18 bundles rather than 50 loose hypotheses.

⚠ The pool's condition is per example (R34PoolSmoothAt, reused): a tie is a property of one image's 3×3 window, not of the batch.

⛔ 0 < q is a real hypothesis here, where ResNet-34 needed none. r34's ladder is at literals, so 0 < 56 closes by norm_num; R50's is at the binder q, and the stem pool's VJP needs its output grid nonempty. At q = 0 the net is degenerate and the statement says so.

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

⭐ N and q are both variables: this tier carries no numerals, so ONE statement covers resnet50in_fwd (q = 7, 224 px) and resnet50in160_fwd (q = 5, 160 px) — the net the quoted 76.66% trains — at every batch size.