MobileNetV2 at TRUE BATCH-NORM — the whole net's forward and graph (T1-forward, T2) #

The MobileNetV2 peer of ResNet34FullB.lean, and the first half of planning/archive/proofs_tier_to_paper_nets.md section 4.2's MobileNetV2 column.

MobileNetV2FullPaper.lean states this net's whole-net ℝ forward and typed graph at per-example BatchNorm (bnPerChannelTensor3, reduce [2,3]). That was the world of mobilenetv2_fwd.mlir and the Imagenette SGD trainer mobilenetv2_train_step.mlir, and every tier built on it is true and was correctly paired with those bytes. It is NOT the world of mobilenetv2_adam_train_step.mlir, mobilenetv2_rms_train_step.mlir or any ImageNet artifact — including mobilenetv2in_rmsdp64, whose accuracy the book quotes — all of which reduce [0,2,3]: one mu/var per channel across the batch, the one op that couples examples.

⛔ MobileNetV2's two renderers did not overlap, so this was not a flag away. MobileNetV2Render.lean was SGD-inline and per-example only; MobileNetV2RenderB is AdamW/RMSProp-only, at the batched index and at batch BatchNorm. This file re-states the ladder at bnBatchLA (= the proven bnBatchTensor4 at the network's left-assoc index), which is that renderer's world. ⭐ Since 4c leg 2 (2026-09-06) it is the ONLY renderer: the per-example one and its train step are retired and mobilenetv2_fwd.mlir comes from the batched chain too, so this file's world is now the whole net's.

What is new here, and what is not #

⭐⭐ Nothing about the blocks is new. MobileNetV2BackB0.lean already carries the batched relu6 stages (cbrB, dwbrB, dwbrBstrided, and projB from EfficientNetRenderPC.lean), their _at VJPs and their backward-graph faithfulness, all at bnBatchLA. What was missing is the level above: a net-level ℝ forward, a net-level forward graph, and the faithfulness tying them. This file is that enumeration.

⭐ The weight bundles are reused, not re-declared. IVW / IVWNoExp (MobileNetV2FullPaper.lean) hold kernels, epsilons, gammas and betas — nothing that knows which BatchNorm world reduces them — so the batched net binds the same records the per-example one does. Only the top-level bundle is new, because it is generic in the class count where the retired per-example record was pinned at 10.

⚠ Padding is XLA-SAME at all five stride-2 sites — the stem 3x3/s2 conv and the four stride-2 depthwises (b2, b4, b7, b14). These are flatConvStride2Xla / depthwiseStride2FlatXla, NOT r34's symmetric flatConvStride2 peers; the two families have identical types and identical emitted shapes, so only the certificate distinguishes them, and MobileNetV2 is the TF-origin net. scripts/convention_audit.py sees this at the artifact tier and nothing sees it here, so it is stated.

⚠ There is no max-pool. MobileNetV2's stem is conv-BN-relu6 and downsamples once; r34's stem is conv-BN-relu, then a 3x3/s2 pool. That is why this net needs no batchMap_has_vjp_at.

Conventions this net runs at #


depth	17 bottlenecks, the paper `[t,c,n,s]` table, stem 32 to head 1280
BatchNorm	batch (`bnBatchLA`, reduce `[0,2,3]`, width `Nhw`), 52 sites
activation	relu6 (TWO kinks, at 0 and at 6); 35 sites, none after a `project`
stride-2 padding	XLA-`SAME` at all five sites
stem	3x3/s2 conv-bn-relu6, 3 to 32, 224 to 112 (NO pool)
head	1x1 conv-bn-relu6 320 to 1280, then GAP and dense, generic in the class count
artifacts	`mobilenetv2_fwd` and every train step — this net now has ONE chain (4c leg 2)

⭐ The head is generic in nCls, so one statement covers the 10-class Imagenette artifacts and the 1000-class mobilenetv2in ones.

⚠ N stays a variable throughout. T1 and T2 carry no numerals, so the batch size does not need pinning here; it is pinned only where a Maps envelope turns a width into a rational (T4/T5), and the artifacts' N is the PER-REPLICA batch (64 on the data-parallel runs) because the collectives average gradients and no BatchNorm statistic is all-reduced.

⚠ The bias operand names are the render's DEFAULT convBias := false ones — %zb{c}, the shared zero constant each conv, depthwise and project bias is bound to once its real bias has been folded into the BatchNorm that follows it. That is what makes the shipped parameter census 158 and not 210. Every graph below is ∀-quantified over the bias VALUE, so it covers the convBias := true render too; only the name would differ there.