PoC: the FULL [3,3,9,3] ConvNeXt-T §1a TIE — the whole net tied through the real forward #

The Chapter-7 §1a tie: mnv2's whole-net thread (now MobileNetV2TieB.mnv2_net_tiedB; the per-example original was deleted 2026-09-08) for the ConvNeXt-T schedule. The §1 fold (ConvNeXtFold + M2/M3/ViT) already makes every rendered param op den = certified ∀ cotangent; this file feeds each consumer the real forward activations of the convNextTrainStepFaithfulV render and the loss-driven backward-chain cotangent that net delivers — so the whole 18-block train step is den-composed forward → loss → backward, no free activations, no symbolic cotangent.

The net this is about #

verified_mlir/convnext_train_step.mlir, measured, not assumed:

Superseded scope note. Until 2026-09-05 this file tied the scalar-LN ConvNeXt-T — the retired whole-map bnForward spelling, with no stem LN and a scalar Vec 1 head LN. §2m flipped the renderer to the real per-channel channel_layer_norm and added the stem LN, §2n deleted the flag that had selected the old spelling, and 2026-08-30 restored the head LN. Every theorem in the old file was true and none of them was about the committed bytes. These are: the 22 spatial LN sites are chanLNTensor3 with Vec c γ/β, the head is ViT's vector-LN at N = 1, and the stem LN is here.

What is new against the scalar-LN version #

• channel-LN γ/β (Vec c) at every spatial site, through CnxPoC.chanLn{Gamma,Beta}Sgd_den — the render re-emits the [h·w, c] transposes and runs ViT's veclnGammaSgd / rowDenseBiasSgd on that view, so the op operands here are chanLNRows of the saved LN input and of the chain cotangent, while the certified Jacobian is chanLNTensor3's in the c·h·w activation layout (ConvNeXtChannelLN's permutation argument bridges the two).
• the channel-LN input-VJP in the cotangent chain: chanLNTensor3Back where the scalar version had bn_grad_input. It is the certified VJP — ConvNeXtBackCertifiedTie.chanLNTensor3Back_eq_chanLN_vjp.
• the stem LN, which the scalar version did not have at all: psng/psnbt tie at the stem-LN output cotangent, and the stem conv's own gradients now see the LN input-VJP of it.
• the head at the vector LN: hng/hnbt : Vec 768 through ViTPoC.veclnGammaSgd_den / rowDenseBiasSgd_den_lnbeta at N = 1. Stated at the literal 768 because 1 * m does not reduce at a variable m — the render's own documented trap, in the proof this time.
• the four even-kernel weight grads are no longer a gap. The three downsample 2×2/s2 weights are convStridedWeightSgd (ResNet34PoC.convStridedW_den is kernel-generic), and the stem 4×4/s4 weight is convStride4WeightGrad, whose den is flatConvStride4_weight_grad_has_vjp.

Coverage / honest residual #

All 182 parameters are tied. 181 of them at the full θ − lr·(certified ∂Loss/∂θ) step; the stem weight psW at its gradient, because the render emits convStride4WeightGrad and wraps it in the hand-written sgd text (a declared §5 carve-out — there is no fused convStride4WeightSgd op to be the den of). What remains outside: the block backward is rendered hand-written, so the cotangent SSA ↔ chain-cot correspondence is the per-op trust the whole suite carries; plus per-op pretty lexing; LN 0 < ε smoothness; ℝ → Float32 — the boundary every prior fold carries.

ConvNeXt block — all 9 params tied (depthwise → channel-LN → expand → GELU → project → layer-scale → +skip) #

Forward: out = addV( layerScaleCh lg (conv₁ₓ₁ₚᵣ( gelu( conv₁ₓ₁ₑₓ( chanLN( dw₇ₓ₇(xin) ))))), xin ). Backward from the block-output cotangent dyOut (the residual addV is the outermost op and there is no post-add activation, so it passes dyOut straight to the layer-scale output): layer-scale-back (cnxCotP) → project-conv-back → GELU mask (cnxCotE) → expand-conv-back (cnxCotN) → the channel-LN input-VJP (chanLNTensor3Back) → depthwise-back. Only that last-but-one step differs from the scalar-LN thread; cnxCotP/cnxCotE/cnxCotN are LN-form-agnostic and are reused verbatim from ConvNeXtChainClose.

Downsample — channel-LN → 2×2/s2 conv (all 4 params tied) #

Forward: o = convˢ²(chanLN(xin)) (LN over the block-input grid 2h×2w with a Vec ci affine, then a 2×2/s2 conv ci → co). No skip. Backward from dyOut: strided-conv-back (cotN') → channel-LN-back. The strided weight is no longer a gap: convStridedWeightSgd is emitted at 2×2 since sWGradGeom split the odd/even padding cases, and ResNet34PoC.convStridedW_den is kernel-generic.

Stem — 4×4/s4 patchify conv → channel-LN (all 4 params) #

psng/psnbt tie at dyStem, the cotangent block 1 delivers at the stem-LN output; the conv's own two parameters then see cotPatch, the LN input-VJP of it. The bias grad is a pure cotangent reduce, so the render emits it as a stride-1 convBiasSgd at the OUTPUT resolution and the carried W/x are generic — the same modelling the mnv2/r34 stems use. The weight is the convStride4WeightGrad op, and it ties at the gradient: its SGD wrap is hand-written text.

Head — GAP → vector-LN at one row → dense #

After GAP the tensor is a single [768] row, so "normalise each spatial row over its channels" and "normalise the feature vector" are the same function at m = 1: the head is ViT's per-token LN with one token, and headLnFwdSite is lnFwdSite with the two transposes deleted. Stated at the LITERAL 768 — 1 * m does not reduce at a variable m (Nat.mul recurses on its second argument), which is the annotation trap the render carries in its own comment.

Forward aliases (@[irreducible]) — thread block inputs through the real forward #

@[irreducible] so the 18-deep nested composition stays opaque during the capstone's dimension inference (the r34/mnv2 heartbeat lesson).

Backward cot-in constructors (@[irreducible]) — thread block dyOuts (the residual fan-in) #

Input-only *TiedAt wrappers (@[irreducible]) — compute internals from a block's input #

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

The convNextTrainStepFaithfulV forward threaded: block inputs are the forward prefixes (cnxStemFwdO / cnxBlockFwdChO / cnxDownFwdChO), and the backward cotangents are composed from the loss g = softmax(logits) − onehot down through dense (dense_has_vjp) + the head LN + GAP (globalAvgPoolFlat_has_vjp) + 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. Each stem / block / down / head tie then holds at its real input + threaded cotangent. The full §1a tie: the whole [3,3,9,3] 182-parameter ConvNeXt-T train step is den-composed forward → loss → backward, no free activations, no symbolic cotangent.