MobileNetV2: 0.045 peak, ×0.98 per epoch, 5-epoch warmup, continuous — the schedule the Imagenette peers train with.

MobileNetV2 on ImageNet (jax/MainMobilenetV2Imagenet.lean): the paper's TF-slim schedule, ×0.98 per epoch as a staircase from step 0 with no warmup.

EfficientNet-B0: 0.016 peak, ×0.97 every 2.4 epochs — the paper's schedule, and the linear scaling of 0.256@4096 down to batch 256 (jax/MainEfficientNetImagenet.lean).

EfficientNet-B0 on ImageNet: TF's schedule, the ×0.97 / 2.4-epoch staircase on the global step with the 5-epoch warmup overriding it while it runs.

The Chapter-1 linear classifier: a single dense 784→10. Trained by MainMnistLinearVerified; its math VJP is proven in Proofs/SpecVJP.lean (linearVerifiedHasVJP) — both over this object.

The Chapter-2 MLP: dense 784→512 → relu → dense 512→512 → relu → dense 512→10. Trained by MainMnistMlpVerified; its folded VJP is mlpVerifiedHasVJPAt in Proofs/SpecVJP.lean, at an input where both ReLU pre-activations are nonzero — both over this object.

Width-parametric MNIST MLP dense 784→d₁ → relu → dense d₁→d₂ → relu → dense d₂→10. The canonical mlpVerified is mlpG 512 512. Every instance has the shape of Proofs.mlpForward {d₀ d₁ d₂ d₃}, whose folded VJP Proofs.mlpHasVJPAt is polymorphic in all four dims, so every (d₁, d₂) is an instance of that one definition. mnist-mlp-grid renders .lake/build/mlp_{d₁}x{d₂}_{train_step,fwd}.mlir (mlirDir, a build product) from the faithful renderer at run time and trains on it. Slug mlp_{d₁}x{d₂}.

The Chapter-3 MNIST CNN (no BN): conv 1→32 → relu → conv 32→32 → relu → maxpool 28→14 → flatten(6272) → dense 6272→512 → relu → dense 512→512 → relu → dense 512→10. Trained by MainMnistCnnVerified; Proofs/SpecVJP.lean ties it to Proofs.mnistCnnNoBnForward (cnnVerified_denote_eq), whose VJP folded through conv/maxpool/dense is Proofs.mnistCnnNoBnHasVJPAt, at an input satisfying its ReLU and max-pool hypotheses (cnnVerifiedHasVJP is the canonical witness).

FC-width-parametric MNIST CNN — the Chapter-3 CNN with the two convs held at 32 channels (so the feature extractor is fixed) and the dense classifier head swept: …maxpool → flatten(6272) → dense 6272→d → relu → dense d→d → relu → dense d→10. The canonical cnnVerified is cnnG 512. The faithful CNN renderer (cnnTrainStepFaithfulV) takes a single dense width d1 (both hidden FC layers share it), so every width renders through that renderer; mnist-cnn-grid d renders .lake/build/cnn_{d}_{train_step,fwd}.mlir (mlirDir, a build product) and trains on it. Isolates the ROI of the classifier head with the conv stack fixed.

The Chapter-4 CIFAR-10 CNN (no BN): conv 3→32 → relu → conv 32→32 → relu → maxpool → conv 32→64 → relu → conv 64→64 → relu → maxpool → flatten(4096) → dense 4096→512 → relu → dense 512→512 → relu → dense 512→10. VJP: Proofs.cifarCnnHasVJPAt (at a smooth point), tied to this spec by cifarVerified_denote_eq in SpecVJP.

The deeper 8-conv CIFAR-10 CNN (no BN), the backbone of the BatchNorm comparison: four conv→conv→pool stages, channels [16,16,32,32], 32→16→8→4→2 spatial, then the 3-dense head (d1=64): flatten 128 → 64 → relu → 64 → relu → 10. VJP: Proofs.cifarCnn8HasVJPAt, at a point off the ten ReLU kinks (eight conv, two dense) and satisfying the four max-pool conditions.

