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

Tier T6 of planning/archive/proofs_tier_to_paper_nets.md §3.5(e) — the last of the four statements ResNet-50 was missing that says anything ((d)'s two float budgets are the vacuous half). T1, T2 and T3 landed 2026-09-06; with this the net is certified from its ℝ forward through its typed graph, its 161-parameter train-step tie and now its whole-net input gradient.

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

resnet50ForwardB_full is r34HeadB ∘ [3,4,6,3] bottlenecks ∘ r34StemB — the stem and head are literally ResNet-34's functions at R50's widths (§3.5b) — so §4.2d's file 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 r34B_full_has_vjp_at 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 resnet50ForwardB_full_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 — the net the quoted 76.66% trains). ⛔ 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. And 0 < q is a real hypothesis where ResNet-34 needed none — the stem pool's VJP needs its output grid nonempty, and at literal 56 that closed by norm_num.

⚠ It stays a SMOOTH-POINT statement, and ResNet-50 carries the heaviest kink budget in the suite: three relu clauses per bottleneck — the two interior ones and the post-residual outer one — where ResNet-34's basic block has two and EfficientNet's MBConv none. Those are §3.5b's bundles, reused verbatim; this file adds no hypothesis of its own.

⛔ The blocks stay opaque and there is no backward_unique step, for §4.2d's measured reason: instantiating a tie of this shape at the concrete blocks is a KERNEL deterministic timeout when the witnesses are HasVJPAt carrying a saved activation. B0 takes that step only because swish has no kink. The shape check is what replaces it.

⛔ What this does NOT reach. resnet50in160_lambaccdp8x64bce all-reduces every gradient as text outside the AST, so this is at the per-replica gradient (§4d). And it is about the INPUT gradient; the 161 parameter gradients are ResNet50StepTieB.lean's tie (§3.5c).