r50InputGradB IS the certified whole-net ResNet-50 gradient #

The whole-net input-gradient tie for resnet50ForwardBFull, the [3,4,6,3] bottleneck ladder at batch BatchNorm, at a variable batch N and resolution q. The parameter-gradient tie is ResNet50StepTieB's.

Almost all of it is ResNet-34's, reused rather than rewritten #

resnet50ForwardBFull is r34HeadB ∘ [3,4,6,3] bottlenecks ∘ r34StemB — the stem and head are literally ResNet-34's functions at R50's widths — so ResNet34BackCertifiedTieB supplies:

• cbReluStridedBBack_eq_vjp_backward and r34HeadBBack_eq_vjp_backward, the two endpoint ties;
• maxPool3s2FlatBackB and its rfl tie, plus the StableHLO.batchMapAux lift the batched 3×3/s2 pool needed;
• opaqueA0 … A16 and r34BFullHasVJPAt itself — the generic eighteen-stage apex. [3,4,6,3] is sixteen blocks for both nets, so the chain is the same construction and a second copy would be two writers for one fact. It is ResNet-34's only by where it was written; every dimension in it is a variable. The prefixes themselves are Foundation/OpaquePrefix.lean's.

What this file adds is the sixteen bottleneck slots, the tie, its pdiv reading, and the shape check resnet50ForwardBFull_eq_slots.

The two things ResNet-34's file did not face #

q is a BINDER. One statement covers resnet50in_fwd (q = 7, 224 px) and resnet50in160_fwd (q = 5, 160 px). So every dimension is an explicit 2 * (…) nest rather than 8 * q: those are equal Nats and NOT definitionally equal terms at a variable q.

Scope #

A smooth-point statement: the tie assumes 0 < εs, the stem relu clause (h_stem) and the stem pool's per-example condition (h_pool), and takes each of the sixteen bottlenecks as an opaque HasVJPDiffAt witness at its running activation (a bottleneck's three relu clauses — the two interior ones and the post-residual outer one — are the caller's, inside that witness). One device: every ResNet-50 data-parallel render synchronises BatchNorm, and its step is ResNet50SyncStepTieB's. It is about the INPUT gradient; the 161 parameter gradients are ResNet50StepTieB.lean's tie.

This statement takes no precision flag. The ImageNet runs the book reports train from resnet50in_momdp64bf16 and resnet50in160_lambaccdp4x128wxclipbcebf16, whose conv weight gradients are the bf16 kinds (Foundation.Bf16GradNodes); those runs' steps are ResNet50StepTieB's and, data-parallel, ResNet50SyncStepTieB's, both stated on the renderers' bf16 switch at the identity rounding (Bf16Erasure).