A two-block inverted-residual net — end-to-end VJP (flattened Vec space) #

Defines mobilenetv2Forward — stem conv → bn → relu6, one inverted-residual block with a skip, one without (channel change), global average pool, dense head — and proves its vector–Jacobian product correct at a smooth point (mobilenetv2HasVJPAt, mobilenetv2HasVJPAt_correct), as cnnHasVJPAt does for the two-residual-block CNN. Every "bn" in this file is bnForward: one normalisation over the whole flattened tensor with scalar γ β : ℝ, not per-channel BatchNorm. Every conv is stride 1. The seventeen-block, batch-BatchNorm net the MobileNetV2 artifacts train is mobilenetv2ForwardBFull (MobileNetV2FullB).

Everything lives in flattened Vec space and reuses the foundation rules from CNN.lean, Depthwise.lean, BatchNorm.lean, MLP.lean, and Residual.lean through vjpCompAt chaining.

What's new here #

• relu6 (defined in MLP.lean, beside relu) — the clamped activation min (max x 0) 6. Unlike relu, the saturated branch is the constant 6 (not linear-through-origin), so the local-linearization trick matches relu6 against an affine surrogate g (proj on the active region, constant 0 below, constant 6 above) whose fderiv is the diagonal indicator 1_{0<x<6}. Smoothness is the two-sided x k ≠ 0 ∧ x k ≠ 6.

• Inverted-residual body — project ∘ depthwise ∘ expand:

  • expand : 1×1 conv → bn → relu6 (ic → mid, mid = t·ic)
  • depthwise: depthwise conv → bn → relu6 (mid → mid)
  • project : 1×1 conv → bn (linear bottleneck, no activation; mid → oc) With a stride-1 / ic = oc skip it becomes residual body (no final activation — MobileNetV2's linear-bottleneck design).

• End-to-end — stem (conv-bn-relu6) → skip inverted-residual → no-skip inverted-residual (channel change) → global average pool → dense head. Two blocks; channel counts and kernel sizes are binders; spatial h w preserved throughout (SAME convs).

Padding convention #

The strided pieces of the batched chain (MobileNetV2BackB0.lean on) read flatConvStride2Xla / depthwiseStride2FlatXla, the XLA-SAME (odd) phase every MobileNetV2 artifact emits. The 2-block generic mobilenetv2Forward here has a stride-1 stem.

All new defs/theorems certify to exactly [propext, Classical.choice, Quot.sound].

References #

• Sandler et al. 2018, MobileNetV2: Inverted Residuals and Linear Bottlenecks. https://arxiv.org/abs/1801.04381