⭐⭐ mnv2InputGradB IS the certified whole-net MobileNetV2 gradient AT BATCH BATCH-NORM #

The per-example seventeen-bottleneck tie (retired 2026-09-19 with MobileNetV2PaperWholeBackCertifiedTie.lean) closed this for the forward the retired MobileNetV2Render.lean emitted. This file closes it for the net the shipped trainers run: mobilenetv2ForwardB_full, the same [t,c,n,s] ladder at bnBatchLA, at a variable batch N. It is tier T6 of planning/archive/proofs_tier_to_paper_nets.md §4.2, alongside ResNet34BackCertifiedTieB.lean.

⭐⭐ One apex, every stage opaque #

mobilenetv2PaperPC_has_vjp_at (below; it moved here from the retired per-example tie, whose apex it was) is a twenty-one-stage chain generic in every dimension and in every stage, so the batched net instantiates it directly: stem at mnv2StemB, the seventeen bottlenecks at the batched block maps, and the head's three stages at cbrB / batchMap gap / batchMap dense. opaqueA0 … A17 are OpaquePrefix.lean's. So this file defines no prefix defs — where ResNet-34's peer had to, because its committed apex bundles the stem's pool into stem and its head into one stage.

The three pieces #

1. mnv2StemBBack_eq_vjp_backward and cbrBBack_eq_vjp_backward — the two concrete conv-BN-relu6 endpoints, one rw of a conv leaf tie and then rfl each. ⚠ The stem's is the XLA-SAME leaf (flatConvStride2XlaBack) and the head's the plain one; that is the one convention this net and ResNet-34 do not share.
2. mnv2InputGradB_eq_mobilenetv2B_full_vjp and mnv2InputGradB_correct — the tie, and its reading as ∑ pdiv … * dy: the chain IS the Jacobian-transpose of the twenty-one-stage composition, at every batch size.
3. mobilenetv2ForwardB_full_eq_slots — the shape check: those twenty-one stages ARE mobilenetv2ForwardB_full, the forward mobilenetv2FwdGraphB_full_faithful (4.2b) says the typed graph denotes. Without it the tie would be a statement about variables.

⛔ Why the blocks stay opaque, measured on ResNet-34's peer. Instantiating a tie of this shape at the concrete blocks is a kernel deterministic timeout: the block witnesses are HasVJPAt at opaqueA{k-1} … x and a caller's are at mnv2PreB{k-1} N w x, which is seventeen defeq checks between seventeen-deep nested applications spelled through different definition chains. B0's file takes that step only because swish has no kink, so its witnesses are GLOBAL HasVJP and carry no point at all. The shape check is what replaces it, and it is the same answer the per-example file gave.

⚠ It stays a SMOOTH-POINT statement: relu6 is kinked on BOTH sides, so each of the 35 sites carries ≠ 0 ∧ ≠ 6. ⛔ MobileNetV2's two clauses per block are the expand relu6 and the depthwise relu6, both INSIDE the body — not ResNet-34's mid-relu and post-residual outer relu. Those are 4.2b's bundles, reused verbatim; this file adds no hypothesis of its own.

⛔ What this does NOT reach. Every gradient node in mobilenetv2in_rmsdp64 is followed by an all-reduce emitted as text outside the AST, so this is at the per-replica gradient (§4d). And it is about the INPUT gradient; the parameter gradients are MobileNetV2StepTieB.lean's tie (§4.2c).