The 210 parameters of the 17-block paper-spec net, in func-arg order. stem (4) + b1 no-expand (8) + b2..b17 (16 × 12 = 192) + head (4) + dense (2) = 210 — the same decomposition paperSig uses, at the names the committed AdamW artifact presents.

The 104 BN running-statistic slots = 52 BN layers × (μ, var): stem 1, b1 two (no expand BN), b2..b17 three each (48), head 1. Both an input (…i) and an output slot.

The driver's variant slug for a given (B, replicas): the artifact is verified_mlir/mobilenetv2_<variant>_train_step.mlir, the entry point is @mobilenetv2_<variant>_train_step, and LEAN_MLIR_VARIANT selects it. All three must agree — the shim checks the entry name and refuses a mismatch outright ("entry mismatch") rather than running the wrong graph. B = 32 is deliberately unsuffixed so the committed artifact keeps its name. The #guards at the bottom pin the literal #eval paths against this.

The MobileNetV2 forward chain at the BATCHED index — one traversal, consumed by both @mobilenetv2_fwd and every train step that differentiates it.

⭐⭐ This exists so @mobilenetv2_fwd and the batch-BN train steps cannot be different nets. They were: the retired MobileNetV2Render.lean built its forward from the PER-EXAMPLE chain — bnPerChannelF, reduce [2,3], divisor H·W — while every train step in this file is batch BN, reduce [0,2,3], divisor B·H·W. scripts/regen_verified_mlir.sh's check_adam_prefix carried the divergence as the LAST KNOWN_SPLIT entry for as long as both existed. This is ResNet34RenderB.r34FwdChainB's shape, for ResNet50RenderB.r50FwdChainB's reason (planning/archive/renderer_convergence.md, leg 2).

⚠ The EVAL forward is deliberately NOT moved onto this chain, exactly as ResNet-34's and ResNet-50's are not: bnPerChannelEvalF reads frozen per-channel statistics and reduces nothing, so mobilenetv2_fwd_eval.mlir is BatchNorm-world-agnostic and correct against both chains. (Until 2026-09-08 there was a second reason: a whole-net float budget's provenance claim named that artifact's SSA names line for line; the budget is deleted, and the eval forward stays where it is only because moving it buys nothing.)

⭐ Extracting the traversal is byte-neutral for the train step: pretty's SSA counter follows the call SEQUENCE, and the sequence is unchanged.

@mobilenetv2_fwd rendered from the BATCHED chain — the same traversal every batch-BN train step in this file differentiates, so the net that scores and the net that trains are one graph by construction. Replaces the retired MobileNetV2Render.lean as the writer of verified_mlir/mobilenetv2_fwd.mlir (2026-09-06, planning/archive/renderer_convergence.md leg 2). Takes %x plus the parameters in mnv2SigList order — 159 inputs at the shipped convBias := false — and returns logits [B, nClasses].

⚠ This CHANGES what @mobilenetv2_fwd computes, and that is the point. The retired render normalised PER EXAMPLE while the AdamW and RMSProp steps whose accuracies the book quotes normalise over the BATCH. ⚠ It also renames every parameter — %sW/%b2eW/%Wd where the retired one said %Ws/%We2/%Wfc — because the names now come from mnv2SigList, this file's single source. The driver binds positionally, so nothing downstream sees the rename.

MobileNetV2 (17-block paper spec) AdamW train step, batch BN, rendered from the verified AST at N := B. 739 inputs (%x, 210 θ, 210 m, 210 v, %lr/%bc1/%bc2, 104 running-stat slots, %onehot) and 737 outputs (210 θ', 210 m', 210 v', %loss/%bc1/%bc2, 104 batch stats) — the interface the committed hand-written artifact already presents, so the driver is unchanged. Parameter ORDER comes from mnv2SigList and stat order from mnv2StatSigList, the single sources, so the arity/order contract cannot drift.

Stem 3×3/s2 (3→32, 224→112, NO maxpool) → b1 (no-expand t=1, 32→16) → b2..b17 (4 stride-2 downsamples, 10 identity skips, 2 stage-first widenings) → 1×1 conv-BN-relu6 head (320→1280) → GAP → dense (1280→nClasses).

@mobilenetv2_fwd_eval rendered ENTIRELY from the verified AST — the inference forward, every BN site consuming frozen per-channel running stats (bnPerChannelEvalF) instead of reducing statistics out of its activation. Same 210 params in the same order, plus the 104 stat inputs (52 BN layers × μ/var, interleaved per layer in bnChannels order): 315 inputs.

Its train-step partner is the batch-BN mobilenetv2_adam_train_step in MobileNetV2RenderB, whose returned batch μ/var the driver EMAs into exactly these slots. Being frozen-stat affine, this graph is the same in either BN world — which is why it can live beside the per-example chain: bnPerChannelEvalF performs no reduction, so there is no batch to be honest about.