The deeper 8-conv CIFAR-10 CNN with per-channel BatchNorm — cifar8Verified + a .bnPerChannel after each of the 8 convs (γ=1/β=0 init, before relu). VJP: Proofs.cifarCnnBn8HasVJPAt, under 0 < εᵢ ×8, the ten ReLU kinks (eight post-BN, two dense) and the four max-pool conditions. Per-channel BN is per-example ⇒ train=eval.

FC-head-parametric cifar8-BN — the 8-conv per-channel-BN CIFAR net with the conv backbone held at [16,16,32,32] and only the dense classifier head swept: …flatten(128) → dense 128→d → relu → dense d→d → relu → dense d→10. The canonical cifar8BnVerified is cifar8BnG 64. cifar8-bn-grid trains each width via trainAdamSched "adam" on the width-slugged renders .lake/build/cifar8_bn_{d}_{adam_train_step,fwd}.mlir (mlirDir, a build product, emitted by tests/TestCifar8AdamTrain.lean with D1 a parameter). Per-channel BN ⇒ train=eval (no running stats, bnChannels empty). Slug cifar8_bn_{d}.

cifar8Verified with the MNIST-style wide 2×512 dense head (d1=512): flatten 128 → 512 → relu → 512 → relu → 10. Same 8-conv backbone; the head jumps from 13K to 334K floats (whole net 52,858 → 373,626). Same parametric VJP Proofs.cifarCnn8HasVJPAt (the dense bridge is generic in width). Slug cifar8w (render LeanMlir/Proofs/Codegen/CnnRender.lean at d1 := 512).

Wide head (d1=512) on the batched op family — the net chapter 4's "Lever 3: the arithmetic" trains. Same net as cifar8wVerified (the one Levers 1–2 measure); only the slug differs, so it loads verified_mlir/cifar8wb_<variant>_train_step.mlir.

The f32 and bf16 arms of Lever 3 both come from this slug and one renderer (c8wbPacked), differing only in the emit, which keeps the comparison controlled. The fp8 arm runs the f32 graph with host-side E4M3, so it has no artifact of its own.

cifar8BnVerified with the wide 2×512 dense head (d1=512). Slug cifar8w_bn.

cifar8wBnVerified on the BATCHED op family. Slug cifar8wb_bn.

Same net, same 38 parameters, same spec — the layer list is inherited verbatim, which is the point: only the op family the train step is rendered from moves. That is what makes bf16 reachable on the normalized net (the bf16 ops exist only in the batched family), and what keeps the f32-vs-bf16 comparison a controlled one. BatchNorm stays per-example and f32 in both arms, so the eval forward is shared with cifar8w_bn unchanged.

Chapter 5 ResNet-34 on Imagenette 224²: 7×7-s2 stem → BN → relu → maxpool → [3,4,6,3] basic-block stages (per-channel BN, strided downsample at the first block of stages 2–4) → GAP → dense. 110 param tensors (no conv biases: every conv is BN-followed). Tied at the full spec in Proofs/SpecVJP.lean (resnet34VerifiedB_denote_eq → Proofs.resnet34ForwardBFull at batch BN, every batch size, and the forward-graph tie resnet34VerifiedB_fwd_faithful); the pointwise whole-net VJP is Proofs.resnet34ForwardBFullHasVJPAt (ResNet34FullBVJP.lean).

ResNet-34 on full 1000-class ImageNet.

Identical architecture to resnet34Verified; only the head width, the class count and the data source differ. It is run as a matched pair with jax/MainResnetImagenet.lean (same net, same heavy-ball + coupled-L2 recipe, same tfds augmentation via the generated shim).

What is proved about it: the train-step capstone Proofs.ResNet34TieB.r34_net_tiedB binds the class count, so it covers this 1000-class head, at one replica, f32 and batch BatchNorm; the data-parallel step is Proofs.ResNet34SyncTieB.r34_net_syncTiedB. The SpecVJP ties (resnet34VerifiedB_denote_eq, resnet34VerifiedB_fwd_faithful) are stated at 10 classes.

