ConvNeXt-T's whole-net backward tie — the stage fold and the even-kernel repair #

The per-example whole-net backward tie for ConvNeXt-T: convnextInputGrad, with every slot pinned to the certified per-op backward at its own saved activation, is (convNextForwardTChHasVJP …).backward x. The batched form is ConvNeXtWholeBackCertifiedTieB.lean.

Even kernels. conv2d pads by pH = (kH-1)/2, so the reversed-kernel forward conv (convFlatBack) is the adjoint only when kH - 1 - pH = pH, i.e. only for odd kH. ConvNeXt's 4×4/s4 patchify stem and its three 2×2/s2 downsamples are even-kernel sites; at kH = 4 the symmetric-pad backward is the adjoint of a conv shifted one pixel. StableHLO.Basic's .convStridedBack / .convStridedBackBatched pad asymmetrically, [[kH-1-pH, pH]], and their den is the certified VJP; BackwardMaps.lean's flatConvStride2Back / flatConvStride4Back are convFlatBack ∘ scatter at the symmetric pad. The repair is padOdd (EvenKernelConvBack.lean): an even-kernel conv is an odd-kernel conv on the kernel zero-extended at (+1,+1), which is the emitter's asymmetric pad written in the vocabulary BackwardMaps.lean already has, so the existing odd-kernel leaf tie applies.

What is here.

1. cnxDownChBack_eq_vjp — the stage-boundary downsample tie, lnB ∘ flatConvStride2Back (padOdd W) against (cnxDownChWHasVJP …).backward. padOdd is required: p.W is 2×2.
2. cnxStageChKBack_eq_vjp — the depth-k stage fold. HasVJP for convNextStageChK is built head-first (block 0 runs first), so its backward composes the block backwards in the opposite order, each at its own saved activation, and the tail's saved input is block 0's forward output. The induction step is one rewrite of the block tie (cnxBlockChBack_eq_vjp) and one of the inductive hypothesis.
3. cnxSavedA0 … cnxSavedA10 — convNextForwardTCh's eleven stage inputs, named as functions, so that the same constants are both the activations the backward's slots are saved at and the f argument of each vjpComp.
4. convnextInputGrad_eq_convNextForwardTCh_vjp — the apex. convNextForwardTChHasVJP is a global HasVJP, because GELU, LayerNorm, convolution and the layer scale are all smooth. Its only hypotheses are the 23 LayerNorm positivities, so, like ViT's (vitInputGradK_eq_vitForwardKV_vjp) and EfficientNet-B0's (efficientnetInputGradBFull_eq_efficientnetForwardB_full_vjp), and unlike the ReLU nets' (ResNet-34/50, MobileNetV2, MobileNetV4), it carries no smoothness side-condition. convNextForwardTCh_eq_chain (proved by rw) says the chain the apex instantiates is the committed forward.

Every stage whose declared type carries a computed dimension (cnxDownChW's Vec (cin * (2 * h) * (2 * w)), the head LayerNorm's Vec (1 * 768)) gets a wrapper here, its type ascribed in the chain's spelling, with Differentiable/HasVJP peers ascribed the same way (see the proof-shape notes after the module docstring).

The wrappers, their Differentiable/HasVJP peers, the stem's cnxSavedA0_differentiable/cnxV0 and the four normalised leaf ties below are public: ConvNeXtWholeBackCertifiedTieB.lean lifts the same twelve stages over a batch and needs them at exactly these spellings.

convNextForwardTCh's eleven stage inputs, named as functions, so that the same constants are both the saved activations the backward's slots are indexed by and the f argument of each vjpComp; every link below is then a one-step iota with syntactically identical sides.