T3 §1 fold for ConvNeXt-T at the BATCHED index — the op set every ImageNet artifact renders #

ConvNeXtFoldG.lean folds the fourteen gradient nodes of the PER-EXAMPLE traversal (ConvNeXtRender.convNextBackAll at adam := true). This is its batched peer, at ConvNeXtRenderB.convNextBackAllB's constructors — and unlike ViT's (ViTFoldGB.lean), it was owed BEFORE any renderer swap: every convnextin_* train step, every *drop* variant and the ConvNeXt-S/B artifacts have rendered from the batched chain since they existed, so the artifact behind this net's quoted ImageNet accuracy (convnextin_adamdpwxclipdrop) had a fold at the per-example constructors that no committed byte of it is pretty of. 4b's "one lemma per op kind certifies every optimizer tail" was, for ConvNeXt, a statement about the Imagenette pair only.

⭐ The bytes are the same on the forward and differ on 78 backward lines. The batched convBackBatched emits the conv input-VJP's transpose/reverse in the other order from the per-example convBack — commuting ops on disjoint axes, one kernel — and tests/TestConvNeXtFwdBTie.lean allows exactly that pair and nothing else. 4c leg 3 moves the drop-free writers onto this chain; this file lands first, per leg 1's ordering rule, so that no committed artifact is ever pretty of an AST without a fold.

The op table of convnext_adam_train_step.mlir and every convnextin_* train step #

⭐ No new mathematics. Every proof is Finset.sum_congr rfl over the batch and then the per-example bridge at batchSlice n — ResNet34FoldB.denseWGradB_den's shape — because each batched den arm is literally the per-example one under a batch sum. The channel-LN sites add one step: the batched render hands the LN ops batchMap N (chanLNRows c h w) of the saved input and of the cotangent (the [h·w, c] transposed views, lifted per example), and batchSlice_batchMap peels the lift so ConvNeXtChannelLN's permutation argument applies at each slice.

⭐ The bf16 artifacts (convnextin_adamwxclipdropbf16, the S/B twins) emit *GradBBf16 constructors, not these nodes: their den rounds the operands and the result once, outside the batch sum. Those are their own op kinds, folded once for every net in Foundation/Bf16GradNodes.lean (first stated in this file, 2026-09-07).

⭐ One lemma per op kind certifies every optimizer tail at once — AdamW, the wx/clip variants, the EMA shadow, drop-path and the data-parallel twins all consume the same *GradB node, and convnextin_adamdpwxclipdrop, whose accuracy the book quotes, is one of them.

Honest residual #

• ⚠ biasGradB is the IDENTITY on its operand and the classifier bias's batch reduce is in the emitted text, outside the AST — so headBGradB_den is stated PER EXAMPLE at batchSlice n, the per-example biasGrad carve-out carried over unchanged (as in ViTFoldGB).
• Every lemma is ∀ cot. Pinning each to the emitted backward subgraph is the §1a tie; ConvNeXt's capstone (ConvNeXtStepTie.lean, 182 params) is at the per-example SGD-inline convnext_train_step.mlir, which stays on the per-example chain (the batched traversal has no fused-SGD arm). Re-pointing it at these nodes with SmoothedLossCot is 4b's ConvNeXt capstone, which this file is the prerequisite for.
• convnextin_adamdp* is four replicas: the all-reduce is emitted text outside the AST, so these lemmas are about the per-replica gradient node (4d).
• ⛔ SYMMETRIC padding at the three 2×2/s2 downsamples and the 4×4/s4 stem (flatConvStride2, flatConvStride4); ConvNeXt is PyTorch-origin and has no XLA-SAME site.