The full [3,3,9,3] ConvNeXt-T step tie — the whole net tied through the real forward #

The whole-net thread for the ConvNeXt-T schedule (the batched MobileNetV2 peer is MobileNetV2TieB.mnv2_net_tiedB). The folds (ConvNeXtFold and the MobileNetV2 / ResNet-34 / ViT folds it imports) make every rendered param op den = certified ∀ cotangent; this file feeds each consumer the forward activations of the convNextTrainStepText render and the loss-driven backward-chain cotangent that net delivers, so the 18-block train step is den-composed forward → loss → backward with no free activations and no symbolic cotangent. The statement is per example, at one image and a hard label; the artifact runs a batch of 32, and that batch and its mean lie outside this statement (the batched form is ConvNeXtStepTieGB.lean).

The net this is about #

verified_mlir/convnext_train_step.mlir, measured, not assumed:

The channel-LN specifics #

• channel-LN γ/β (Vec c) at every spatial site, through CnxFold.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 (ChannelLN's permutation argument bridges the two).
• the channel-LN input-VJP in the cotangent chain: chanLNTensor3Back. It is the certified VJP — chanLNTensor3Back_eq_chanLN_vjp.
• the stem LN: psng/psnbt tie at the stem-LN output cotangent, and the stem conv's own gradients see the LN input-VJP of it.
• the head at the vector LN: hng/hnbt : Vec 768 through SgdNode.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. The three downsample 2×2/s2 weights are convStridedWeightSgd (SgdNode.convStridedW_den is kernel-generic), and the stem 4×4/s4 weight is convStride4WeightGrad, whose den is flatConvStride4WeightGradHasVJP.

Coverage #

All 182 parameters are tied. 181 of them at the fused step θ − lr·(certified per-layer Jacobian · the chain cotangent), where each chain cotangent is the certified VJP backward of the stages above it (CnxTieGB.cnxBlockCotInChAt_eq_vjp, cnxDownCotInChAt_eq_vjp, cnxHeadDyXheadChN_eq_vjp); the stem weight psW at its gradient, because the render emits convStride4WeightGrad and wraps it in hand-written sgd text (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. 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 SgdNode.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; the node carries an input it never reads (stated at zero), and the clause is at the real stride-4 stem on the image x through GradNodeB.pdiv_flatConvStride4_bias_eq_conv2d (any conv's bias Jacobian is the channel indicator). 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 cnxHeadLnFwdSite is cnxLnFwdSite 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 — thread block inputs through the real forward #

Backward cot-in constructors — thread block dyOuts (the residual fan-in) #

Input-only *TiedAt wrappers — compute internals from a block's input #

Note: only cnxStemChTiedAt is @[irreducible]: without it the capstone's refine ⟨cnx_stem_ch_tiedAt …, ?_, …⟩ times out in whnf, and moving it to its own goal does not help. Every other definition in this section and the two above is a plain def.

The ties' weight records #

The whole-net ties share ONE ε across the stem, every block, downsample and head LN, so these records carry no ε (unlike CnxBlockParamsCh, whose εn is per block). The dot-notation wrappers below are abbrevs over the constructors above: a statement over a record unfolds to exactly the unpacked one.

The same net as ConvNeXtFullT states it #

The records above are the render's shape: one shared ε, the eighteen blocks by name. ConvNeXtFullT states ConvNeXt-T with an ε per record and Fin-indexed stages. These say the two describe one function: block by block (rfl), and whole-net at toCh ε.

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

The convNextTrainStepText 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 (denseHasVJP) + the head LN + GAP (globalAvgPoolFlatHasVJP) + 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 whole [3,3,9,3] 182-parameter ConvNeXt-T train step is den-composed forward → loss → backward, no free activations, no symbolic cotangent.