slug is resnet34in so its three artifacts cannot collide with the 10-class ones — the forwards carry no variant in their path and would otherwise overwrite them.

Chapter 5 ResNet-50 on Imagenette 224² — the bottleneck sibling of resnet34Verified: 7×7-s2 stem → BN → relu → pool → [3,4,6,3] bottleneck stages → GAP → dense.

The stem pool is He et al.'s 3×3/s2 (Proofs.StableHLO.SHlo.maxPool3s2F / the Proofs.StableHLO.BatchableOp.maxPool3s2 descriptor, denoting Proofs.maxPool3s2Flat), with symmetric padding 1 — the paper's window [2i−1, 2i+1], not XLA 'SAME''s [2i, 2i+2]. A 2×2/s2 pool has the same output shape (112→56), so no arity or op-count check can tell the two apart; only the emitted window does.

ResNet-50 on full 1000-class ImageNet — the verified peer of jax/MainResnet50Imagenet.lean. Same backbone as resnet50Verified, head widened to 2048→1000.

The reference's RSB-A3 rsb-faithful recipe runs LAMB at an effective batch of 2048 (512 × 4 gradient accumulation). The verified driver accumulates in the acc<k>x<B> variants (VerifiedVariant.accOn, VerifiedVariant.accK), e.g. resnet50in_accdp8x64 and resnet50in160_lambaccdp8x64bce.

ResNet-50 on ImageNet-1k at RSB-A3's train resolution, 160² — the same net as resnet50ImagenetVerified, fed 160² crops, which makes a 100-epoch A3 run shorter than at 224².

Everything except imageH/imageW/slug/shimScript is the 224 spec's: layers is shared by construction below, so toSpecs — hence the 161 tensors and the 25,557,032 params — is derived from the same list. Resolution enters only through d0 = 3·160·160 = 76,800, and the #guards under this definition pin exactly that.

The shim is the short recipe's, not default's:

• short is timm's A3 (jax/MainResnet50Imagenet.lean — trainRes := 160, testCropRatio := 0.95, RandAugment m6, mixup 0.1 / cutmix 1.0). default is 224, so it cannot feed this net.
• Jax/Codegen.lean applies trainRes only inside _imagenet_decode_random_crop_flip (the train path); eval goes through _imagenet_decode_center_crop at _IMG_SIZE = 224. So this shim emits A3's 160/224 split — 76,800 floats on train, 150,528 on val.

Eval runs at 224² through resnet50in160_fwd_eval.mlir, whose %x is tensor<256x150528xf32>; the driver reads the eval width off that artifact and passes it to loadData as evalD0.

ResNet-50 at 224², streaming the 2018 recipe's augmentation. The same net as resnet50ImagenetVerified — same slug, same renders, same artifacts, same d0. The only difference is which shim it streams.

shimScript is a field on the net, not on the recipe. The other 224² R50 spec streams generated_resnet50_imagenet_shim.py, emitted from the default recipe, which is RSB-A2 and calls _randaugment(img, 2, 7.0, 0.5) on every training image. A 2018 run fed that shim would train 2018's optimizer and schedule on A2's augmentation, and would not be comparable to the JAX 2018 number. This spec streams the 2018 shim (random-resized-crop + hflip).

scripts/shim_wiring_gate.py cannot catch a wrong recipe: it checks that each net streams its own shim rather than R34's, and there is no per-recipe slot for it to check. The last #guard below asserts this spec does not carry A2's shim.

The shared slug is deliberate: resnet50in_momdp64_train_step and resnet50in_fwd_eval are the artifacts a 2018 run executes, and a fresh slug would orphan them.

ResNet-50 at 224² with RSB-A1's augmentation — the third shimScript on the 224 net.

