THE BLOCK TABLE — transcribed once, from jax/MainMobilenetV4.lean.

⭐⭐ Everything downstream folds over this list: the parameter signature, the BN stat slots, the forward chain, the backward chain and the running-statistic recomputes. Before it existed the same rows were hand-written FOUR times, and §3/§7.2's whole point is that a divergence between two such readings is invisible — same ops, same channel counts, same types, different net. One table means a dispatch error is a typo in one place rather than a mismatch nothing checks.

Families in order (Conv-M): ExtraDW ×7, ConvNeXt, FFN, ConvNeXt, ExtraDW ×4, FFN, ConvNeXt, ExtraDW ×2, FFN ×2, ConvNeXt — 13 ExtraDW / 4 ConvNeXt / 4 FFN, and no IB at all, where Conv-S used three. Spatial ladder 56 → 28 → 14 → 7.

⚠ Verified against timm 1.0.28 (mobilenetv4_conv_medium, walking model.blocks[1:4]): all 21 rows agree on (ic, oc, expand, preDWk, postDWk, h, stride2). The #guards in Proofs/Nets/MobileNet/MobileNetV4BackB0.lean pin that reading; they are derived from timm rather than re-read off this table, or they would gate nothing.

The MobileNetV4-Conv-M parameter inputs, in func-arg order: stem (3), the fused stage, the 21 UIB blocks, the TWO head convs, the classifier. Single source for the signature and the return order, the same role r50ShapeList plays for R50.

⚠ This list and VLayer.toSpecs are TWO HAND-WRITTEN READINGS of the same layout — the renderer cannot import the spec without inverting the dependency, which is the same two-lists shape as toSpecs == XLayout.specs elsewhere. mnv4-fwd-smoke is the gate that pins them.

The same list as MLIR types. Derived, so the shapes have one definition.

The 154 BN running-statistic slots = 77 BN layers × (μ, var), in forward-traversal order: stem, the fused stage's two, each UIB block's (2–4 depending on family), the head.

⚠ A misaligned stat slot is SILENT: the arities still match and the wrong layer's statistics simply flow into the wrong @mnv4_fwd_eval slot. That is why the order here and the order the train step returns them in are both derived from the same block table, and why the eval forward reads them through mnv4Bn's statP rather than an independently-numbered list.

The stat slots as MLIR types. Derived, so the widths have one definition.

The MobileNetV4-Conv-M forward chain, batch BN, at N := B, 224² → 10 classes.

Transcribed 1:1 from jax/MainMobilenetV4.lean, which is the faithful Conv-M table as of 2026-08-14 (historical/RESULTS.md's 84.58% belongs to the SUPERSEDED Conv-S table). Spatial ladder:

  224 --stem s2--> 112 --fused s2--> 56 --uib s2--> 28 --uib s2--> 14 --uib s2--> 7 --GAP--> 1

Block dispatch is forced by the table and checked by the types: the three stride-2 blocks (1, 3, 11) are ic ≠ oc and split by which depthwise carries the stride — all three are PRE-strided in Conv-M; the eighteen stride-1 blocks are all ic = oc, hence all skip. Families in order after the fused stage: ExtraDW ×7, ConvNeXt, FFN, ConvNeXt, ExtraDW ×4, FFN, ConvNeXt, ExtraDW ×2, FFN ×2, ConvNeXt — 13 / 4 / 4 and no IB at all. ⚠ This paragraph listed Conv-S's fourteen families until 2026-09-07.

Activations, and they are not uniform — each read off the emitter that produced the number, not assumed:

• stem and head .convBn → relu (MlirCodegen.lean:5852, emitConvBnTrain … useRelu := true)
• the fused stage → swish (jax/Jax/Codegen.lean:1031) — a deliberate paper deviation, see fusedMbConvFwdStridedB
• every UIB block → relu (MlirCodegen.lean:6357, "Plain ReLU throughout")

Returns the full forward RECORD, not just (code, logits): the train step needs every saved activation the backward reads, and the alternative — a second copy of the chain inside the train step — is the two-readings defect this file exists to avoid.

Every distinct channel width a bias-free conv in this net binds %zb{c} at: the stem, the fused stage's two convs, each block's pre-DW (ic), expand and post-DW (mid) and project (oc), and the head. Derived by hand and pinned by mnv4-fwd-smoke, which fails on an unbound %zb.

@mnv4_fwd — the MobileNetV4-Conv-M forward as one MLIR module.

%x plus mnv4SigList's parameters in VLayer.toSpecs order, logits [B, nClasses]. Every conv is bias-free, so the proven conv ops' bias operands bind to the %zb{c} zero constants the prelude declares — same op, bias = 0, and x + 0.0 is exact (§2l step B).

⚠ zeroBiasPrelude must cover every width the chain references or the module has an unbound SSA name. That is a link error at parse time rather than a wrong number, which is the good direction, but mnv4-fwd-smoke checks it anyway so the failure arrives at lake build and not at iree-compile.

@mnv4_fwd_eval — the inference forward, every BN site reading frozen running stats. %x + 233 params + 154 stat inputs = 388 inputs (counted off mnv4_fwd_eval.mlir). This is what the driver scores through.

⭐ It is mnv4FwdChainB at .eval — the SAME traversal @mnv4_fwd and the train step use, so its BN order matches mnv4StatSigList by construction rather than by a second reading.

The driver's variant slug for a given (B, replicas): the artifact is verified_mlir/mnv4_<variant>_train_step.mlir, the entry point is @mnv4_<variant>_train_step, and LEAN_MLIR_VARIANT selects it. All three must agree — the shim checks the entry name and refuses a mismatch outright rather than running the wrong graph. B = 32 is deliberately unsuffixed so the Imagenette artifact keeps a stable name.

MobileNetV4-Conv-M AdamW train step, batch BN, rendered from the verified AST at N := B.

858 inputs (%x, 233 θ, 233 m, 233 v, %lr/%bc1/%bc2, 154 running-stat slots, %onehot) and 856 outputs (233 θ', 233 m', 233 v', %loss/%bc1/%bc2, 154 batch stats) — counted off mnv4_adam_train_step.mlir, which is the only reading that cannot go stale (this line said 583 / 581 at Conv-S's 158 slots until 2026-09-07). Parameter order comes from mnv4ShapeList — through zipPs, which builds each block's gradient list from the very same uibSig slice the signature does — and stat order from mnv4StatShapeList.

Forward: stem 3×3/s2 XLA-SAME (3→32, 224→112) → fused MBConv (32→48, 112→56, swish) → the 21 UIB blocks (three stride-2 downsamples, eighteen identity skips; ExtraDW, ConvNeXt and FFN — no IB) → TWO 1×1 conv-BN-relu head stages (256→960, then 960→1280) → GAP → dense.

The cotangent is composed from kit ops (softmaxRow → subB → scaleB → addVB → shiftB → divConstB, α = 0.1, K = nClasses), and %loss is report-only and stays outside the AST — the same carve-out resnet34/mobilenetv2 take.