One BN site. statP is the running-stat input prefix (%{statP}mu / %{statP}var), used only in .eval mode; in .train mode the stats are reduced out of xin and statP is ignored. Every R34 BN site is spatially square, so one hh suffices.

The ResNet-34 parameters in net.paramShapes (= func-arg) order, names + types. The forward, the eval forward and the train step all take their signature from here, so the arity/type/order contract the driver relies on cannot drift between renders.

⚠ 110 at the shipped convBias := false — stem 3 + 13 identity blocks × 6 + 3 downsample blocks × 9 + dense 2 — and 146 with the conv biases in. Every writer below omits the argument, so every committed artifact is the 110 one; the biases are zeroBiasPrelude's zero constants. (Corrected 2026-09-06: this docstring and four below said 146 unconditionally.)

The 72 running-stat inputs — 36 BN layers × (μ, var), each [oc], in BN-forward order: stem, then per identity block n1 n2, per downsample block n1 n2 np. This is exactly the order VerifiedNet.bnChannels is listed in, which is how the driver packs runningBnStats (bnChannels.foldl (fun acc c => acc ++ #[#[c], #[c]])) — μ and var interleaved per layer, NOT all-μ-then-all-var. Appended after the parameters, so @resnet34_fwd_eval takes 1 + 110 + 72 = 183 inputs as committed (1 + 146 + 72 = 219 at convBias := true).

@resnet34_fwd_eval rendered ENTIRELY from the verified AST — the inference forward, with every BN site consuming frozen per-channel running stats (bnPerChannelEvalF) instead of reducing statistics out of its activation. Same net, same parameters in the same order, plus the 72 stat inputs of r34StatSigList: 183 inputs as committed, returning logits [B, nClasses].

This is the eval partner of a batch-statistic train step, whose EMA'd batch mean/var are exactly these per-channel scalars — i.e. of resnet34_adam_train_step.mlir, which is still a hand-written render in TestResnet34Train.lean (since retired). So the eval forward is now certified while the train step it partners is not; that asymmetry is the remaining §2a work, not a property of this render.

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

⭐⭐ ONE WRITER, shared by .adamwAccum and .lambAccum. These eight lines are the whole accumulate/apply mechanism, and duplicating them per optimizer is exactly the double-writer failure planning/archive/next_session_rsb_a3.md §1.1 wanted the type restructured to avoid — the restructure's real purpose was to stop this block existing twice, and factoring it out buys that without the ~8 match sites and 13-artifact re-render the restructure costs.

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 r34WdName produces rather than passed alongside it.

⚠⚠ Derived and not a second argument, on purpose. The skip-list now controls TWO things — whether the decay term enters r (%wdz) and whether the trust ratio applies at all (recipe_fidelity_diffs.md D2) — 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.

At replicas > 1 the gradient is first averaged across devices by prettyAllReduceMean — pretty of the allReduceMeanF node (4d piece 2, 2026-09-07), whose den is the replica MEAN of the per-replica gradient nodes (den_allReduceMeanF, DataParallelNode.lean). ⭐ Until then this was ViTRender.emitGradAllReduce, emitted text outside every faithfulness theorem and a declared TRUSTED CARVE-OUT; the node's emit is that text verbatim, so the committed *dp* artifacts did not move. The optimizer tail consumes the averaged gradient as an .operand, exactly as it consumed the raw one. What stays trusted is the lowerer's all_reduce, as every op's lowering is — and §2b's %loss bug is the standing reminder that a collective needs its own numeric check. Until 2026-09-21 that was the cifar8 exact decomposition gate (no BN ⇒ the identity holds exactly), because per-replica BN made N×b ≠ 1×(N·b) BY DESIGN; the DP render is now SYNC-BN (bnFwdSite/bnBackSite/ bnGammaSite), the identity holds at R34 itself, and resnet34-syncbn-check gates it.

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.

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.

⚠ Identical to cnxWdDecays by construction rather than by coincidence: the rule is timm's, not the net's, and ConvNeXt's own docstring records that its ViT-style nm != "pos" carve-out does not apply to a net with no positional parameter. ResNet has none either.

⚠⚠ This is a3_paper_fidelity.md §2.1, open since the A3 run. The live A3 artifact has ZERO %wdz occurrences against ConvNeXt's 123 — so the 77.43% run decayed BN γ/β and every bias at wd = 0.02 where its reference (resnet50ImagenetConfigRSBFaithful, which sets wdExcludeNormBias := true) did not. Decay on pre-BN conv weights is renormalised away by BN and acts only as an effective-LR control; decay on γ/β is not, because γ directly scales the layer's output. The effect concentrates at low LR — i.e. in the cosine endgame.

The decay operand for one parameter: the real %wd, or the zero constant when excluded.

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.

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. jax/Jax/Codegen.lean:2439 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 one function up.

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 two-writers shape bce/vSuffix was just removed for (a3_paper_fidelity.md §3.3).

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 (planning/archive/verified_optimizer_parity.md §3), 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 — the last-writer-wins race §2a cost this repo a committed artifact once already. 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 (§3.3's lesson, one feature over).

▶ 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 below caught exactly that on the first render. ⚠ It must reach r34AdamVariant and not merely the renderer — the rule wx, clip and bf16 each state above, which ConvNeXt shipped wrong twice and this net shipped wrong once: 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 why they used to be one slot and what that cost RSB-A2/A1.

⚠⚠ THIS IS A FUNCTION SO THAT THE ONE-STEP GATE CAN DRIVE THE SHIPPED PATH. It was inline in ResNet50RenderB.resnet50TrainStepFaithfulB until 2026-08-14, which meant the only way to exercise the clip numerically was to render a whole 161-parameter train step and run a forward. planning/archive/verified_optimizer_parity.md §5's 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 (§5's own point, one level down: a gate on a copy is not a gate on the thing copied). tests/TestOptStepFixtures.lean calls exactly this. ⭐ Pure refactor: every committed R50 artifact re-renders byte-identically.

⚠⚠ 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 (jax/Jax/Codegen.lean:2439): 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.

The driver's variant slug for a given (B, replicas): the artifact is verified_mlir/resnet34_<variant>_train_step.mlir, the entry point is @resnet34_<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 — which is exactly what it did the first time the DP render kept the single-device name (§2b-quater). Deriving the name here, from the same two numbers the render is built from, is what stops it drifting from the #eval paths below; the #guards at the bottom pin those literal paths against this function.

B = 32 is deliberately unsuffixed, so the two existing artifacts keep their names and bytes.

The ResNet-34 forward chain at the BATCHED index — one traversal, consumed by both @resnet34_fwd and every train step that differentiates it.

@resnet34_fwd rendered from the BATCHED chain — the same traversal every batch-BN train step in this file differentiates, so the net that scores and the net that trains are one graph by construction. Replaces the retired ResNet34Render.lean as the writer of verified_mlir/resnet34_fwd.mlir (2026-09-06, planning/archive/renderer_convergence.md leg 1). Takes %x plus the parameters in r34SigList order — 111 inputs at the shipped convBias := false — and returns logits [B, nClasses].

ResNet-34 [3,4,6,3] AdamW train step, batch-BN, rendered from the verified AST at N := B. 407 inputs at the shipped convBias := false (%x, 110 θ, 110 m, 110 v, %lr/%bc1/%bc2, 72 running-stat slots, %onehot) and 408 outputs (110 θ', 110 m', 110 v', %loss/%bc1/%bc2, 72 batch stats). ⛔ This docstring said "515 inputs, 146 θ" until 2026-09-06: 146 is the convBias := true census and the writers all take the default — the fourth file caught on that in one session. The interface is the one TestResnet34Train.lean's hand-written render (since retired) already presented, so the driver is unchanged. Parameter ORDER comes from r34SigList, the same single source the per-example render and both forwards use, so the arity/order contract cannot drift between them.