The batched stem tie. batchMap B of the reversed-kernel conv at the zero-extended 4×4 kernel IS the lift's backward: flatConvStride4Back_padOdd_eq_vjp_backward at one example's row. padOdd is required here as in the per-example tie: w.sW is 4×4.

The batched channel-LayerNorm tie, at any c h w — chanLNTensor3Back_eq_chanLN_vjp at each row. Note: stated at variable dims because an rfl proof at the literal 96 56 56 recursed past maxRecDepth 100000 on the numerals; at variables it is ViT's vitLNBackB_eq_vjp. The stem instance below is a term.

The batched stage tie — cnxStageChKBack_eq_vjp at one example's row, for every depth.

The batched downsample tie, at any resolution — cnxDownChBack_eq_vjp at one example's row. Generic for the same reason as cnxChanLNBackB_eq_vjp; the three instances below are terms at the chain's dimension spellings (cnxDn1 … cnxDn3), which is the per-example tie's cnxDn1Back_eq_vjp … cnxDn3Back_eq_vjp one batch index over. padOdd is required: p.W is 2×2.

The batched GAP tie is rfl, as the per-example gapBack_eq_vjp_backward is.

The batched head-LayerNorm tie — cnxLNhBack_eq_vjp at one example's row.

The batched classifier tie — dense_transpose_eq_vjp_backward at one example's row (the head is linear, so the saved v is free).

The batched tie. convnextInputGradB with every slot the per-example slot at the batched saved activation is the backward of convNextForwardTChBHasVJPAt, at every B, nC and batch x, under the 23 LayerNorm positivities.

The shape check. batchMap B of the per-example twelve-factor chain — the function convNextForwardTChHasVJP is stated on — IS the twelve batched stages the apex is stated on: batchMap_comp eleven times, and the normalised spellings (cnxLNh, cnxDn1 … cnxDn3, cnxSavedA0) unfold to the chain's.

The batched apex at the global witness. convnextInputGradB is (batchMapHasVJP _ (convNextForwardTChHasVJP …) …).backward x — the certified gradient of the drop-free per-example ConvNeXt-T forward lifted over B examples, for every B, every nC and every batch x. The hypotheses are the 23 LayerNorm positivities. Carried from the chain-shaped apex by HasVJPAt.backward_unique_of_eq along convNextForwardTChB_eq_chain.

The batched apex, read as the Jacobian of the committed forward. convnextInputGradB is the pdiv-contracted Jacobian transpose of batchMap B (convNextForwardTCh w) — the nested-application forward the graph faithfulness convNextFwdGraphTCh_faithful is about — at EVERY batch and EVERY cotangent, through convNextForwardTCh_eq_chain.

ConvNeXt-T's batched whole-net backward tie at the ImageNet head. convnextInputGradB_eq_batchMap_convNextForwardTCh_vjp at nC = 1000, the class count of the convnextin_* (ConvNeXt-T) artifacts, at a variable batch B (64 per device in those artifacts). The dims are ConvNeXt-T's (3×224², [3,3,9,3] at 96→192→384→768). The forward is the drop-free convNextForwardTCh in exact arithmetic: the drop-path (*drop*) artifacts and ConvNeXt-S/B (convnextsin_*, convnextbin_*) compute other functions and are not covered. The batched peers of the other nets are r34InputGradB_eq_r34B_full_vjp, mnv2InputGradB_eq_mobilenetv2B_full_vjp and vitTinyInputGradB_eq_vitTiny_vjp.