Concrete verified architectures — the shared specs

Readable layer-list specs that are referenced by both a trainer (Main*Verified) and a proof (LeanMlir/Proofs/*). Kept in this light module (no Mathlib) so the proof side can import the exact object the trainer runs — there's then a single source of truth, and "the spec the trainer runs is the proven one" is literally true, not a twin.

Specs with no proof importing them yet (e.g. resnet34Verified) stay in their own Main*Verified.lean; a spec moves here the moment a proof needs to name it.

structure RmsSchedule : Type

The driver-side half of the MobileNetV2 / EfficientNet RMSProp recipe — peak LR, the exponential decay VerifiedNet.trainAdamSched runs, and the warmup length.

The emitted half (ρ, μ, ε, coupled wd) is Proofs.StableHLO.RmsHyper, which the renderers bake into each graph via rmsConstsBlock. These three do NOT belong there: %lr is a runtime tensor<f32> argument exactly so one render serves a whole schedule, and a learning rate that became a graph constant would be a silent, uncheckable hyperparameter — the RenderCifar8Sgd02 / EfficientNet-16× failure this repo has already paid for twice (handoff §2a-quater, §2a-quinquies). Keeping the two halves in two modules makes that impossible rather than merely discouraged.

It lives here, in the light shared-spec module, for this file's own stated reason: four entry points read it (Imagenette and ImageNet × two nets) and a per-site copy of 0.98 is the double-writer disease at its smallest and most plausible.

⚠ These are the reference's values at the reference's batch 256. Anything else is a different experiment; the Imagenette callers scale lr by batch and say so.

• lr : Float

  learningRate — the peak, at batch 256.

• decayRate : Float

  expLRDecayRate — the multiplier applied once per decayEpochs, after warmup.

• decayEpochs : Float

  expLRDecayEpochs — how many epochs one multiplication spans. ⚠ Not 1 on both nets.

• warmup : Nat

  warmupEpochs — the linear ramp to lr. 5 on both.

def mnv2RmsSchedule : RmsSchedule

MobileNetV2: 0.045 peak, ×0.98 per epoch (jax/MainMobilenetV2Imagenet.lean).

Equations

• mnv2RmsSchedule = { lr := 45e-3, decayRate := 0.98 }

def enetRmsSchedule : RmsSchedule

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).

Equations

• enetRmsSchedule = { lr := 16e-3, decayRate := 0.97, decayEpochs := 2.4 }

def linearVerified : VerifiedNetSpec

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

Equations

• One or more equations did not get rendered due to their size.

def mlpVerified : VerifiedNetSpec

The Chapter-2 MLP: dense 784→512 → relu → dense 512→512 → relu → dense 512→10. Trained by MainMnistMlpVerified; its math VJP is proven in Proofs/SpecVJP.lean (mlpVerified_has_vjp / _at) — both over this object.

Equations

• One or more equations did not get rendered due to their size.

def mlpG (d₁ d₂ : Nat) : VerifiedNetSpec

Width-parametric MNIST MLP dense 784→d₁ → relu → dense d₁→d₂ → relu → dense d₂→10. The canonical mlpVerified is mlpG 512 512. Every instance shares the exact same architecture shape as the proven mlpForward {d₀ d₁ d₂ d₃} (VJP: mlp_has_vjp, which is polymorphic in all four dims), so any (d₁, d₂) is covered by that one theorem — the grid is a single proof instantiated, not a new proof per point. mnist-mlp-grid renders verified_mlir/mlp_{d₁}x{d₂}_{train_step,fwd}.mlir from the faithful renderer at run time and trains on it. Slug mlp_{d₁}x{d₂}.

Equations

• One or more equations did not get rendered due to their size.

def cnnVerified : VerifiedNetSpec

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; its math VJP is proven in Proofs/SpecVJP.lean (cnnVerified_has_vjp_at, folded through conv/maxpool/dense).

Equations

• One or more equations did not get rendered due to their size.

def cnnG (d : Nat) : VerifiedNetSpec

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 d (both hidden FC layers share it), so this is the honest den-certified path; mnist-cnn-grid d renders verified_mlir/cnn_{d}_{train_step,fwd}.mlir and trains on it. Isolates the ROI of the classifier head with the conv stack fixed.

Equations

• One or more equations did not get rendered due to their size.

def cifarVerified : VerifiedNetSpec

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: cifarCnn_has_vjp_at (Proofs/SpecVJP).

Equations

• One or more equations did not get rendered due to their size.

def cifarBnVerified : VerifiedNetSpec

The Chapter-4 CIFAR-10 CNN with per-channel BatchNorm (.bnPerChannel, γ/β per channel) after each conv. Same backbone as cifarVerified + 4 .bnPerChannel layers. VJP: cifarBnVerified_has_vjp (the conditional fold is cifarCnnBn_has_vjp_at).

Equations

• One or more equations did not get rendered due to their size.

def cifar8Verified : VerifiedNetSpec

The deeper 8-conv CIFAR-10 CNN (no BN) — the pedagogical BN-demo backbone: four conv→conv→pool stages, channels [16,16,32,32], 32→16→8→4→2 spatial, then the reused 3-dense head (d1=64): flatten 128 → 64 → relu → 64 → relu → 10. VJP: Proofs.cifarCnn8_has_vjp_at (12 ReLU kinks + 4 maxpools), 3-axiom clean.

Equations

• One or more equations did not get rendered due to their size.

def cifar8Bf16Verified : VerifiedNetSpec

bf16 peer of cifar8Verified — identical net, identical layers, identical parameter layout; the ONLY difference is the slug, which points mkSession at the bf16-rendered artifacts (verified_mlir/cifar8_bf16{,_mom,_adam}_train_step.mlir, emitted by the same renderers with bf16 := true).

⭐ Being a slug change and nothing else is the point: the fp32, fp8 and bf16 arms train the SAME network with the SAME initialisation, so a difference between them is a difference in PRECISION and not in the model. That is what makes the §5.2 optimizer-ordering comparison a controlled one.

⚠ The eval forward (cifar8_bf16_fwd.mlir) is the f32 cifar8_fwd renamed — you train in bf16 and evaluate in f32. ⚠ The bf16 is FORWARD-ONLY (cifar8's backward is on the per-example convBack/dotOut, which have no bf16 twin); see planning/archive/cifar_lowprec_stability.md §4.1.

Equations

• One or more equations did not get rendered due to their size.

def cifar8bVerified : VerifiedNetSpec

cifar8 on the BATCHED op family (cifar8AdamTrainStepFaithfulB). Same net, same layers, same parameter layout as cifar8Verified; only the slug differs, so this trains on verified_mlir/cifar8b_adam_train_step.mlir.

⭐ Its reason to exist is a GATE: the batched and per-example renders denote the same function, so their f32 training runs must agree. Any divergence is a bug in the migration, and it is much cheaper to catch here than inside a bf16 result.

Equations

• One or more equations did not get rendered due to their size.

def cifar8BnVerified : VerifiedNetSpec

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). The pedagogical BN-acceleration demo. VJP: Proofs.cifarCnnBn8_has_vjp_at (12 ReLU kinks + 4 maxpools + 0<εᵢ ×8), 3-axiom clean. Per-channel BN is per-example ⇒ train=eval.

Equations

• One or more equations did not get rendered due to their size.

def cifar8BnG (d : Nat) : VerifiedNetSpec

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 verified_mlir/cifar8_bn_{d}_{adam_train_step,fwd}.mlir (emitted by tests/TestCifar8AdamTrain.lean, D1 parametric). Per-channel BN ⇒ train=eval (no running stats, bnChannels empty). Slug cifar8_bn_{d}.

Equations

• One or more equations did not get rendered due to their size.

def cifar8wVerified : VerifiedNetSpec

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.cifarCnn8_has_vjp_at (the dense bridge is generic in width). Slug cifar8w (render tests/TestCifar8WideTrain.lean).

Equations

• One or more equations did not get rendered due to their size.

def cifar8wbVerified : VerifiedNetSpec

Wide head (d1=512) on the BATCHED op family — the net the §4.3 "Lever 3: precision" sweep trains. Same net as cifar8wVerified (the one Levers 1–2 already measure); only the slug differs, so it loads verified_mlir/cifar8wb_<variant>_train_step.mlir.

⭐ Both the f32 and the bf16 arms of Lever 3 come from THIS slug and ONE renderer (c8wbPacked), differing only in the emit — which is what keeps the lever a controlled comparison. The fp8 arm rides the f32 graph (host-side E4M3), so it needs no artifact of its own; that asymmetry is real and is stated in the lever's text.

Equations

• One or more equations did not get rendered due to their size.

def cifar8wBnVerified : VerifiedNetSpec

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

Equations

• One or more equations did not get rendered due to their size.

def cifar8wbBnVerified : VerifiedNetSpec

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 27 bf16 ops are batched-only), 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.

Equations

• One or more equations did not get rendered due to their size.

def resnet34Verified : VerifiedNetSpec

ch6 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 params (§2l step B: no conv biases). Tied at the FULL spec in Proofs/SpecVJP.lean (resnet34Verified_denote_eq → resnet34Forward_full_pc, + rung E resnet34Verified_fwd_faithful); the honest pointwise VJP is the audited parametric skeleton Proofs.resnet34_has_vjp_at.

Equations

• One or more equations did not get rendered due to their size.

def resnet34ImagenetVerified : VerifiedNetSpec

ResNet-34 on full 1000-class ImageNet — the scale/reference tier (handoff §2k).

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

⚠ Read the claim ceiling before quoting this. The proof-carrying tier stops at Imagenette: this net has no §1a tie, no SpecVJP witness, and no entry in the prefix audit's hand-lists. What it has is provenance — pretty(provenGraph) off the same certified renderer, nClasses and B being ordinary parameters of it — plus whatever the pair agreement shows. The honest sentence is "one architecture, two independent lowerings, agreeing", not "proven".

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.

Equations

• One or more equations did not get rendered due to their size.

ResNet-50 — the bottleneck pair (planning/archive/rsb_a3_r50_verified.md)

⚠⚠ **SKELETON, 2026-08-03. These two specs are the LAYOUT only.** There is no
[`Proofs/Architectures/ResNet50*.lean`](https://github.com/brettkoonce/lean4-mlir/tree/main/LeanMlir/Proofs/Architectures), no `ResNet50RenderB.lean`, no artifact and no rung E —
so nothing renders, trains or is gated off them yet. They exist because the layout is what the
`#guard`s below can check *today*, and because the derived param count is the §2k precondition
that decides whether the JAX pair is meaningful at all. Phases 1–3 of the planning doc are what
make them real. 

def resnet50Verified : VerifiedNetSpec

ch? 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 as of 2026-08-04 (SHlo.maxPool3s2F / the 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].

⚠ The deviation this docstring used to record was 2×2 stride-2, non-overlapping, inherited from resnet34Verified and documented nowhere for as long as the R34 renders existed. It survived because the output shape is identical (112→56), so every structural check in the repo was blind to it and nothing ever failed. Kept in the record because that is the reusable part: a deviation at an unchanged type is invisible to arity, op counts and the prefix audit alike, and only the emitted window separates the two. planning/archive/rsb_a3_r50_verified.md §4b.

Equations

• One or more equations did not get rendered due to their size.

def resnet50ImagenetVerified : VerifiedNetSpec

ResNet-50 on full 1000-class ImageNet — the verified peer of jax/MainResnet50Imagenet.lean, whose RSB-A3 rsb-faithful recipe has already run: 76.66% top-1 / 93.03% top-5 @ ep100. Same backbone as resnet50Verified, head widened to 2048→1000.

⚠ The reference number is at effective batch 2048 (512 micro × 4 grad-accum), and the verified driver has no gradient accumulation. At bs512 the same recipe gives 40.8%, not 78.1% — LAMB is a large-batch optimizer. So a pair run is not comparable until that is settled; planning/archive/rsb_a3_r50_verified.md §3 is the decision.

Equations

• One or more equations did not get rendered due to their size.

def resnet50Imagenet160Verified : VerifiedNetSpec

ResNet-50 on ImageNet-1k at RSB-A3's TRAIN resolution, 160² — the same net as resnet50ImagenetVerified, fed 160² crops. planning/archive/next_session_rsb_a3.md §2.1.

⭐ WHY THIS EXISTS AT ALL IS A WALL-CLOCK ARGUMENT, not a modelling one. §4's probes measured R50 at 376 ms/step (4×bs64, resident, SHIM_WORKERS=8), which puts 100 epochs at 52.3 h at 224 — outside the operator's 40 h bar. At 160 the same 100 epochs is ~31–37 h and fits. So this spec is the difference between A3 being runnable on this box and not.

⚠ EVERYTHING EXCEPT imageH/imageW/slug/shimScript IS IDENTICAL TO THE 224 SPEC, and that is checkable rather than asserted: 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. The #guards under this definition pin exactly that, and are the cheapest possible answer to §2.1's "confirm the 160 spec is the same net".

⚠ The shim is the short recipe's, NOT default's, and that is load-bearing twice over:

• short IS timm's A3 (jax/MainResnet50Imagenet.lean — trainRes := 160, testCropRatio := 0.95, RandAugment m6, mixup 0.1 / cutmix 1.0). default is 224 with RRC+hflip only, so it cannot feed this net at all.
• Jax/Codegen.lean applies trainRes only inside _imagenet_decode_random_crop_flip (the TRAIN path); eval goes through _imagenet_decode_center_crop at the hardcoded _IMG_SIZE = 224. ▶ So this one shim already emits A3's 160/224 SPLIT — 76,800 floats on train, 150,528 on val — which is the answer to §2's open question and the reason §2.3's evalD0 driver change is unavoidable rather than optional.

⚠⚠ DO NOT run this net with eval enabled until evalD0 lands. The driver feeds net.d0 to both invokes, so the val read would pull 150,528 floats into a 76,800-float graph. Use LEAN_MLIR_SKIP_EVAL=1.

Equations

• One or more equations did not get rendered due to their size.

def resnet50Imagenet2018Verified : VerifiedNetSpec

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, and that difference is the entire reason it exists.

⛔ WHY. shimScript is a field on the NET, not on the recipe. Until this spec, the only 224² R50 net pointed at generated_resnet50_imagenet_shim.py — emitted from the default recipe, which is RSB-A2 and calls _randaugment(img, 2, 7.0, 0.5) UNCONDITIONALLY on the train path. A verified 2018 run therefore trained 2018's optimizer and schedule on A2's augmentation: neither recipe, and not comparable to the JAX 2018 number it exists to sit beside. Caught 2026-08-24 as a mean −4.90 top-1 gap against the JAX per-epoch curve over epochs 1–10, and the run was killed at epoch 13.

⚠ scripts/shim_wiring_gate.py CANNOT catch this class — 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 is the substitute: it 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; a fresh slug would orphan them. What changes is the data those artifacts are fed, which is precisely what a shim is.

Equations

• One or more equations did not get rendered due to their size.

def resnet50ImagenetA1Verified : VerifiedNetSpec

ResNet-50 at 224² with RSB-A1's augmentation — the third shimScript on the 224 net, and the one that exists for a SINGLE emitted constant.

⛔ WHY IT EXISTS, and it is a one-line difference that a shared shim would silently erase. A1 differs from A2 in exactly three fields (jax/MainResnet50Imagenet.lean's resnet50ImagenetConfigA1): epochs 300 → 600, weight decay 0.02 → 0.01, and Mixup α 0.1 → 0.2. The first is a driver knob and free. The second is a BAKED stablehlo.constant, so it is a re-render — resnet50in_lambaccdp8x64wxclipbcewd001_train_step, which wdVariantMark keeps on its own path. The third is DATA-SIDE, and this spec is what carries it.

⭐ Measured, not assumed (2026-08-27). The two emitted shims were generated and diffed: generated_resnet50_imagenet_a1_shim.py differs from the default/A2 shim in ONE line — _MIX_A 0.100000 → 0.200000. Everything else is byte-identical. ⚠ And that line reads float(os.environ.get('SHIM_MIXUP_ALPHA', '0.200000')), i.e. the α is also an ENV OVERRIDE on the default shim. Getting A1's mixup that way would "work" and is exactly the failure class this repo has already paid for twice: a knob with no output and no gate is a knob that is silently wrong, and nothing in a 600-epoch run's log would record which α it trained on. A named shim the driver REFUSES to start without is the version that cannot be got wrong.

⚠ The shared slug is deliberate, for resnet50Imagenet2018Verified's reason: the artifacts an A1 run executes are resnet50in_*, and a fresh slug would orphan them. What changes is the data those artifacts are fed, which is precisely what a shim is.

Equations

• One or more equations did not get rendered due to their size.

def mobilenetv2Verified : VerifiedNetSpec

ch7 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: mobilenetv2Verified_denote_eq → mobilenetv2ForwardPaper, + rung E mobilenetv2Verified_fwd_faithful. The VJP fold is at full depth too: Proofs.mobilenetv2_full_has_vjp_at covers stem + all 17 blocks + head. ⚠ It is POINTWISE, and stays that way — relu6 is kinked, so each of the 35 activation sites carries a ≠ 0 ∧ ≠ 6 side condition. Proofs.mobilenetv2_has_vjp_at is the older stem+2-block fold.)

Equations

• One or more equations did not get rendered due to their size.

def mobilenetv2ImagenetVerified : VerifiedNetSpec

MobileNetV2 on full 1000-class ImageNet — the fifth and last scale-tier spec (§2p). 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 needs @mobilenetv2in_fwd_eval with frozen running stats, and its DP evidence comes from shard-check (which carries the 2×52-tensor stat region) rather than the plain duplicated-batch harness.

⚠ §2g's warning applies to this net by name. mobilenetv2_fwd is the artifact that was found to be the WRONG BN WORLD — batch-BN against a per-example-BN train step, so the trainer scored a different net than it trained (logits rel 1.86). That is why the forward pair here is rendered from the same chain the train step differentiates, under its own slug. ⭐ Since 4c leg 2 (2026-09-06) that is literally true for every MobileNetV2 forward: they all come from mnv2FwdChainB, and both forwards are batch-BN because both train steps are.

⚠ Claim ceiling (§5): proofs stop at Imagenette. And the recipe does not match — the reference uses RMSProp at LR 0.045, where this path is AdamW + cosine.

Equations

• One or more equations did not get rendered due to their size.

def efficientnetVerified : VerifiedNetSpec

ch8 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 → efficientnetForwardB_full, batched ∀N, + rung E efficientnetVerified_fwd_faithful); the honest pointwise VJP witness is the representative Proofs.efficientnet_has_vjp.

Equations

• One or more equations did not get rendered due to their size.

def efficientnetImagenetVerified : VerifiedNetSpec

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

⚠ This is the first ImageNet net here with BatchNorm, and that has two consequences the LayerNorm ones did not have: it needs a _fwd_eval artifact (frozen running stats — batch-BN eval is degenerate on a sorted validation split), and its data-parallel evidence cannot come from the plain duplicated-batch harness without the running-stat region, which is 2×49 extra tensors on both sides (§5 — omitting it is refused by the shim's G4 guard, not answered wrongly).

⚠ Claim ceiling (§5): proofs stop at Imagenette; provenance carries. And the recipe does not match — efficientNetB0ImagenetConfig trains with RMSProp and exponential LR decay (×0.97 every 2.4 epochs), where the verified path has AdamW + cosine. That is a bigger optimizer gap than ConvNeXt's or ViT's, and it is on top of the usual missing mixup/cutmix/EMA.

Equations

• One or more equations did not get rendered due to their size.

def convnextVerified : VerifiedNetSpec

ch9 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 → dense. 182 param tensors, 27,827,818 scalars (28,589,128 at K = 1000 — timm.create_model('convnext_tiny')'s count exactly, since the head LN was restored 2026-08-30; it was 180/27,826,282/28,587,592 before, short by 2×768). Tied at the FULL spec in Proofs/SpecVJP.lean (convnextVerified_denote_eq → convNextForwardTCh, the committed channel-LN config, + rung E convnextVerified_fwd_faithful); the full-depth REAL VJP is Proofs.convNextForwardTCh_has_vjp_correct (ConvNeXtFullT.lean:341), whose HasVJP is Proofs.convNextForwardTCh_has_vjp (:270) — GLOBAL, not the pointwise _at form MobileNetV2 is stuck with, because GELU is smooth where relu6 kinks. Its only hypotheses are the 22 LN positivities (stem + 18 blocks + 3 downsamples; there is no head LN). ⚠ Three things above were stale or wrong until 2026-08-12 and all three typeset fine: the LN was described as scalar (§2m made it channel LN on all 22 sites), a head LN was listed that the layer list does not contain, and the VJP pointer named convNextForwardTC_..., a symbol that does not exist. A docstring is not gated by anything.

Equations

• One or more equations did not get rendered due to their size.

def convnextImagenetVerified : VerifiedNetSpec

ConvNeXt-T on full 1000-class ImageNet — the ConvNeXt peer of resnet34ImagenetVerified and vitImagenetVerified (handoff §2p). 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.

⚠ Batch is 32 per device, because cBS is still a private constant in the renderer while nClasses is now a parameter. At four replicas that is global 128 and 10,009 steps/epoch — more steps than the reference's 5,004 at batch 256, which §2d.2 says is the axis accuracy actually tracks. Threading cBS is a separate refactor, not a prerequisite.

⚠ Claim ceiling: the proof-carrying tier stops at Imagenette; what carries here is provenance plus whatever the pair comparison shows (§5).

⚠⚠ This docstring used to end "none of which exist on the verified path", and that was WRONG by four of six as of 2026-08-12 — it contradicted this spec's own dropKeeps note twenty lines below. convNeXtTinyImagenetConfig's extra knobs are mixup 0.8, cutmix 1.0, stochastic depth 0.1, EMA 0.9999, grad clip 1.0 and wdExcludeNormBias, and they land as follows:

• wdExcludeNormBias, grad clip and stochastic depth are RENDER VARIANTS (wx, clip, drop), all three combined in convnextin_adamdpwxclipdrop.
• EMA is a render variant too (convnextin_ema, convnextin_emadp), but it is not combined with the wx/clip/drop stack in any committed artifact, so no single ConvNeXt render carries all five at once.
• Mixup and CutMix are data-side and ride the PRODUCER's SHIM_MIX, never the graph. ▶ The general lesson (chapter_makeover.md §4a-quater): ls verified_mlir/ | grep <marker> before concluding a feature is absent. A missing constructor in the spec language is not evidence, because these are variants, not layers. ⚠ The pipeline augs (RandAugment geometric, random erasing) come across via the shim — as of 2026-08-02. This line used to say "do come across free" and it was a statement about the CAPABILITY: generateShim honoured the flags, but the driver spawned R34's shim for every net, so what this trainer actually streamed was RandomResizedCrop + hflip. See shimScript.

Equations

• One or more equations did not get rendered due to their size.

def convnextSImagenetVerified : VerifiedNetSpec

ConvNeXt-Small on full ImageNet-1k — the second net here added by RESHAPING an existing renderer rather than by writing a new chain, and the cheapest of them.

⭐ S is PURE DEPTH. [3,3,9,3] → [3,3,27,3], dims UNCHANGED at [96,192,384,768]. Where ViT-S needed six width constants turned into a record, ConvNeXt-S needed one Array Nat threaded as a trailing defaulted parameter: the renderer already folded over the stage table in both directions, and because no dimension moves, its hardcoded 96/768 literals (the head and the GAP backward) stay correct untouched. Every ConvNeXt-T artifact re-renders byte-identical, which is what says the parameterisation was inert.

⭐ The proof side needed nothing, for a different reason than ViT's: the certificates here are per-SITE and already generic in c/e/h, so 18 more blocks is 18 more uses of theorems that were never indexed by depth. Depth was not a hypothesis.

342 parameter tensors, 50,222,152 scalars — the published ConvNeXt-S figure, and the count jax/MainConvNeXtSImagenet.lean emits from an independent implementation.

⚠ ImageNet only, deliberately — as with ViT-S. There is no ConvNeXt-S Imagenette peer and this spec does not imply one.

⚠⚠ 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 NOT the Tiny ramp with more entries — it is a steeper ramp over 36 sites. That is exactly why the ramp lives in the SPEC and not in the renderer: the render is sd : Bool and reads its scales from the driver's blob, so a rate change costs no artifact. ▶ The 80-epoch tier wants 0.2, not 0.4 (planning/archive/vit_convnext_sb_scaleup.md: the paper values underfit at 80 epochs) — set it with the driver's LEAN_MLIR_DROP_RATE_U (micro-units: 200000 = 0.2) rather than by editing this line — the rate is data the driver supplies per step, so changing it costs no artifact.

⚠ Nothing has been trained. The artifacts render, the shapes tie, the count is #guarded. No accuracy is claimed and none has been measured.

Equations

• One or more equations did not get rendered due to their size.

def convnextBImagenetVerified : VerifiedNetSpec

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

⚠⚠ B is the size that made the DIMS a renderer parameter. S was pure depth, so it never touched a dimension literal; B moves the stem (96 → 128), the head (768 → 1024) and every stage, which is all ~27 literals the two renderers had hardcoded. Depths and dims are now one Proofs.StableHLO.CnxDims record precisely so that (S depths, T dims) — a net that exists nowhere but type-checks and trains — 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. That is not hypothetical: the renderer's banner function did key on block count, and every B artifact would have introduced itself as a ConvNeXt-S.

342 parameter tensors, 88,589,416 scalars — the same tensor COUNT as S (B widens, it does not add), the published 88.59M, and the count jax/MainConvNeXtBImagenet.lean emits from an independent implementation.

⭐ The proof side needed nothing, and B is better evidence of that than S was: S reused the per-site certificates at the same widths, where B instantiates them at four widths no committed artifact had ever used. They are generic in c/e/h; width was never a hypothesis either.

⚠ Stochastic depth is 0.5 — the ConvNeXt paper's B value at 300 epochs, against S's 0.4 and T's 0.1. Third distinct rate, and still data rather than a render knob.

⚠ Nothing has been trained. Renders, shapes tie, count is #guarded. No accuracy.

Equations

• One or more equations did not get rendered due to their size.

def vitVerified : VerifiedNetSpec

ch10 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 → vitForwardKV depth-12 distinct-param vector-LN, retiring the old weight-shared scalar-LN caveats), with the REAL whole-net VJP vitVerified_has_vjp (all-smooth, 0 < ε only) and rung E vitVerified_fwd_faithful (the depth-12 multi-head vector-LN graph vitFwdGraphKMHV).

Equations

• One or more equations did not get rendered due to their size.

def vitImagenetVerified : VerifiedNetSpec

ViT-Tiny on full 1000-class ImageNet — the ViT peer of resnet34ImagenetVerified, and the scale tier of handoff §2p. 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.

⚠ Claim ceiling, and it is lower here than the name suggests. The proof-carrying tier stops at Imagenette: vitVerified_denote_eq / vitVerified_has_vjp / rung E are stated about the 10-class net. What carries to this one is provenance — the artifacts are pretty(provenGraph) off the same renderer, since nClasses, bs and replicas are ordinary parameters of it — plus whatever a matched-pair comparison against jax/MainVitImagenet.lean shows. Say "one architecture, two independent lowerings, agreeing", never "proven" (§5).

⚠ It is not the DeiT recipe. vitTinyImagenetConfig carries mixup, cutmix, stochastic depth, EMA and grad clipping; none of those exist on the verified path (mixup/cutmix would need soft labels on the shim wire AND a softLabelCE cotangent — this render's is smoothed-CE over a one-hot). ⚠ The pipeline-level augs come across as of 2026-08-02 — RandAugment, random erasing and repeated aug ×3 were all absent in practice until shimScript existed, because the driver spawned R34's shim here. Do not compare a number from this to DeiT-Ti's 72.0%.

Equations

• One or more equations did not get rendered due to their size.

def vitSImagenetVerified : VerifiedNetSpec

ViT-Small on full ImageNet-1k — the first net in this repo added by WIDENING an existing one rather than by writing a new chain.

⭐⭐ Nothing on the proof side was needed. Proofs.vitForwardKV_has_vjp is already ∀ 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 theorem that covers 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, and deliberately. The 10-class vit_* artifacts come from the per-example renderer (ViTRender.lean), which is still pinned at Tiny by ~154 dimension literals. Only the BATCHED renderer was parameterised, and it is the one that writes the ImageNet artifacts. There is no ViT-S Imagenette peer and this spec does not imply one.

⚠ No accuracy has been measured. The artifacts render and the shapes tie; nothing has trained.

Equations

• One or more equations did not get rendered due to their size.

def vitBImagenetVerified : VerifiedNetSpec

ViT-Base (DeiT-B) on full ImageNet-1k. D = 768 = 12 heads × 64, MLP 3072, still depth 12 and still 16×16 patches. Added by handing the renderer a third VitDims; nothing else moved.

⚠⚠ THE "PER-DEVICE BATCH 32" PIN IS LIFTED (2026-08-27). This docstring used to call 32 "a memory fact rather than a recipe choice", on a phase-2 JAX probe that found ViT-B OOM at 4×128 "on these 16 GB cards". The OOM was against 11.68 GiB — the CUDA plugin's BFC memory_fraction = 0.75 default, not the card — and LEAN_MLIR_MEM_FRACTION=0.97 gives 15.11 GiB. Both vitbin_adamdp128x4wxclipdrop* renders execute on four cards at global 512, which IS DeiT's batch: fp32 at 13.99 GiB (93 % of the raised budget, RESOURCE_EXHAUSTED at the default) and bf16 at 12.61. Evidence: runs/2026-08-27-vitb-global512/.

⚠⚠ AND THE 32×4 PAIR IS DELETED, not kept as a fallback. It was global 128 where DeiT's recipe is 512, it applied the reference's batch-512 LR to a quarter of the images that rate was set for, and it was SLOWER per epoch — 291 h against 322 in fp32, 178 against 228 in bf16, both measured. Nothing was left for it to win on. ▶ Consequence: this net has no small-batch render, so LEAN_MLIR_MEM_FRACTION is not optional and runViTBImagenet refuses without it (except on the bf16 twin, which fits the default arena at 10.88 GiB).

⚠ Neither precision has been TRAINED.

Equations

• One or more equations did not get rendered due to their size.

MobileNetV4-Conv-M — the Universal Inverted Bottleneck (planning/archive/mnv4_verified.md)

def mobilenetv4Verified : VerifiedNetSpec

MobileNetV4-Conv-M on Imagenette 224² — the sixth Imagenette net, and the one that makes a point the others cannot: its whole trunk is 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.

⚠ Converted Conv-S → Conv-M on 2026-08-14 (14 UIB blocks → 21, one 1×1 head conv → two, 4.1M → 8.4M at 10 classes), so that mnv4ImagenetVerified below can target the Conv-M number ch6 §6.5 prints. historical/RESULTS.md's 84.58% belongs to the SUPERSEDED Conv-S table and is tagged there as such; this spec has no Imagenette accuracy run of its own yet.

⚠ The two specs move together and cannot diverge: mnv4ImagenetVerified takes its bnChannels from this one and #guards its toSpecs against it. jax/MainMobilenetV4.lean moved in the same commit, because the ties read ITS generated output.

⚠⚠ 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. The only thing that pins the ORDER is scripts/mnv4_forward_tie.py against the JAX reference on shared weights, and the only thing that pins the BACKWARD's dispatch is scripts/grad_tie.py --net mnv4. Same invisibility class as R50's stride-on-the-3×3.

✅ Both ran at the Conv-M table on 2026-09-07 and both pass. Forward max |Δ| = 3.770e-06 over the logits at B = 2 (the Conv-S value was 1.423e-06 — same order); gradient tie 0 of 232 live parameters worse than 10× the reference's own relu-discontinuity floor, in BOTH the raw and the --nokink mode, with the render's worst error (1.281e+00) INSIDE that floor (1.468e+00). Family dispatch, the strided depthwise placement, the two-conv head and the AdamW slot order are all covered.

Equations

• One or more equations did not get rendered due to their size.

def mnv4ImagenetVerified : VerifiedNetSpec

MobileNetV4-Conv-M on full 1000-class ImageNet — the sixth scale-tier spec, built the way resnet50ImagenetVerified was: identical trunk to mobilenetv4Verified, only the head moves (1280→1000).

⭐ This IS Conv-M as of 2026-08-14, so it is now comparable to the chapter's 75.51%. That number comes from the 100-epoch JAX reference behind jax/MainMobilenetV4Imagenet.lean (the run lives OUTSIDE the repo, at /home/skoonce/mnv4_convm_100ep), and this spec is the 1000-class head on the same block table. #guarded at 9,715,512 parameters, the ~9.7M Conv-M is quoted at.

⚠ Comparable is not measured. The blueprint's phase-4 row stays TBD until this spec is actually run, and the blocking item for a printable row is unchanged by the conversion: there is no data-parallel render, so it is single-device and every other ImageNet row was measured at 4×.

⚠ A batch-BN net, so it needs @mnv4in_fwd_eval with frozen running stats. Same pre/post-DW-swap invisibility as its Imagenette peer: toSpecs cannot see the order, so the forward tie is what pins it. ✅ That tie was re-run at the Conv-M table on 2026-09-07 and passes (max |Δ| = 3.770e-06), as did the gradient tie. ⚠ Both 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 they establish about block order carries — but no run has scored THIS net: it has no verified ImageNet training run yet.

Equations

• One or more equations did not get rendered due to their size.