ConvNeXt-T's T3 §1a TIE at the BATCHED index, the UN-FUSED gradient and the SMOOTHED loss #

ConvNeXtStepTie.lean ties all 182 parameters of the SGD-inline convnext_train_step.mlir: each fused θ − lr·g op dens to the certified step at the cotangent the emitted backward chain delivers, per example, at a hard label. This file is that statement re-pointed along the THREE axes 4b and 4c left open (planning/archive/proofs_tier_to_paper_nets.md §4b, §4c-quater) — and unlike EfficientNet-B0's (EfficientNetStepTieG.lean, two axes), ConvNeXt's per-example capstone was at a single image with the batch outside the AST, so the index is the third.

⭐ Axis 1 — the OPTIMIZER FORM. Every conjunct is at the RAW gradient node (*GradB), which is what convnext_adam_train_step.mlir and every convnextin_* artifact emit; the fused op appears only in the SGD-inline file. One statement covers AdamW, the wx/clip variants, EMA and the data-parallel twins, because they all consume this node. ConvNeXtFoldGB.lean (§4c-quater) is the fold each conjunct delegates to.

⭐ Axis 2 — the LOSS. The capstone's top-of-chain cotangent is smoothedLossCotGraphDiv's, at a GENERAL target: the six-op chain expe → softmaxDiv → subB → scaleB → addVB → shiftB → divConstB this render emits, with the target arriving as the graph input %onehot — a soft vector under mixup or cutmix. The fused file pins it to softmax − oneHot, the gradient of plain cross-entropy at a hard label, which no ImageNet artifact computes. ⚠ ConvNeXt's chain runs at the plain width N·K (no 1· row index), so there is no rowB/unrowB cast anywhere here.

⭐ Axis 3 — the INDEX. N is a binder. Every forward activation is batchMap N of the per-example prefix the fused file threads (cnxStemFwdO, cnxBlockFwdChO, cnxDownFwdChO), and every cotangent is batchMapAux N of the per-example chain (cnxBlockCotInChAt, cnxDownCotInChAt, ConvNeXtChainClose's cnxCotP/E/N, chanLNTensor3Back). That lift is honest for this net and for no BatchNorm net: LayerNorm, GELU, the convolutions, layer scale and the residual add are all batch-separable, so the batched op IS the per-example op under batchMap — which is what the *B constructors' den arms say. nC is a binder too: the Imagenette artifact is nC = 10, the ImageNet ones nC = 1000.

What is NOT new, and why the file is a transformation rather than a proof #

Every activation, every Jacobian witness and every chain cotangent is ConvNeXtStepTie.lean's, lifted; every conjunct's proof is one CnxPoCGB.*_den lemma. The wN, bN, gN, lrStr and lr binders disappear with the fused wrapper, exactly as they did for B0. ⚠ The head takes g as a PARAMETER where the fused cnxHeadChTied computed it from a label — that is the whole of axis 2 at the block level; the per-block ties were already loss-agnostic.

⛔ Conventions carried unchanged from the fused file: channel LayerNorm (chanLNTensor3, a Vec c affine, h·w statistics per example) at all 22 spatial sites, the head at ViT's vector LN on one row, per-channel layer scale, GELU (no kink — no smoothness hypothesis anywhere), SYMMETRIC padding at the 4×4/s4 stem and the three 2×2/s2 downsamples. Stated at the literal widths of ConvNeXt-T; S and B are other nets. ⛔ ONE REPLICA: in convnextin_adamdp* every gradient node feeds allReduceMeanF, the collective as an AST node since 4d piece 2 (2026-09-07); DataParallelNode.lean composes the per-replica statement with the replica mean. ⛔ The %dgi…%dgapf GAP backward is hand-written text on both chains (a declared carve-out); its value here is globalAvgPoolFlat_has_vjp.backward, as in the fused file.

Per-example internal cotangents as functions of a block's INPUT #

ConvNeXtChainClose's cnxCotE/N and chanLNTensor3Back take the saved activations as arguments; batchMapAux lifts a function of (one saved value, one input), so these recompute the activations from the block input, exactly as cnxBlockCotInChAt does.

ConvNeXt block — all 9 gradient nodes, batched #

Downsample — channel-LN → 2×2/s2 conv, all 4 gradient nodes, batched #

Stem — 4×4/s4 patchify conv → channel-LN, all 4 gradient nodes, batched #

The bias grad is a pure cotangent reduce, so the render emits it as a stride-1 convBiasGradB at the OUTPUT resolution and the carried W/x are generic (xstem is a free parameter here, as Tensor3 3 h w is in the fused file). The weight is convStride4WeightGradB, at its gradient on both chains.

Head — GAP → vector-LN at one row → dense, all 4 gradient nodes, batched #

Stated at the LITERAL 768 for the fused file's reason: 1 * m does not reduce at a variable m. g is a PARAMETER — the loss cotangent arrives from smoothedLossCotGraphDiv in the capstone.

@[irreducible] wrappers — keep the 22-deep capstone thread opaque (the r34/mnv2 heartbeat lesson) #

The whole-net capstone — all 182 params through the REAL batched forward + composed cotangent #

The fused file's thread, lifted: block inputs are batchMap N of the forward prefixes, and the backward cotangents are batchMapAux N of the per-example chain, composed from the smoothed loss g down through the head, every block's backward with the residual fan-in + dyOut at each of the eighteen identity-skip merges, the channel-LN-back at each of the three downsamples, and the stem LN's own back before the patchify conv's gradients.