A BatchNorm layer's running-statistic slots %{nm}mu, %{nm}var, each [c], μ before var — the order the driver packs runningBnStats in. Every render's stat signature is built from this one pair: a misaligned slot keeps the arities and silently feeds the wrong layer's statistics.

Does this parameter get weight decay? timm's no_weight_decay rule, and it is the PLAIN RANK TEST with no name carve-out — every 1-D parameter is excluded: BN γ, BN β and every bias. The wx renders bind the excluded parameters' decay operand to %wdz (wdNameBy).

Every net with no positional parameter uses it (ResNet, MobileNet, EfficientNet, ConvNeXt): the rule is timm's, not the net's. ViT's vitWdDecays adds its nm != "pos" carve-out, which is why the predicate takes the name it ignores here.

rankWdDecays minus the depthwise kernels — TF-slim's rule for MobileNetV2. mobilenet.training_scope puts slim.l2_regularizer(weight_decay) on slim.conv2d (the stem, every expand / project 1×1, the 1280 head and the logits) and weights_regularizer=None on slim.separable_conv2d, which is what expanded_conv builds its depthwise from (conv_blocks.py); BN and biases carry no regularizer. A depthwise kernel is [C, 1, k, k]: rank 4 with one input channel and more than one output — the same test VerifiedConfig.dwFanK2 uses, and the JAX _wd_mask's wdExcludeDepthwise leaf test. The wxdw renders bind these to %wdz too (imagenet_parity.md D11).

rankWdDecays plus the biases — TF TPU EfficientNet's rule. main.py adds weight_decay · Σ l2_loss(v) over every trainable variable whose name lacks 'batch_normalization', so the BN γ/β alone are exempt: the squeeze-excite biases, the classifier bias and (under convBias) the conv biases decay along with every kernel, the depthwise included. The rank cannot tell a bias from a γ, so this reads the NAME the renderer gave the parameter: EfficientNet's BN scales end in g (sg, b2eg, hg) and its shifts in bt (sbt, b2ebt, hbt); no bias does (zb1, zb2, bd, sb, b2eb). EfficientNetRender.Basic guards the counts on its own signature. The wn renders bind only the BN parameters to %wdz; the JAX peer is _wd_mask's structural form (wdDecayBiases).

The decay operand for one parameter: the real %wd, or the zero constant when wdExclude is on and decays excludes it.

The variant marker for a BatchNorm ε other than the committed 1.0e-5, in the wd/ls decimal grammar (first digit the integer part): eps0001 is 1e-3, the TF papers' value (MobileNetV2 in slim, EfficientNet). ε is baked into every BN site of the train step AND of the eval forward, so a different ε is a different pair of artifacts: the train step's entry carries the marker, and the eval forward it scores through is <slug>_fwd_eval_<marker> (VerifiedVariant.evalTag reads it back).

The variant marker for the form of the GELU: nothing for the tanh approximation, whose names are the committed ones, and erf for the exact x · Φ(x). It sits after the ε marker and before bf16 (emadp128x4wxclipdropeps0000001erfbf16, emadpwxclipdroperfbf16). The form is baked into every GELU site of the train step and of the forward, so an exact-GELU train step scores through an exact-GELU forward: its own <slug>_<variant>_fwd, else <slug>_erf_fwd (VerifiedVariant.erfOn reads the marker back, checkGeluWorld refuses a mixed pair).

