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

MobileNetV2FullB.lean states the batch-BN forward and its typed graph. This file gives that forward a certified HasVJPAt at the paper depth — the MobileNetV2 peer of ResNet34FullBVJP.lean, and the second piece of formalization.yaml 4e's port.

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

Every block VJP is already proven at bnBatchLA: mnv2BodyB_has_vjp_at and mnv2DownBodyB_has_vjp_at (MobileNetV2BackB0.lean) are exactly the two body shapes mnv2ExpOnlyB / mnv2StridedB unfold to, and residual_has_vjp_at wraps the first for the ten skip blocks. The bundle lemmas below are delegations in the EfficientNetFullB0 style.

⭐ Where r34 needed a new Foundation lemma, this net needs none. ResNet-34's stem ends in batchMap N (maxPool3s2Flat …) and a max-pool has no derivative at a tie, so 4.1c had to write batchMap_has_vjp_at. MobileNetV2 has NO stem pool — the stem is conv-BN-relu6 and downsamples once — and its head's GAP and dense are smooth, so batchMap_has_vjp (the global one) covers every batchMap in the net.

⭐ Three shapes are bnRelu6Stage_has_vjp_at at a different inner op, and that lemma is already generic in it: the stem is that stage at flatConvStride2Xla, the head's first stage is cbrB, and the expand/depthwise stages are cbrB / dwbrB / dwbrBstrided. The t = 1 block projB ∘ dwbrB (b1) has no mnv2*BodyB peer; it is dwbrLayer ; projLayer.

The hypothesis budget #

⚠ Pointwise (HasVJPAt), not global, and necessarily. relu6 is kinked on BOTH sides, so each site carries ≠ 0 ∧ ≠ 6 and a global HasVJP through it is false. That is the repo standard for the relu-family nets and matches MobileNetV2FullVJP.lean's per-example fold; the axis this file moves is the BatchNorm world, not the pointwise/global one.

⛔ Two kink clauses per bottleneck, and the second is not r34's. ResNet-34's blocks carry the body's mid-relu AND a post-residual OUTER relu. MobileNetV2's carry the EXPAND relu6 and the DEPTHWISE relu6, both inside the body — the linear bottleneck has no activation after project, so the residual add IS the block output and contributes nothing. Sixteen expand-bearing blocks give 32 clauses, plus b1's single depthwise clause, plus the stem's and the head's: 35 relu6 sites, bundled into 19 binders.

⭐ The positivity bundles are REUSED, not re-declared: IVPos / IVNoExpPos (MobileNetV2FullVJP.lean) say 0 < ε at each BatchNorm site and know nothing about which world reduces it. Only the smoothness bundles need batched peers, because a kink condition names the activation and bnBatchLA is a different activation from bnPerChannelTensor3.

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

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