MobileNetV2's whole-net input-VJP at batch BatchNorm #

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.

Built from the block VJPs #

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

No pointwise batchMap lemma is needed. ResNet-34's stem ends in batchMap N (maxPool3s2Flat …) and a max-pool has no derivative at a tie, so it needs batchMapHasVJPAt. MobileNetV2 has NO stem pool — the stem is conv-BN-relu6 and downsamples once — and its head's GAP and dense are smooth, so batchMapHasVJP (the global one) covers every batchMap in the net.

Three shapes are bnRelu6StageHasVJPAt 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. relu6 is kinked on both sides, so each site carries ≠ 0 ∧ ≠ 6 and a global HasVJP through it is false.

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 IVPos / IVNoExpPos (MobileNetV2FullPaper.lean): 0 < ε at each BatchNorm site. The smoothness bundles are declared here, because a kink condition names the activation, which is bnBatchLA's output.

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 mobilenetv2ForwardBFull_eq_chain bridges it back to the committed nested-application forward.

N is a variable throughout.