MobileNetV4-Conv-M's block table #
UibSpec (one Universal Inverted Bottleneck row) and mnv4Blocks (the 21 rows of Conv-M), the one
transcription of the net's layout. The renderer (MobileNetV4RenderB) folds over it to
emit the artifacts, and the proof chain from MobileNetV4BackB0.lean on folds over it to state the
net, so the proofs read the table without importing the renderer. Names are in Proofs.StableHLO,
where the renderer first defined them.
One row of the MobileNetV4-Conv-M block table. h is the block's OUTPUT spatial size, so
a stride2 block reads its input at 2h.
- p : String
parameter-name prefix:
"1"…"21"(Conv-M; Conv-S ran to"14"). - ic : Nat
- oc : Nat
- expand : Nat
- preDWk : Nat
pre-depthwise kernel,
0= absent. - postDWk : Nat
post-depthwise kernel,
0= absent. - h : Nat
- stride2 : Bool
Instances For
Equations
Equations
- One or more equations did not get rendered due to their size.
Instances For
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.
Equations
- One or more equations did not get rendered due to their size.