@<slug>_fwd_eval, or @<slug>_fwd_eval_<marker> at a non-default ε (an artifact's entry is its file name).

The banner clause of a train step: which of its lines are not pretty of a node. acc adds the accumulation β scalars, which the render computes from %aup by hand; hand names any further hand-written block, followed by ", " (ConvNeXt's GAP backward).

The banner of a sync-BN data-parallel train step, after its title line: every gradient and update op is pretty of a node, the all-reduce blocks included; BN is synchronised; and the step is the single-device step at the global batch, proved as tieThm (the all-reduced gradients) and fwdThm (the forward), both in LeanMlir/Proofs/Nets/<dir>/. Scope notes the statements leave out (drop-path masks, accumulation, bf16: syncBnBf16WgradNote / syncBnBf16TwinsNote) follow it, from the caller.

The sync-BN banner's bf16 note for the nets whose conv weight gradients have a sharded bf16 statement (ResNet, Proofs.den_allReduceMeanF_convWeightGradBBf16_sub_global): only the weight gradient's rounding differs from one device's.

The sync-BN banner's bf16 note for the nets with no such peer (depthwise and XLA-strided convs: MobileNetV2, MobileNetV4, EfficientNet): the bf16 twins are outside the statement.

The %wdz declaration an excluding render needs. Emitted only when the flag is on, so at wdExclude := false not one byte moves and every committed artifact is untouched. params names which parameters take it, in the banner comment only.

The optimizer's name in an artifact's banner.

The optimizer's marker in a variant slug, with the data-parallel dp placed the way every net spells it: adam/adamdp, rms/rmsdp, mom/momdp, sgd/sgddp, lamb/lambdp.

k is IN THE NAME for the accumulating recipes (acc4x, accdp4x) because the driver has to know it (to decide which micro-batch applies) and the graph has it baked (in %ob1/%ob2). Two places, and a disagreement between them is silent: the run would apply on a cadence the 1/k does not match, i.e. a wrong effective learning rate with no error anywhere. Carrying k in the artifact NAME makes the driver read it off the same string that selects the file.

The %aup-driven scalar block that turns ONE graph into both accumulation phases.

ONE WRITER, shared by .adamwAccum and .lambAccum. These eleven lines are the whole accumulate/apply mechanism; one definition keeps the two optimizers from carrying two copies of it.

accumulate (%aup = 0):  β₁ = 1, (1−β₁) = 0  ⇒  m' = m,  v' = v   exactly
apply      (%aup = 1):  β₁ = 0.9, (1−β₁)/k  ⇒  m' = 0.9·m + (1−β₁)·(Gt/k)

1/k is folded in HERE, and asymmetrically: %ob1 carries 1/k while %ob2 carries 1/k², because v consumes the gradient SQUARED. v' = β₂v + ((1−β₂)/k²)·Gt² = β₂v + (1−β₂)·(Gt/k)² — the identity that makes accumulation equal a real large-batch step rather than the "mean of per-micro-batch second moments" a naive implementation produces.

fmt12, not fmt6: at k = 4, (1−β₂)/k² = 6.25e-5, and fmt6 emits 0.000063 — 0.8% wrong, baked, in the optimizer.

β₁/β₂ are 0.9/0.999 for BOTH optimizers (LAMB's moments ARE Adam's), which is why this block needs no per-optimizer parameter. Only %eps/%wd differ, and those stay in optConstsB.

Is this parameter in timm's no_weight_decay group?, recovered from the ONE name wdNameBy produces rather than passed alongside it.

Derived and not a second argument, on purpose. The skip-list controls TWO things — whether the decay term enters r (%wdz) and whether the trust ratio applies at all — and a caller threading a Bool beside the name is exactly the two-writers shape that lets them disagree: a parameter decayed but not adapted, or the reverse. One name, one predicate, both consumers downstream of it.

(θ', m', v') for one parameter, from its un-fused gradient.

For .adamw the three ops are the proven adamMNextF/adamVNextF/adamWParamF (adamW_triple_faithful bundles their dens into Proofs.adamWStep by rfl). β₁/β₂/ε/wd are baked literals; %lr/%bc1/%bc2 are runtime tensor<f32> args, so one render serves a whole LR schedule. For .heavyBall see the inline notes — same discipline, different three ops, and m becomes a passthrough so the packed signature does not move. For .rmsprop the buffer is returned in the m slot and the mean-square in v.

At replicas > 1 the gradient is first averaged across devices by prettyAllReduceMean — pretty of the allReduceMeanF node, whose den is the replica MEAN of the per-replica gradient nodes (den_allReduceMeanF). The optimizer tail consumes the averaged gradient as an .operand, exactly as it consumes the raw one. What stays trusted is the lowerer's all_reduce, as every op's lowering is, so the collective has its own numeric check: the DP render is SYNC-BN (bnFwdSite/bnBackSite/ bnGammaSite), so the data-parallel step at 2×32 should equal the single-device step at 1×64 on every output region, and resnet34-syncbn-check checks that numerically.

At replicas ≤ 1 this emits nothing and threads the raw gradient, so the single-device render stays byte-identical — which is the cheap self-check that this insertion is inert.

How many micro-batches the optimizer accumulates over — k for the two accumulating constructors and 1 for every other, so a caller can ask the question without a second match that could disagree with accOn's.

It exists for the CLIP (clipNormStr/clipEpsStr below), which is the first feature whose emitted constants depend on k from OUTSIDE accumScalarConsts.

The clip threshold as the render bakes it, k·C — and the k is not a typo.

THE REFERENCE CLIPS THE MEAN ACCUMULATED GRADIENT, NOT THE MICRO-BATCH ONE. emitLossAndTraining in jax/Jax/Codegen.lean is unambiguous about the order:

grads = jax.tree.map(lambda _a: _a / _K, _gsum)   # the MEAN over k micro-batches
loss  = jnp.mean(_ls)
gn    = jnp.sqrt(sum(jnp.sum(g * g) for g in jax.tree.leaves(grads)))
grads = jax.tree.map(lambda g: g * jnp.minimum(1.0, C / (gn + 1e-6)), grads)

This render never materialises that mean: optOne's accumulator carries the SUM Gt, and the 1/k is folded into %ob1 = (1−β₁)/k and %ob2 = (1−β₂)/k² downstream (accumScalarConsts, and it is split that way because v is QUADRATIC in the gradient). So the fold here runs on Gt, whose norm is k·‖mean‖, and the threshold must move with it:

min(1, kC / (‖Gt‖ + k·ε)) = min(1, C / (‖Gt‖/k + ε))

— the reference's factor on the mean, exactly, with no new op and no division emitted. And the factor is then applied to Gt rather than to the mean, which is the same thing for the same reason: scaling commutes with the 1/k the moments fold in afterwards.

fmt12, not fmt6, for accumScalarConsts' stated reason — these are baked literals in the optimizer, where nothing downstream would question a truncated one. At k = 1 this is the identity and emits the plain threshold.

The clip's ε, scaled by the same k and for the same reason — see clipNormStr.

It is NOT cosmetic and it does not cancel: the reference's + 1e-6 is what keeps the factor from being 0/0 at a zero gradient (Proofs.clipDenom_pos), and leaving it unscaled while the numerator scales would shift the factor by k in exactly the regime the guard exists for.

The rank-0 zero that seeds the global-norm fold. Its own name rather than %lzero: that one exists only under the two LAMB constructors (optConstsB), and the clip is an independent axis that has to work over .adamw too. Emitted only when the flag is on, so at gradClip := false not one byte moves and every committed artifact is untouched — the same discipline wdzConst keeps.

The weight decay each optimizer bakes when the caller does not override it.

The two families genuinely differ, and by 200×: AdamW's 1e-4 against LAMB's 0.02, the latter off timm's a3 arg string (lamb-cosine-lr0.008-wd0.02-…). optConstsB's .lamb arm records what reusing AdamW's number here would produce — a LAMB that is structurally right and 200× off on the decay.

It exists so that wdStr can mean "the optimizer's own value" by DEFAULT rather than by the caller restating a number that is already decided by the constructor.

The decay actually baked: the caller's override, or optWdDefault. Empty means default.

%wd IS A BAKED stablehlo.constant, NOT A RUNTIME OPERAND — this parameterises the literal, it does not make the decay schedulable. Unlike %lr, which stays a tensor<f32> argument so one graph serves a whole cosine, changing the decay is a RE-RENDER. That is the same shape ConvNeXtRender.convnextAdamConsts already has (wdStr := "0.0001", with the ImageNet render passing 0.05), copied rather than re-invented.

Why it exists: RSB-A1 uses wd = 0.01 where A3 uses 0.02, so A1 costs a re-render rather than a new op.

The variant marker for a NON-DEFAULT decay, and it is not optional bookkeeping.

Two renders that differ only in a baked constant MUST NOT share a path. %wd lives in the artifact, so an A1 render (0.01) and an A3 render (0.02) at the same optimizer, batch and replica count would otherwise both be lambaccdp8x64wxclipbce, and the last writer would win. scripts/regen_verified_mlir.sh check would catch it as a two-writer collision, but a collision that cannot be SPELLED is better than one that is merely detected.

Spelling: wd ++ the digits with the point removed, so 0.01 → wd001 and 0.005 → wd0005. Mechanical, and unambiguous because the leading 0 is kept. Empty at the default, so every committed artifact keeps its name and its bytes.

The label-smoothing marker, wdVariantMark's peer and there for the identical reason: α is BAKED into the smoothed-CE cotangent, so two renders differing only in it would collide on one artifact path. Empty at the default 0.1, so every committed spelling is unchanged. ls0, not ls0000000: fmt6 0.0 is "0.000000" and stripping its point leaves seven zeros, so OFF gets the short spelling it deserves and any other α keeps the general one. The #guards in ResNet34RenderB pin that. It must reach r34AdamVariant and not merely the renderer — the rule wx, clip and bf16 each state there: an artifact whose declared entry disagrees with its own path is refused by the shim outright.

The WHOLE optimizer stage for a net: the hoisted global-norm clip, then optOne per parameter. Returns (code, θ', m', v', G', E'), with G' empty unless the optimizer accumulates and E' empty unless ema. The two are INDEPENDENT — see VerifiedVariant.nRegions for the region count.

THIS IS A FUNCTION SO THAT THE ONE-STEP GATE CAN DRIVE THE SHIPPED PATH. The one-step optimizer gate — one step of each optimizer on the same (θ, g, state) — needs the optimizer stage ALONE, and a second copy of it written for the gate would gate a transcription rather than the emission. tests/TestOptStepFixtures.lean calls exactly this.

THE ORDER IS THE SEMANTICS, and there are two orderings to get right, not one.

① the clip goes AFTER the all_reduce. Each replica holds a PARTIAL gradient; clipping those and then averaging is a clip of nothing in particular. optOne all-reduces per parameter, so under the clip the collective is hoisted here and optOne is told (preAvg) not to repeat it. ② the clip goes AFTER the ACCUMULATION. The reference is explicit (emitLossAndTraining in jax/Jax/Codegen.lean): grads = _gsum / _K and only THEN the clip line, so the norm is of the MEAN over the k micro-batches. Clipping the micro-batch gradient instead would clip k times per optimizer step against a threshold meant for their mean — again something that trains and descends. So the accumulator is hoisted here too, and the threshold moves to k·C to read the fold on Gt as a fold on Gt/k (clipNormStr).

Neither ordering is visible to a gate that only checks "the gradients got smaller", which is why Proofs.clipFactor_shared is the statement to drive and why it must be driven in the CLIPPING regime — the identity-below-threshold gate is structurally blind to placement.

At gradClip := false NOT ONE pretty CALL happens in the clip block, so the fresh-name counter does not move and every committed artifact re-renders byte-identically.

The optimizer's baked constants. .adamw is byte-for-byte the committed block; .heavyBall emits only what it reads, so there are no dead constants in the momentum artifact.

%wd is baked rather than a runtime arg because weight decay is not scheduled — unlike %lr, which stays a tensor<f32> argument so one graph serves the whole cosine schedule.

.rmsprop bakes the net's own rms (mnv2RmsHyper, enetRmsHyper): ε is where the two references differ, so there is no shared default to fall back on.

The packed train step's argument list after %x: the parameter regions in the order the driver packs them — θ, m, v, then the accumulator G (<p>a, only under gradient accumulation) and the model-EMA shadow E (<p>{emaSuf}, only under ema) — followed by the runtime scalars %lr, %bc1, %bc2, %aup, %akeep (accumulation) and %emad, %oemad (EMA). ps is (%name, type) per parameter, in signature order.

G precedes E and never follows it: [θ|m|v|G|E] is the order that leaves both single-axis layouts at the index they already occupy. emaSuf is "e" except on the ResNet family, whose stem BN gamma %sg + e would be %sge — select_and_scatter's block-local name in the max-pool backward — so there it is "ema" (optOne's emaSuf).

The packed train step's leading result types, in packedTrainSig's order: the updated regions θ', m', v'[, G'][, E'], then %loss, %bc1, %bc2, then the handed-back accumulation / EMA scalars. pTy is the parameter types in signature order.

The stochastic-depth mask arguments , %dp<i>: tensor<Bxf32> for the sites idxs, in the order given — the order the driver's dropScales writes them into the blob. Empty when sd is off, which keeps every non-SD render byte-identical. Each net passes its own site list (vitDropSig, cnxDropSig, enetDropSig, r50DropSig).

One frozen-statistic BN site at the per-example index — bnPerChannelEvalF on xin, with the running statistics arriving as graph inputs %{statP}mu / %{statP}var. The BN site of the per-example eval chains (r34FwdChain, r50FwdChain, mnv2FwdChain), which write @resnet34_fwd_eval, @resnet50in_fwd_eval and @mobilenetv2_fwd_eval: frozen-stat affine BN performs no reduction, so these forwards are class-batch-independent and partner the batch-BN train steps whose EMA'd μ/σ² they read. There is deliberately no training arm — the per-example training BN those chains once also emitted (bnPerChannelF) is not the BN any shipped train step uses.

One vector-LN site at the per-example index: lnRowF at the scalar identities %one/%zero (γ = 1, β = 0), then the real [n] affine rowScaleF gN and rowBiasF btN, on the [m, n] matrix xin, at ε epsStr. ViT's token LN (m tokens) and ConvNeXt's head LN (m = 1, after GAP). Returns the LN-output SSA. The ℝ arguments do not print, so 0 and 1 stand for them.

vecLnSite at the batched index: the same three ops as batchOps over N examples of [m, n] each. m is the row count PER EXAMPLE; folding the batch into it is a different graph.

The label-smoothed cotangent after a render's softmax: pretty of smoothedCotTail over the softmax's name smN and %onehot, at width n per example (1 * K under the row softmax, K under softmaxDiv ∘ expe). The ℝ arguments do not print, so 0 stands for them. With the softmax printed first, the text is pretty of smoothedLossCotGraph (row) or smoothedLossCotGraphDiv, the graphs the step ties start from.

The BCE cotangent after a render's sigmoid: pretty of bceCotTail over the sigmoid's name sgN and %onehot; with the sigmoid printed first, the text is pretty of bceLossCotGraph.

Mean label-smoothed CE over the softmax nSm ([B, nClasses]): loss = −(1/B)·Σ_b [ (1−α)·Σ_k onehot·log sm + (α/K)·Σ_k log sm ], the objective whose cotangent smoothedCotB prints. Every batched CE render's %loss.

Mean BCE-with-logits over the logits nLog ([B, nClasses]), the reportSmoothedCeLoss peer for the renders whose cotangent is bceCotB. It is the stable form softplus(z) − t·z: expanding t·softplus(−z) + (1−t)·softplus(z) with softplus(−x) = softplus(x) − x collapses the reference's two softplus calls to one, and softplus(z) = max(z,0) + log(1 + exp(−|z|)) never exponentiates a positive number. The mean is over all B·K entries, not of the per-example sum.

Mean plain CE from the logits nLog ([B, nClasses]): the block re-derives the softmax itself, because the per-example SGD renders (MLP, MNIST CNN) never name theirs.

The banner reportCeLossOfSm opens with unless its caller passes its own.

Mean plain CE from the softmax nSm ([B, nClasses]), read from the same softmax the cotangent uses: the packed-optimizer CIFAR renders. It reduces against %lzero, which those renders' constants block declares.