MobileNetV2 at batch BatchNorm — the whole net's forward and graph #

The MobileNetV2 peer of ResNet34FullB.lean. mobilenetv2ForwardBFull is the seventeen-bottleneck net at batch BatchNorm (bnBatchLA, the proven bnBatchTensor4 at the network's left-assoc index; reduce [0,2,3]: one mean/variance per channel across the batch, the one op that couples examples), which is the forward MobileNetV2RenderB emits for mobilenetv2_fwd, mobilenetv2in_fwd and the f32 train steps. mobilenetv2FwdGraphBFull is its typed graph and mobilenetv2FwdGraphBFull_faithful ties the two.

What this file adds #

The batched relu6 stages (cbrB, dwbrB, dwbrBstrided in Batched.StageLayers, projB in Batched.Stages), their _at VJPs and their backward-graph faithfulness are one level down, all at bnBatchLA; MobileNetV2BackB0.lean composes them into block bodies. This file adds the net-level ℝ forward, the net-level forward graph, and the faithfulness tying them.

The block weight records IVW / IVWNoExp come from MobileNetV2FullPaper.lean; only the top-level bundle MNV2BWeights is declared here, generic in the class count.

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/gates/convention_audit.py checks this at the artifact level.

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 batchMapHasVJPAt.

Precision is a flag on the graph. Every conv and depthwise site is .convAt bf16 id … / .convStridedXlaAt … / .depthwiseAt … / .depthwiseStridedXlaAt … (StableHLO.PrecisionSwitch, the renderers' own switch), so one builder describes the f32 artifacts (bf16 := false) and the bf16 ones (bf16 := true, the kinds mobilenetv2in_rmsdp64wxdols0eps0001bf16 emits); BatchNorm, relu6, GAP and the dense carry no flag because no render switches them. The faithfulness theorems hold at either value through Bf16Erasure (Bf16Fold.denOp_convAt_id, …: the bf16 kind at the identity rounding is its f32 peer), so the typed graph denotes mobilenetv2ForwardBFull whichever precision the text declares. The rounding itself is not modelled here, as it is not at f32: den is over ℝ at both values.

Conventions this net runs at #

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. On the data-parallel artifacts the render's N is the per-replica batch and BatchNorm is synchronised across replicas; MobileNetV2SyncB.lean is this file's twin for them: replica r's forward graph denotes shard r of mobilenetv2ForwardBFull (R * N), this file's forward at the global batch.

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.

References #

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