A1 differs from A2 in three fields (jax/MainResnet50Imagenet.lean's resnet50ImagenetConfigA1): epochs 300 → 600, weight decay 0.02 → 0.01, and Mixup α 0.1 → 0.2. The epoch count is a driver knob. The weight decay is a baked stablehlo.constant, so it is a separate render — the resnet50in_emalambacc4x128wxclipdropbcewd001 and …accdp4x128…wd001 renders and their bf16 twins, kept on their own paths by Proofs.StableHLO.wdVariantMark. The Mixup α is data-side, and this spec carries it: generated_resnet50_imagenet_a1_shim.py differs from the default/A2 shim in the _MIX_A default, 0.1 → 0.2.

That line reads float(os.environ.get('SHIM_MIXUP_ALPHA', …)), so the α is also an environment override on the default shim. Setting A1's α that way leaves nothing in the run's log recording which α it trained on; a named shim the driver refuses to start without does.

The shared slug is deliberate, for resnet50Imagenet2018Verified's reason: the artifacts an A1 run executes are resnet50in_*, and a fresh slug would orphan them.

Chapter 6 MobileNetV2 on Imagenette 224²: 3×3-s2 stem → BN → relu6 → 17 inverted-residual blocks (full-paper [t,c,n,s] config, strided depthwise downsamples, per-channel BN, relu6, linear bottleneck) → 1×1 head conv (320→1280) → BN → relu6 → GAP → dense. Tied at the full paper spec in Proofs/SpecVJP.lean: mobilenetv2VerifiedB_denote_eq → Proofs.mobilenetv2ForwardBFull at batch BN, every batch size, and the forward-graph tie mobilenetv2VerifiedB_fwd_faithful. The whole-net VJP is Proofs.mobilenetv2ForwardBFullHasVJPAt (MobileNetV2FullBVJP.lean): stem, all 17 blocks and the head, pointwise — relu6 is kinked, so each of the 35 activation sites carries a ≠ 0 ∧ ≠ 6 side condition at every example.

MobileNetV2 on full 1000-class ImageNet. Identical architecture to mobilenetv2Verified; only the head moves (1280→1000), which takes the count to the JAX reference's 3,504,872.

A batch-BN net, so it scores through @mobilenetv2in_fwd_eval with frozen running stats, and its data-parallel check is shard-check (which carries the 2×52-tensor stat region) rather than the plain duplicated-batch harness.

Every MobileNetV2 forward, eval included, is rendered from Proofs.StableHLO.mnv2FwdChainB, the chain the train step differentiates, and both forwards are batch-BN because both train steps are; a forward from a different chain would score a different net than the one trained.

What is proved about it: the train-step capstone Proofs.MobileNetV2TieB.mnv2_net_tiedB binds the class count, so it covers this 1000-class head, at one replica, f32 and batch BatchNorm; the data-parallel step is Proofs.MobileNetV2SyncTieB.mnv2_net_syncTiedB. The SpecVJP ties are stated at 10 classes. The optimizer follows the variant: the rms* renders (the shipping rmsdp64bf16) are the reference's RMSProp at LR 0.045 with its warmup and ×0.98 exponential decay; the adam* renders are AdamW.

Chapter 7 EfficientNet-B0 on Imagenette 224²: 3×3-s2 stem → 16 MBConv blocks ([t,c,n,s,k] B0 config; expand 1×1 [skip when t=1] → depthwise k×k → squeeze-excite → project 1×1, all BN + swish) → 1×1 head (320→1280) → GAP → dense. 213 param tensors, 4,020,358 scalars (the 1000-class peer below is 5,288,548, i.e. B0's canonical 5.29M). The 16 mbConvSE ic mid oc r k args are the B0 generator unrolled (mid=t·ic, r=ic/4, ic threads stage→stage). Tied at the full spec in Proofs/SpecVJP.lean (efficientnetVerified_denote_eq → Proofs.efficientnetForwardBFull, batched ∀N, and the forward-graph tie efficientnetVerified_fwd_faithful); the full-depth VJP is Proofs.efficientnetForwardBFullHasVJP (global; its only hypotheses are the 0 < ε positivities, Proofs.B0Weights.EpsPos).

EfficientNet-B0 on full 1000-class ImageNet — the EfficientNet peer of the R34, ViT and ConvNeXt ImageNet specs. Identical architecture to efficientnetVerified; only the head moves (1280→1000), which takes the count to the JAX reference's 5,288,548.

A BatchNorm net, which has two consequences the LayerNorm nets do not: it needs a _fwd_eval artifact (frozen running stats — batch-BN eval is degenerate on a sorted validation split), and its data-parallel check needs the running-stat region, 2×49 extra tensors on both sides (omitting it is refused by the shim's G4 guard).

⚠ Claim ceiling (§5): proofs stop at Imagenette; provenance carries. The recipe follows the variant: the emarmsdp64dropdo* renders (the shipping one is emarmsdp64dropdobf16) carry the reference's RMSProp with ×0.97-every-2.4-epoch decay, EMA, drop-connect and classifier dropout, as efficientNetB0ImagenetConfig trains; the adam* renders are AdamW + cosine.

Chapter 8 ConvNeXt-T on Imagenette 224²: 4×4-s4 patchify → [3,3,9,3] ConvNeXt blocks @ [96,192,384,768] (depthwise 7×7 → channel-LN → 1×1 expand → GELU → 1×1 project → layerScale) with 3 between-stage (LN + 2×2-s2) downsamples (56→28→14→7) → GAP → LN → dense. 182 param tensors, 27,827,818 scalars (28,589,128 at K = 1000 — timm.create_model('convnext_tiny')'s count). Tied at the full spec in Proofs/SpecVJP.lean (convnextVerified_denote_eq → Proofs.convNextForwardTCh, the channel-LN net, and the forward-graph tie convnextVerified_fwd_faithful); the full-depth VJP is Proofs.convNextForwardTChHasVJP, with correctness theorem Proofs.convNextForwardTChHasVJP_correct (ConvNeXtFullT.lean). It is global rather than pointwise, because GELU has no kink. Its only hypotheses are the 23 LN positivities (stem + 18 blocks + 3 downsamples + the head LN).

ConvNeXt-T on full 1000-class ImageNet — the ConvNeXt peer of resnet34ImagenetVerified and vitImagenetVerified. Identical architecture to convnextVerified; only the head moves (768→1000), which is what takes the count to timm's 28,589,128.

Data comes from the generated tfds shim, so this side does no augmentation at all. The committed data-parallel renders take 64 examples per replica (%x : tensor<64x150528xf32>), global 256 at four replicas, the reference's batch.

What is proved about it: the train-step capstone Proofs.CnxTiePoCGB.cnx_net_tiedGB binds the class count, so it covers this 1000-class head, at one replica, in f32, on the chain without drop-path. The SpecVJP ties are stated at 10 classes.

convNeXtTinyImagenetConfig's extra knobs — mixup 0.8, cutmix 1.0, stochastic depth 0.1, EMA 0.9999, grad clip 1.0 and wdExcludeNormBias — land as follows:

• wdExcludeNormBias, grad clip and stochastic depth are render variants (wx, clip, drop), combined in convnextin_adamdpwxclipdrop.
• EMA is a render variant too (convnextin_ema, convnextin_emadp), and convnextin_emadpwxclipdropbf16 carries it together with wx, clip and drop.
• Mixup and CutMix are data-side and ride the producer's SHIM_MIX, never the graph. These are variants, not layers, so a feature can be present with no constructor for it in the spec language: check verified_mlir/ for the variant marker. The pipeline augmentations (geometric RandAugment, random erasing) come from this net's own shim (shimScript).

ConvNeXt-Small on full ImageNet-1k — ConvNeXt-T deepened: [3,3,9,3] → [3,3,27,3], dims unchanged at [96,192,384,768]. The renderer takes the depth table as a parameter (Proofs.StableHLO.CnxDims), and the per-site certificates are generic in c/e/h and not indexed by depth, so the 18 extra blocks are further uses of the same theorems.

344 parameter tensors, 50,223,688 scalars (the #guards below), the published ConvNeXt-S size of 50.22M.

ImageNet only: there is no ConvNeXt-S Imagenette peer.

The stochastic-depth rate is the one recipe knob that moves with size, and it is data. The ConvNeXt paper uses 0.4 for S at 300 epochs against T's 0.1, so dropKeeps below is a steeper ramp over 36 sites, not the Tiny ramp with more entries. The render reads its drop scales from the driver's blob, so a rate change costs no artifact: LEAN_MLIR_DROP_RATE_U (micro-units, 200000 = 0.2), read by the ConvNeXt-S entry point (apps/imagenette/MainConvNeXtSImagenet.lean), overrides it per run.

No accuracy has been measured: the artifacts render, the shapes tie and the count is #guarded.

ConvNeXt-Base on full ImageNet-1k — ConvNeXt-S's depth at [128,256,512,1024].

B moves the stem (96 → 128), the head (768 → 1024) and every stage width, so the renderer's depths and dims are one Proofs.StableHLO.CnxDims record: a net with S's depths and T's dims cannot be spelled.

B shares S's depth table exactly ([3,3,27,3], 36 blocks), so anything keying on block count cannot tell them apart.

344 parameter tensors, 88,591,464 scalars (the #guards below) — the same tensor count as S (B widens, it does not add), and the published 88.59M. The per-site certificates are generic in c/e/h, so B instantiates them at its four widths.

Stochastic depth is 0.5 — the ConvNeXt paper's B value at 300 epochs, against S's 0.4 and T's 0.1 — and is data, not a render knob.

Nothing has been trained: the artifacts render, the shapes tie and the count is #guarded.

Chapter 9 ViT-Tiny on Imagenette 224² (patch-16): 16×16-s16 conv patch embed (3→192, →196 patches), learned CLS token + positional embed (→197 tokens), 12 pre-norm transformer blocks (dim 192, 3 heads, MLP 768), final per-channel LayerNorm, CLS-slice dense head 192→10. 200 params. Tied at the full spec in Proofs/SpecVJP.lean (vitVerified_denote_eq → Proofs.vitForwardKV at depth 12 with distinct per-block parameters and vector LN), with the whole-net VJP vitVerifiedHasVJP (global, 0 < ε only) and the forward-graph tie vitVerified_fwd_faithful (the depth-12 multi-head vector-LN graph Proofs.StableHLO.vitFwdGraphKMHV).

ViT-Tiny on full 1000-class ImageNet — the ViT peer of resnet34ImagenetVerified. Identical architecture to vitVerified above; the head is the only thing that moves (192→1000), exactly as the two ResNet-34 specs differ only in theirs.

Data comes from the generated tfds shim (VerifiedData.imagenet), so this side does no augmentation at all — one definition of the transform, and it is the reference's.

What is proved about it: the train-step capstone Proofs.ViTTiePoCGB.vit_net_tiedGB binds the class count, so it covers this 1000-class head, at one replica, in f32, on the chain without drop-path. vitVerified_denote_eq, vitVerifiedHasVJP and vitVerified_fwd_faithful are stated at 10 classes. The matched-pair reference is jax/MainVitImagenet.lean.

The recipe follows the variant. The shipping emadp128x4wxclipdropbf16 (bf16, with drop-path, so outside the capstone's scope) carries the rest of vitTinyImagenetConfig: EMA, grad clip 1.0, drop-path (24 host-drawn masks), weight decay off norm/bias, and mixup/cutmix, which ride the producer's SHIM_MIX (this shim bakes both) as soft targets on the wire; the render's cotangent smooths that mixed target (α = 0.1). The pipeline-level augmentations (RandAugment, random erasing, repeated aug ×3) come from this net's own shim (shimScript). The remaining differences from DeiT-Ti (clip, EMA-scored eval, LN eps, tanh GELU) are listed in planning/imagenet_parity.md.

ViT-Small on full ImageNet-1k — ViT-Tiny widened.

Proofs.vitForwardKVHasVJP is stated for all heads d_head mlpDim k, and it is a global HasVJP rather than the pointwise _at form the ReLU-family nets carry, because GELU/softmax/LayerNorm have no kink. So S is covered by the same definition as Tiny, at different arguments.

S is Tiny widened and nothing else: D = 384 = 6 heads × 64 against Tiny's 192 = 3 × 64, MLP 1536 against 768. Same depth (12), same 16×16 patch grid (196 tokens + CLS), same block structure. d_head stays 64 — ViT widens by adding heads.

ImageNet only: there is no ViT-S Imagenette peer.

No accuracy has been measured: the artifacts render and the shapes tie.

ViT-Base (DeiT-B) on full ImageNet-1k. D = 768 = 12 heads × 64, MLP 3072, still depth 12 and still 16×16 patches — a third Proofs.StableHLO.VitDims for the same renderer.

The two vitbin_adamdp128x4wxclipdrop* renders run on four cards at global 512, DeiT's batch. The fp32 render needs the PJRT allocator fraction raised (LEAN_MLIR_MEM_FRACTION=0.97, 15.11 GiB; the default 0.75 gives 11.68 GiB), and runViTBImagenet refuses to start the fp32 render without it; the bf16 twin fits the default arena. There is no smaller-batch data-parallel render.

Neither precision has been trained.

MobileNetV4-Conv-M on Imagenette 224² (the book's MobileNetV4 side quest, chapter 6) — a trunk built from one parameterised block. uib's k = 0 omits a depthwise, so the same constructor renders all four MNv4 families — ExtraDW (both DWs), IB / MBConv (post only), ConvNeXt-like (pre only) and FFN (neither) — and the fused stage is the only other block form in the net. 21 UIB blocks, 233 parameter tensors, 8,447,322 parameters (the #guards below). This spec has no Imagenette accuracy run of its own.

The two MNv4 specs move together: mnv4ImagenetVerified takes its bnChannels from this one and #guards its toSpecs against it. jax/MainMobilenetV4.lean is the reference the ties read.

A pre/post-DW swap is invisible to everything in this file: same k, same channels ⇒ same toSpecs, so the #guards below pass on a spec that swaps them, and at stride 1 both positions are shape-preserving so the types pass too. What pins the order is scripts/parity/mnv4_forward_tie.py against the JAX reference on shared weights, and what pins the backward's dispatch is scripts/parity/grad_tie.py --net mnv4. R50's stride-on-the-3×3 is invisible in the same way.

The net is timm 1.0.28's mobilenetv4_conv_medium: stride on the post-DW, a BN-only pre-DW, a ReLU stage 0, GAP before conv_head, a symmetric stem. Three gates check it: scripts/parity/mnv4_timm_parity.py (the JAX reference against timm, logits to 1.5e-5 relative); scripts/parity/mnv4_forward_tie.py (this render against the JAX reference, max |Δ| = 1.767e-05 at B = 2); scripts/parity/grad_tie.py --net mnv4 --nokink at B = 8 (0 of 201 live parameters worse than 10× the control; the two precision-limited head parameters are exempt there and checked by the default mode).

MobileNetV4-Conv-M on full 1000-class ImageNet — identical trunk to mobilenetv4Verified, only the head moves (1280→1000). #guarded at 9,715,512 parameters, the ~9.7M Conv-M is quoted at.

The chapter's 75.48% top-1 from the 100-epoch JAX reference behind jax/MainMobilenetV4Imagenet.lean was measured on an earlier transcription that differed from timm's; it is a target for this spec, not a comparison. This spec has no verified ImageNet training run.

What is proved about it: the train-step capstone Proofs.Mnv4TieB.mnv4_net_tiedB binds the class count, so it covers this 1000-class head, at one replica, f32 and batch BatchNorm; the data-parallel step is Proofs.MobileNetV4SyncTieB.mnv4_net_syncTiedB. Data-parallel renders: mnv4in_adamdp64 (and its bf16 twin) and mnv4in_emaaccdp8x128wxdowd005bf16.

A batch-BN net, so it scores through @mnv4in_fwd_eval with frozen running stats. It has its Imagenette peer's pre/post-DW-swap invisibility: toSpecs cannot see the order, and the forward and gradient ties (see mobilenetv4Verified) run against the Imagenette render (@mnv4_fwd, 10 classes). This spec differs from it only in the classifier, which the #guards below pin, so what those ties establish about block order carries to it.