ConvNeXt-T at the BATCHED index N := B — the forward (handoff §0.2 ▶2) #
The ConvNeXt peer of ResNet34RenderB / MobileNetV2RenderB, and the reason it exists is
planning/archive/stochastic_depth.md: the drop mask is per-EXAMPLE, and in the per-example-indexed
render (ConvNeXtRender.lean) a node denotes ONE example — pretty B lifts it across the batch, so
the node cannot see j. dropPathB needs its operand at index B·n, which is what this file's
chain produces.
⚠⚠ The trap this closes is that the wrong thing TYPECHECKS. pretty B already emits
tensor<B×n>, so a broadcast_in_dim %mask, dims = [0] + multiply against a per-example node
compiles, trains and descends — with no faithful den behind it. Every node below is instead a
batchOp/*B form whose den is batchMap N (…) or batchMapAux N (…), i.e. honest about which
index is the batch.
What this file writes — every ConvNeXt artifact but one (4c leg 3, 2026-09-07). The forward,
the backward, the AdamW/EMA tail and, since leg 3, the seventeen drop-free writers that used to sit
in ConvNeXtRender.lean, beside the stochastic-depth, ImageNet, S/B and bf16 ones that were always
here. Only the SGD-inline convnext_train_step.mlir is still written there: this traversal has no
fused-SGD arm, and ConvNeXtStepTie.lean's 182-parameter tie is stated at those bytes. The Proofs
tier for this chain is Nets/ConvNeXt/ConvNeXtFoldGB.lean, which landed before the writers
moved (leg 1's ordering rule).
The gate (lake build convnext-fwd-b-tie): the per-example chain and this one must emit
byte-identical forwards, and train steps that differ on the conv-VJP transpose/reverse pair
and nothing else (78 lines — commuting ops on disjoint axes). That is a much stronger claim than the
numeric ties elsewhere in this thread, and it is available because every batched form was built to
emit its per-example peer's text byte-for-byte (tests/TestBatchedEmitTie.lean, 31 forms). So the
whole-net statement is the per-form statement composed — and if it ever fails, the tie file
localises which form did it in one run. ⚠ Since leg 3 the committed bytes are THIS chain's, so the
gate renders the per-example chain and compares it against them — the same statement read from the
other side.
The batched shape helpers #
⚠ reassoc/unassoc in the per-example renderer cast SHlo (c*h*h) ↔ SHlo (c*(h*h)). At the
batched index the same cast has to happen UNDER N * ·, which is bnBatchLA's existing move
(congrArg (N * ·) (Nat.mul_assoc …)). It is a reindex, not a function change — the emitted text
is unaffected, since skel never sees the index.
ConvNeXt-T / ImageNet's per-replica batch, spelled ONCE for the whole convnextin_*
family (2026-09-17).
64, not the 32 every other ConvNeXt render uses, and the reason is a PAIRING fact rather
than a throughput one. This net's JAX reference trains at global 256 = 4 × 64 (its own
banner: batch 256 (4x64) · SPE 5004). The verified job ran 4 × 32 = global 128 with
10,009 steps/epoch and a baseLR that is the bs-256 value — half the batch, twice the
updates, and an LR off the linear-scaling rule. That is a RECIPE difference, not a lowering
difference, and it forfeits the only thing this pair is in the book for: ConvNeXt has no
BatchNorm, so a tie here says the LOWERER is clean and an offset here implicates the lowerer
or the feed fleet-wide. Neither reading survives if the batch does not match.
⚠ Spelled once because it has to reach thirteen #evals AND both halves of every train step
(body at N := bB, wrapper via cBS). Thirteen literals is the shape of defect this file's
own thread keeps finding.
⚠ convnextsin_* and convnextbin_* (ConvNeXt-S and -B at ImageNet) stay at the 32
default, deliberately. Neither has ever been trained or paired with a reference, so moving
them would churn nine committed artifacts and nine gate runs for nothing. If either is ever
launched, its job's LEAN_MLIR_BATCH must be checked against its render — the PRECHECK in
scripts/jobs/cnx-default-4gpu.conf greps the artifact for its own baked batch and is the
template for that.
Equations
Instances For
The sites, one per per-example site in ConvNeXtRender.lean #
The full ConvNeXt-T [3,3,9,3] forward at the batched index. Node for node the same chain
convNextFwdChain emits — 4×4/s4 patchify stem (3→96, 224→56) → stem channel-LN → 4 stages at
56/28/14/7 with 2×2/s2 downsamples between → GAP(7×7) → dense(768→nClasses).
⚠ Every node is a batchOp/*B form, so den is a batchMap/batchMapAux at N := bB and
the batch is an index of the AST rather than a number only pretty knows. That is the entire
content of the move; the emitted text is unchanged, which the tie checks.
sd := true adds the 18 stochastic-depth sites, one per block, at ramp index cnxBlockIdx si j
— and the sites are emitted in the FORWARD as well as the train step deliberately
(stochastic_depth.md §3): at eval the driver supplies an all-ones mask, so they are the exact
identity, and the forward ⊂ train-step prefix audit keeps a partner for the SD render instead
of quietly not covering it.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@convnext_fwd_b — the batched-index peer of convNextFwdFaithfulV, same 180-parameter
signature and same %x. ⭐ Since 4c leg 3 (2026-09-07) this WRITES convnext_fwd,
convnextin_fwd, convnextsin_fwd and convnextbin_fwd (the #evals at the bottom of this
file), all four measured byte-identical to the per-example render before the writers moved;
convnext-fwd-b-tie now runs the other way, per-example against these bytes.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The backward #
Every site below is the per-example site with its node swapped for the batched form. ⚠ Two of them are where increments 2 and 3's constructors earn their keep, and both are cases the emit tie alone cannot judge:
lnRowBackBtakes the whole-batch saved LN input and hands examplekbatchSlice k x(batchMapAux). A descriptor here would hand example 0's activation to allN— same types, same bytes, different function (den_lnRowBackB_per_example).veclnGammaGradB/rowDenseBiasGradBcontract the batch and the spatial rows. The per-example peers contract only the rows, and the two spellings agree atN = 1(den_rowDenseBiasGradB_at_one) — so a render that dropped the batch sum would pass a one-example check.
The whole-net batched traversal — forward + cotangent + every parameter gradient, the
batched peer of convNextBackAll true (some …). Returns (code, gradMap, softmaxSSA) with the
same shape, so the AdamW tail in ConvNeXtRender.lean can consume either.
⚠ AdamW only, deliberately. The per-example traversal serves both renders off one adam
flag; this one does not, because the SGD path bakes lr as a literal where AdamW takes it as a
runtime %lr operand, and an SGD render at the batched index is not something any config asks
for yet. Adding the flag later is cheap; adding an artifact nobody loads is §2a-quater's
silent-hyperparameter hazard.
⚠ The %dgi/%dgb/%dgn/%dgd/%dgapf GAP-backward block is hand-written text on both
sides, carried over verbatim. It is one of §5's declared non-AST carve-outs, so the batched
move neither improves nor degrades it — but note it is parameterised by bB and therefore
already batch-correct, which is why it needs no peer.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The ConvNeXt-T AdamW train step at the batched index. ⚠ It is the SAME renderer the
per-example path uses — convNextAdamTrainStepFaithful with traversal pointed at
convNextBackAllB — not a copy.
That is possible because the AdamW tail is entirely parameter-space: adamMNextF,
adamVNextF, adamWParamF, gradSumSqAccF and clipScaleF are indexed by the parameter's
own size and never see the batch. So "the AdamW tail at the batched index" turned out to be no
work at all — the batch had already been factored out of it, by the ops' own shapes. The only
thing that moves is which traversal produced the gradients.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The drop-free forward's banner — the line ConvNeXtRender.convNextFwdFaithfulV emits, restated
here so the byte tie can demand byte-identity rather than "identical apart from a comment".
⚠ Worth the parameter: a tie that compares modulo one line is a tie with a hole in it, and the
hole is exactly where a renderer's own description of what it did would live. Measured first,
then removed — the two chains differed in this line and nothing else. ⭐ Since 4c leg 3
(2026-09-07) this is the banner the committed convnext_fwd / convnextin_fwd /
convnextsin_fwd / convnextbin_fwd carry, which is why it takes the size: the model name
is derived from the stage table, exactly as the per-example line derives it.
Equations
- Proofs.StableHLO.cnxFwdBanner V = toString " // ── " ++ toString (Proofs.StableHLO.cnxModelName V) ++ toString " forward: every line is pretty(verified AST node) ──\n"
Instances For
The SD forward's banner. Its own, and not cnxFwdBanner, because these bytes ARE a
different render and a banner claiming otherwise is the VerifiedNets docstring defect (§0.9
finding 3) in the artifact itself.
Equations
- One or more equations did not get rendered due to their size.