MobileNetV4-Conv-M at batch BatchNorm — the whole net's forward and graph #

MobileNetV4BackB0.lean is the block and stage level — every UIB family, the stride-2 form, the fused stage, the head, the table-driven k = 0 dispatch and the row-typed UibParams. This file is the net level: a net-level ℝ forward at the 21-row Conv-M table (mobilenetv4ForwardBFull), the typed StableHLO graph over it at mnv4FwdChainB's own tokens (mnv4FwdGraphBFull), and their faithfulness (mnv4FwdGraphBFull_faithful). ResNet50FullB.lean is the file this one mirrors.

This is timm's mobilenetv4_conv_medium (1.0.28, the pinned spec): the post-DW carries each downsample's stride, the pre-DW is BN only, stage 0 is relu, the head pools before conv_head, the stem pads symmetrically. The artifacts are pinned to that function by three gates: scripts/parity/mnv4_timm_parity.py (the JAX reference = timm on shared weights), scripts/parity/mnv4_forward_tie.py (the render = the JAX reference) and scripts/parity/grad_tie.py --net mnv4 (the render's backward = jax.grad of it).

No accuracy is quoted for this net.

The trunk is five CertLayer groups #

Each resolution group — rows 1–2, 3–6, 7–10, 11–15, 16–21 — is assembled with CertLayer.comp and CertLayer.residual directly, as are the fused stage and the head, and inside a group:

• .fwd is that group's forward — no second definition to keep in step;
• .ok is its smoothness hypothesis, conjoined at exactly the right activations by comp rather than written out (the net has 38 relu clauses, counted by MobileNetV4FullBSeal's #guard; none of them is written here);
• .vjp is its HasVJPAt (MobileNetV4FullBVJP.lean chains them); and
• .faithful is its backward-graph faithfulness.

The groups are composed by a prefix chain (mnv4Pre0 … mnv4Pre6), not by one more CertLayer.comp; the section before mnv4Pre0 says why. Mnv4SmoothAt therefore binds one .ok per group plus the stem's clause (eight fields), and no 0 < ε hypothesis, because those live inside the weight records.

The stem sits outside the chain, as EfficientNet-B0's does. CertLayer demands a backward graph, and no render emits a gradient into %x: the artifact's backward ends at the stem conv's weight gradient. So mnv4StemB is a plain function here (cbReluStridedB at the stem's widths), its VJP is cbReluStridedBHasVJPAt, and the net-level VJP composes the two with vjpCompAt.

Conventions this net runs at #

N stays a binder throughout, as at r34/R50. On the data-parallel artifacts the render's N is the per-replica batch and BatchNorm is synchronised across replicas; MobileNetV4SyncB.lean is this file's twin for them: replica r's forward graph denotes shard r of mobilenetv4ForwardBFull (R * N), this file's forward at the global batch. Unlike R50 there is no resolution binder q: the statements are at 224×224.

Rows 4/5/7, 8/10, 12/18, 13/14 and 15/19/20 are shape-identical (same ic, oc, expand, preDWk, postDWk, h), so their UibParams records have the same type and swapping their weights typechecks. Typing pins shape, not identity; what pins identity is the SSA names the forward graph writes (%u4qW vs %u10qW), which is why the graph reads its names from s.p off the table rather than taking them as arguments.

Checked against the committed bytes: verified_mlir/mnv4_fwd.mlir's signature is 234 arguments = %x + 233 parameters, and every name this file writes appears there.

References #

• Qin et al. 2024, MobileNetV4: Universal Models for the Mobile Ecosystem. https://arxiv.org/abs/2404.10518

These are abbrevs, and the rows are named rather than indexed. UibParams (mnv4Blocks[3]!) in a type would force whnf through List.get! at every use; a named reducible constant reduces to its projections directly, which is what lets CertLayer.comp line up 2 * 28 with 56 across a stride join without a single transport.

The #guard below is the whole safety of that move: these 21 constants are pinned to mnv4Blocks — the ONE table mnv4FwdChainB, the backward, the parameter signature and the BN stat list all fold over — so a typo here is a build failure rather than a proof about a different net.

The trunk is built in groups, and that is a proof-engineering requirement. One 24-stage CertLayer elaborates fine — it is the graph faithfulness proof over it that does not: the whole-net rewrite chain produces a term whose kernel check ends in a deterministic timeout. Split at the net's own resolution boundaries, each group's proof is small, and the whole-net theorem is six rewrites over them. The grouping is the ladder a reader already knows — 56, 28, 14, 7 — so it costs nothing in readability and buys a bounded proof.

The seven groups are composed by a prefix chain, not by one more CertLayer.comp.

A mnv4NetLayer := fused.comp (res28.comp (… .comp head)) elaborates fine and reads beautifully. But every downstream statement then has to peel CertLayer.comp to get at .fwd, and at MNv4's LITERAL resolutions that peel is fatal: (L₁.comp L₂).fwd = L₂.fwd ∘ L₁.fwd is rfl, yet discharging it at these instances — by rfl, by simp only [CertLayer.comp_fwd], inside the graph-faithfulness capstone or in a standalone lemma — ends in a (kernel) deterministic timeout. The groups' own five-stage comp chains are fine; it is composing the compositions, under something that can start unfolding, that is not.

So the top level is seven named prefixes and the forward is their nest — ResNet-50's shape at seven stages instead of eighteen. What that costs is the hypothesis bundle: Mnv4SmoothAt binds one .ok per group plus the stem's clause (eight fields) rather than one for the whole trunk. Each group's .ok is still the conjunction CertLayer.comp assembled from its blocks' conditions at their own activations, so the 38 relu clauses are never written down one by one, and no 0 < ε hypothesis appears at all. R50's two apex bundles carry 35 fields.

More generally, a net whose resolutions are literals cannot afford the proof idioms a net with a resolution binder can: ResNet-50's q keeps den stuck, MNv4's 224/112/56/28/14/7 let it run. The stem graph builder's genericity, the prefix chain and the capstone's rw in place of simp only all trace to that.