ConvNeXt-T: [3,3,9,3] @ [96,192,384,768], 28.6 M at K=1000. The DEFAULT everywhere, so every pre-existing call site is unchanged and every committed artifact re-renders byte-identical.

ConvNeXt-S: T deepened — stage 3 goes 9 → 27, dims UNCHANGED. 50.2 M at K=1000.

ConvNeXt-B: S's depth AND a wider net — [128,256,512,1024]. 88.6 M at K=1000. ⚠ B is the size that made the dims a parameter: it shares S's depth table exactly, so anything keying on block count alone cannot tell them apart.

Total ConvNeXt blocks = the reference's totalDrop, i.e. the ramp DENOMINATOR is this minus 1. Derived from the stage table the render traverses, not restated beside it — which is what makes it follow D to 36 at ConvNeXt-S without a second edit.

The ramp index of stage si's block j — the reference's dbi, which counts blocks over the WHOLE net. The single source for the drop-site numbering: the forward calls it walking the stages forwards, the backward walking them backwards, and they cannot disagree.

The number of per-example drop-path scale inputs an SD ConvNeXt render takes: one per block.

The model name a render's banner claims, DERIVED from the stage table it was rendered at.

⚠ A banner is a render's own description of what it did, and the one thing worse than not having one is having one that lies — cnxDropFwdBanner's own note says exactly that about reusing a drop-free banner on an SD artifact. Passing the name as a second parameter beside D would be two writers for one fact, the shape (§2k's α/K, the wx variant marker) that has shipped a real defect in this net three times. So it is read off D.

⚠⚠ It matches on the WHOLE RECORD, not on the block count, and that is not fussiness. This function keyed on cnxDropTotal while ConvNeXt-S was the only new size, and B broke it: B is [3,3,27,3] too, so 36 blocks names S and B alike and every B artifact would have opened by calling itself a ConvNeXt-S. Caught by the guards below, which is why they enumerate all three rather than spot-checking one. An unrecognised table gets a name that SAYS it is unrecognised, rather than falling back to "ConvNeXt-T" the way a getD would.

The %dp<i>: tensor<Bxf32> inputs an SD render appends to its signature — one per block, in ramp-index order, which is the order the driver's dropScales writes them into the blob. Empty when off, which is what keeps every committed artifact byte-identical.

The %one/%zero constants the channel-LN chain binds lnRowF/lnRowBack's SCALAR γ/β to — the real per-channel affine is rowScaleF/rowBiasF downstream, exactly as ViT does it. Emitted once per module body.

⚠ This is the enet zeroBiasPrelude defect one net over (§2m): wire the operand and forget the prelude, and the artifact uses an SSA name nothing defines — iree-compile/XLA say "use of undeclared SSA value name" and nothing before them says anything. It happened HERE too, on the first flag-on render, and regen_verified_mlir.sh check's prelude audit is what generalises.

Does this parameter get weight decay? ConvNeXt's half of the timm rule.

⚠ It is the PLAIN RANK TEST, with no name carve-out, and that is the difference from ViT. The reference's _wd_mask also excludes anything matching _WD_POS_SHAPE, but ConvNeXt has no patch-embedding positional parameter, so its generated reference sets _WD_POS_SHAPE = None and that branch can never fire. Checked in the generated file rather than assumed — carrying ViT's nm != "pos" over would have been a transcription of a rule this net does not have.

What that leaves excluded here: every LN γ/β ([c]), every conv bias, and LayerScale γ (lg, [c]) — which is 1-D and therefore excluded for the same structural reason, not as a special case.

The decayed / excluded split, as the renderer computes it.

allParams is private (it is this file's internal signature source); this is the one thing outside it that legitimately needs the list — tests/TestWdExcludeTie.lean, which must read the SAME names and shapes the renderer chose %wd/%wdz from. Exposing an alias rather than dropping private keeps the surface one definition wide.

@convnext_fwd rendered ENTIRELY from the verified AST — the peer of the train-step render, sharing its forward chain and its 180-parameter signature. Takes %x plus the 180 params in allParams (= func-arg) order (181 inputs) and returns logits [32, 10].

This replaces the independent hand-written string emitter in tests/TestConvNeXtFwd.lean: the forward the driver evals is now the same graph the train step differentiates, by construction rather than by inspection. Because it shares the chain, the emitted body is a byte-identical PREFIX of convnext_train_step.mlir's, ending exactly where the loss begins — which is what scripts/regen_verified_mlir.sh check audits.

The whole-net forward + cotangent + backward traversal, SHARED by the SGD and AdamW renders.

Returns (code, params, softmax): every emitted line; one SSA per parameter — the updated param at adam := false, the un-fused gradient at adam := true; and the softmax SSA, which the AdamW render's report-only %loss reads.

smooth is the cotangent recipe. none → the SGD render's (softmax − onehot)/B, unchanged down to the hand-written %dy divide. some (α, −α/K, B) → the label-smoothed ((softmax − onehot) + α·onehot − α/K)/B composed from kit ops, which is what the AdamW recipe trains on. ConvNeXt already spells the ÷B explicitly (unlike ViT/R34, which fold the mean into lr), so here the smoothing is the only difference between the two cotangents.

Gate on the refactor: convnext_train_step.mlir must come back byte-identical. It does — the softmax is now prettyd on its own line instead of nested inside the .sub so that %loss can read it, but .operand is a leaf that emits nothing, so the fresh-name sequence is unchanged.

ConvNeXt-T (full [3,3,9,3]) SGD train step rendered from the verified AST (except the two documented weight-grad gaps — the stem 4×4/s4 patchify and the even-kernel 2×2/s2 downsample, neither of which has a VJP-cert SHlo op). Every other line is pretty of a verified node: forward + backward cotangent chain + the param-SGD ops, whose output IS the updated param.

The cotangent is plain CE with an explicit ÷B — unlike ViT/R34, which fold the batch mean into lr — so the committed cLR = 0.1 is an effective 0.1, the house convention spelled differently (§2a-quinquies).

The driver's variant slug for a given replica count: the artifact is verified_mlir/convnext_<variant>_train_step.mlir, the entry point is @convnext_<variant>_train_step, and LEAN_MLIR_VARIANT selects it. All three must agree — the shim checks the entry name and refuses a mismatch outright ("entry mismatch") rather than running the wrong graph. The #guards at the bottom pin the literal #eval paths against this.

ConvNeXt has only one batch (32), so unlike mnv2AdamVariant/r34AdamVariant there is no batch suffix — rendering another batch would need cBS to stop being a private constant.

⚠ The EMA renders get their OWN slugs (ema/emadp), for the reason the RMSProp ones do: a render carrying a fourth [θ|m|v|ema] region must never be able to overwrite the artifact the AdamW trainer runs, whose blob has three. That is §2a's last-writer-wins race, and here it would also be an arity mismatch the driver could not survive.

ConvNeXt-T AdamW train step rendered from the verified AST. The certified peer of the hand-written render in tests/TestConvNeXtTrain.lean that convnext-verified-adam trains on.

Same backward as convnext_train_step (convNextBackAll, one traversal) but taking the un-fused gradients, each fed to the proven AdamW triple. The cotangent adds label smoothing (α = 0.1, K = 10); ConvNeXt already spelled the ÷B explicitly, so that is the only difference.

Interface: 545 in (%x, 180 θ, 180 m, 180 v, %lr/%bc1/%bc2, %onehot) / 543 out (180 θ', 180 m', 180 v', %loss/%bc1/%bc2) — positionally identical to the hand-written render, so trainAdamSched's packed [θ|m|v] protocol is unchanged.

What this certifies. As of 2026-07-28 all 180 params are pretty(AST) end to end — the two weight-grad gaps this render used to carry (the stem 4×4/s4 patchify and the even-kernel 2×2/s2 downsample) are closed, by a new cert (flatConvStride4_weight_grad_has_vjp) and an emit-side odd/even padding split (StableHLO.sWGradGeom) respectively. Licensed by convnext-adam-tie against the previously committed hand-written render: bit-exact on all 83,434,629 returned floats, spread 0/180, against a bit-exact A-vs-A floor.

Still outside the AST here, and unchanged: %loss (report-only, no gradient path).

replicas > 1 renders the DATA-PARALLEL variant (handoff §2h-quater) to its own entry name and artifact path via cnxAdamVariant, so producing it can never clobber the one the trainer runs. The only difference is one all_reduce(add)/N per parameter gradient, between the certified gradient and the certified AdamW triple: certified gradient → trusted collective → certified AdamW. See convnextAdamOne for the carve-out.