ConvNeXt Item D — pinning the block cotangent chain

ConvNeXtClose.lean (Item C) certifies each ConvNeXt param output for any cotangent dy at that layer's output. This file pins dy to the cotangent the actual backward chain delivers — the ConvNeXt analogue of MobileNetV2ChainClose (planning/archive/convnext_close.md Item D). Pure-Lean, batch-1 — LayerNorm is per-example separable, so none of EfficientNet's batched-VJP machinery (batchMap_has_vjp) is needed.

The chain through a ConvNeXt block composes the rendered backward denotations — layer-scale back (layerScale γls applied to the cotangent: the input-VJP γ ⊙ dy is the forward map itself, the layerScaleF-on-the-cotangent trick the Item B render uses), the 1×1 conv input-VJP (conv2d_has_vjp3 via the flatten bridge, = convBack's denotation), the GELU mask (dy ⊙ geluScalarDeriv, = gelu_has_vjp's backward; geluScalarDeriv_eq certifies the closed form geluBack emits), the scalar-LN input-VJP (bn_grad_input, = bnBack's denotation), and the depthwise input-VJP (depthwiseFlat_has_vjp, = depthwiseBack's denotation) — back through layerScale → project → gelu → expand → LN → depthwise:

block: o = addV( layerScale γls (conv₁ₓ₁ₚᵣ( gelu( conv₁ₓ₁ₑₓ( LN( dw₇ₓ₇(x) ))))), x )

The residual addV is the outermost op and passes the block cotangent dyOut straight through to the layer-scale output (ConvNeXt has no post-add activation — the r34 relu(add(…)) mask never appears), and the identity skip adds dyOut back at the block input. Unlike MNV2/r34 there is no stride split: ConvNeXt blocks keep resolution (stride-1 7×7 depthwise), so one set of cotangent definitions covers every block. Each param output then denotes θ − lr·(certified ∂/∂θ · the actual-chain cotangent) — including the two ConvNeXt-signature families (layer-scale γ, scalar-LN γ/β), which MNV2/r34 had no analogue of. Pins the cotangent; the = ∂loss/∂θ fold stays separate, as for the CNN. 3-axiom clean.

noncomputable def Proofs.cnxCotP {n : ℕ} (γls dyOut : Vec n) : Vec n

Cotangent at the project conv output (= the layer-scale input): layerScale γls dyOut — the forward map applied to the block cotangent. The residual addV passes dyOut through to the layer-scale output unchanged (no post-add activation), and layerScale's input-VJP γ ⊙ dy is layerScale γ itself (diagonal/symmetric — layerScale_has_vjp), which is why the Item B render emits a second layerScaleF on the cotangent rather than a backward token.

Equations

• Proofs.cnxCotP γls dyOut = Proofs.layerScale γls dyOut

noncomputable def Proofs.cnxCotE {c cExp h w : ℕ} (γls : Vec (c * h * w)) (Wpr : Kernel4 c cExp 1 1) (bpr : Vec c) (g e : Vec (cExp * h * w)) (dyOut : Vec (c * h * w)) : Vec (cExp * h * w)

Cotangent at the expand conv output (cExp ch, pre-GELU): continue through the project 1×1 conv-back and the GELU mask (geluScalarDeriv at the saved pre-GELU activation e).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Proofs.cnxCotN {c cExp h w : ℕ} (γls : Vec (c * h * w)) (Wex : Kernel4 cExp c 1 1) (bex : Vec cExp) (Wpr : Kernel4 c cExp 1 1) (bpr : Vec c) (nl : Vec (c * h * w)) (g e : Vec (cExp * h * w)) (dyOut : Vec (c * h * w)) : Vec (c * h * w)

Cotangent at the LN output (c ch): continue through the expand 1×1 conv-back. This is the cotangent the scalar-LN γ/β grads contract with — the substantive LN pin.

Equations

• Proofs.cnxCotN γls Wex bex Wpr bpr nl g e dyOut = (Proofs.hasVJP3_to_hasVJP (Proofs.conv2d_has_vjp3 Wex bex)).backward nl (Proofs.cnxCotE γls Wpr bpr g e dyOut)

noncomputable def Proofs.cnxCotD {c cExp h w : ℕ} (ε γn : ℝ) (γls : Vec (c * h * w)) (Wex : Kernel4 cExp c 1 1) (bex : Vec cExp) (Wpr : Kernel4 c cExp 1 1) (bpr : Vec c) (d nl : Vec (c * h * w)) (g e : Vec (cExp * h * w)) (dyOut : Vec (c * h * w)) : Vec (c * h * w)

Cotangent at the depthwise conv output (c ch): continue through the scalar-LN input-VJP (bn_grad_input — the three-term bnBack denotation, recomputing x̂/istd from the saved LN input d).

Equations

• Proofs.cnxCotD ε γn γls Wex bex Wpr bpr d nl g e dyOut = Proofs.bn_grad_input (c * h * w) ε γn d (Proofs.cnxCotN γls Wex bex Wpr bpr nl g e dyOut)

noncomputable def Proofs.cnxCotXin {c cExp h w kH kW : ℕ} (ε γn : ℝ) (γls : Vec (c * h * w)) (Wdw : DepthwiseKernel c kH kW) (bdw : Vec c) (Wex : Kernel4 cExp c 1 1) (bex : Vec cExp) (Wpr : Kernel4 c cExp 1 1) (bpr : Vec c) (xin d nl : Vec (c * h * w)) (g e : Vec (cExp * h * w)) (dyOut : Vec (c * h * w)) : Vec (c * h * w)

Cotangent at the block input: the depthwise input-VJP of cnxCotD, plus the identity skip's dyOut. This is what the block hands upstream — the next block's dyOut, and at block 1 the stem's dyStem.

Equations

• Proofs.cnxCotXin ε γn γls Wdw bdw Wex bex Wpr bpr xin d nl g e dyOut i = (Proofs.depthwiseFlat_has_vjp Wdw bdw).backward xin (Proofs.cnxCotD ε γn γls Wex bex Wpr bpr d nl g e dyOut) i + dyOut i

noncomputable def Proofs.cnxStemCot {n : ℕ} (ε γst : ℝ) (patch dyStem : Vec n) : Vec n

Cotangent at the stem conv output: bn_grad_input at the saved patchify output (the stem is conv → scalar-LN, nothing else — no activation, no pool), applied to dyStem, the cotangent block 1 delivers at the stem-LN output (= block 1's cnxCotXin).

Equations

• Proofs.cnxStemCot ε γst patch dyStem = Proofs.bn_grad_input n ε γst patch dyStem

theorem Proofs.cnx_render_lsgamma_chain_certified {n : ℕ} (p γls dyOut : Vec n) (lr : ℝ) (i : Fin n) : γls i - lr * layerScale_grad_gamma p dyOut i = γls i - lr * ∑ j : Fin n, pdiv (fun (γ' : Vec n) => layerScale γ' p) γls i j * dyOut j

Layer-scale γ, chain-certified. The chain cotangent at the layer-scale output IS the block cotangent dyOut — the residual addV is the outermost op and ConvNeXt has no post-add activation, so the passthrough is exact. γlsⁿ denotes γls − lr·(certified ∂(layerScale)/∂γ · dyOut) with the saved project output p as the layer input.

theorem Proofs.cnx_render_projW_chain_certified {c cExp h w : ℕ} (bpr : Vec c) (g : Vec (cExp * h * w)) (γls dyOut : Vec (c * h * w)) (v : Vec (c * cExp * 1 * 1)) (lr : ℝ) (idx : Fin (c * cExp * 1 * 1)) : v idx - lr * (conv2d_weight_grad_has_vjp bpr (Tensor3.unflatten g)).backward v (cnxCotP γls dyOut) idx = v idx - lr * ∑ j : Fin (c * h * w), pdiv (fun (v' : Vec (c * cExp * 1 * 1)) => (conv2d (Kernel4.unflatten v') bpr (Tensor3.unflatten g)).flatten) v idx j * cnxCotP γls dyOut j

Project 1×1 conv weight, chain-certified. Wprⁿ denotes Wpr − lr·(certified ∂conv/∂Wpr · layerScale γls dyOut) — the conv weight bridge at the layer-scale-back cotangent, with the saved GELU output g as the conv input.

theorem Proofs.cnx_render_projb_chain_certified {c cExp h w : ℕ} (Wpr : Kernel4 c cExp 1 1) (g : Vec (cExp * h * w)) (bpr : Vec c) (γls dyOut : Vec (c * h * w)) (lr : ℝ) (o : Fin c) : bpr o - lr * (conv2d_bias_grad_has_vjp Wpr (Tensor3.unflatten g)).backward bpr (cnxCotP γls dyOut) o = bpr o - lr * ∑ j : Fin (c * h * w), pdiv (fun (b' : Vec c) => (conv2d Wpr b' (Tensor3.unflatten g)).flatten) bpr o j * cnxCotP γls dyOut j

Project 1×1 conv bias, chain-certified.

theorem Proofs.cnx_render_expW_chain_certified {c cExp h w : ℕ} (bex : Vec cExp) (nl γls : Vec (c * h * w)) (Wpr : Kernel4 c cExp 1 1) (bpr : Vec c) (g e : Vec (cExp * h * w)) (dyOut : Vec (c * h * w)) (v : Vec (cExp * c * 1 * 1)) (lr : ℝ) (idx : Fin (cExp * c * 1 * 1)) : v idx - lr * (conv2d_weight_grad_has_vjp bex (Tensor3.unflatten nl)).backward v (cnxCotE γls Wpr bpr g e dyOut) idx = v idx - lr * ∑ j : Fin (cExp * h * w), pdiv (fun (v' : Vec (cExp * c * 1 * 1)) => (conv2d (Kernel4.unflatten v') bex (Tensor3.unflatten nl)).flatten) v idx j * cnxCotE γls Wpr bpr g e dyOut j

Expand 1×1 conv weight, chain-certified. Wexⁿ denotes Wex − lr·(certified ∂conv/∂Wex · the chain cotangent at the expand output) — through layer-scale back, project conv-back, and the GELU mask — with the saved LN output nl as the conv input.

theorem Proofs.cnx_render_expb_chain_certified {c cExp h w : ℕ} (Wex : Kernel4 cExp c 1 1) (nl : Vec (c * h * w)) (bex : Vec cExp) (γls : Vec (c * h * w)) (Wpr : Kernel4 c cExp 1 1) (bpr : Vec c) (g e : Vec (cExp * h * w)) (dyOut : Vec (c * h * w)) (lr : ℝ) (o : Fin cExp) : bex o - lr * (conv2d_bias_grad_has_vjp Wex (Tensor3.unflatten nl)).backward bex (cnxCotE γls Wpr bpr g e dyOut) o = bex o - lr * ∑ j : Fin (cExp * h * w), pdiv (fun (b' : Vec cExp) => (conv2d Wex b' (Tensor3.unflatten nl)).flatten) bex o j * cnxCotE γls Wpr bpr g e dyOut j

Expand 1×1 conv bias, chain-certified.

theorem Proofs.cnx_render_lngamma_chain_certified {c cExp h w : ℕ} (ε βn : ℝ) (γ : Vec 1) (γls : Vec (c * h * w)) (Wex : Kernel4 cExp c 1 1) (bex : Vec cExp) (Wpr : Kernel4 c cExp 1 1) (bpr : Vec c) (d nl : Vec (c * h * w)) (g e : Vec (cExp * h * w)) (dyOut : Vec (c * h * w)) (lr : ℝ) : γ 0 - lr * bn_grad_gamma (c * h * w) ε d (cnxCotN γls Wex bex Wpr bpr nl g e dyOut) = γ 0 - lr * ∑ j : Fin (c * h * w), pdiv (fun (γ' : Vec 1) => layerNormForward (c * h * w) ε (γ' 0) βn d) γ 0 j * cnxCotN γls Wex bex Wpr bpr nl g e dyOut j

Block scalar-LN γ, chain-certified. The substantive LN pin: the chain cotangent at the LN output is cnxCotN (through layer-scale back → project conv-back → GELU mask → expand conv-back), and γⁿ denotes γ − lr·(certified ∂LN/∂γ · cnxCotN) with the saved depthwise output d as the LN input — the Item C Vec 1 embedding at the actual chain cotangent.

theorem Proofs.cnx_render_lnbeta_chain_certified {c cExp h w : ℕ} (ε γn : ℝ) (β : Vec 1) (γls : Vec (c * h * w)) (Wex : Kernel4 cExp c 1 1) (bex : Vec cExp) (Wpr : Kernel4 c cExp 1 1) (bpr : Vec c) (d nl : Vec (c * h * w)) (g e : Vec (cExp * h * w)) (dyOut : Vec (c * h * w)) (lr : ℝ) : β 0 - lr * bn_grad_beta (c * h * w) (cnxCotN γls Wex bex Wpr bpr nl g e dyOut) = β 0 - lr * ∑ j : Fin (c * h * w), pdiv (fun (β' : Vec 1) => layerNormForward (c * h * w) ε γn (β' 0) d) β 0 j * cnxCotN γls Wex bex Wpr bpr nl g e dyOut j

Block scalar-LN β, chain-certified.

theorem Proofs.cnx_render_dw7W_chain_certified {c cExp h w : ℕ} (bdw : Vec c) (xin : Vec (c * h * w)) (ε γn : ℝ) (γls : Vec (c * h * w)) (Wex : Kernel4 cExp c 1 1) (bex : Vec cExp) (Wpr : Kernel4 c cExp 1 1) (bpr : Vec c) (Wdw : DepthwiseKernel c 7 7) (d nl : Vec (c * h * w)) (g e : Vec (cExp * h * w)) (dyOut : Vec (c * h * w)) (lr : ℝ) (ci : Fin c) (hi wi : Fin 7) : Wdw ci hi wi - lr * (depthwise_weight_grad_has_vjp3 bdw (Tensor3.unflatten xin)).backward Wdw (Tensor3.unflatten (cnxCotD ε γn γls Wex bex Wpr bpr d nl g e dyOut)) ci hi wi = Wdw ci hi wi - lr * ∑ co : Fin c, ∑ ho : Fin h, ∑ wo : Fin w, pdiv3 (fun (W' : DepthwiseKernel c 7 7) => depthwiseConv2d W' bdw (Tensor3.unflatten xin)) Wdw ci hi wi co ho wo * Tensor3.unflatten (cnxCotD ε γn γls Wex bex Wpr bpr d nl g e dyOut) co ho wo

Depthwise 7×7 weight, chain-certified. Wdwⁿ denotes Wdw − lr·(certified ∂(depthwiseConv2d)/∂Wdw · the deepest in-block cotangent) — through the whole chain down to the scalar-LN input-VJP — with the saved block input xin as the conv input.

theorem Proofs.cnx_render_dw7b_chain_certified {c cExp h w : ℕ} (Wdw : DepthwiseKernel c 7 7) (xin : Vec (c * h * w)) (bdw : Vec c) (ε γn : ℝ) (γls : Vec (c * h * w)) (Wex : Kernel4 cExp c 1 1) (bex : Vec cExp) (Wpr : Kernel4 c cExp 1 1) (bpr : Vec c) (d nl : Vec (c * h * w)) (g e : Vec (cExp * h * w)) (dyOut : Vec (c * h * w)) (lr : ℝ) (cc : Fin c) : bdw cc - lr * (depthwise_bias_grad_has_vjp Wdw (Tensor3.unflatten xin)).backward bdw (cnxCotD ε γn γls Wex bex Wpr bpr d nl g e dyOut) cc = bdw cc - lr * ∑ j : Fin (c * h * w), pdiv (fun (b' : Vec c) => (depthwiseConv2d Wdw b' (Tensor3.unflatten xin)).flatten) bdw cc j * cnxCotD ε γn γls Wex bex Wpr bpr d nl g e dyOut j

Depthwise 7×7 bias, chain-certified.

theorem Proofs.cnx_stem_render_convW_chain_certified {ic c h w : ℕ} (bst : Vec c) (x : Vec (ic * h * w)) (ε γst : ℝ) (patch dyStem : Vec (c * h * w)) (v : Vec (c * ic * 1 * 1)) (lr : ℝ) (idx : Fin (c * ic * 1 * 1)) : v idx - lr * (conv2d_weight_grad_has_vjp bst (Tensor3.unflatten x)).backward v (cnxStemCot ε γst patch dyStem) idx = v idx - lr * ∑ j : Fin (c * h * w), pdiv (fun (v' : Vec (c * ic * 1 * 1)) => (conv2d (Kernel4.unflatten v') bst (Tensor3.unflatten x)).flatten) v idx j * cnxStemCot ε γst patch dyStem j

Stem 1×1 patchify conv weight, chain-certified. Wstⁿ denotes Wst − lr·(certified ∂conv/∂Wst · bn_grad_input(patch, dyStem)) — the stem-LN input-VJP at the cotangent block 1 delivers (dyStem = block 1's cnxCotXin; generic here, as for the MNV2/r34 stems).

theorem Proofs.cnx_stem_render_convb_chain_certified {ic c h w : ℕ} (Wst : Kernel4 c ic 1 1) (x : Vec (ic * h * w)) (bst : Vec c) (ε γst : ℝ) (patch dyStem : Vec (c * h * w)) (lr : ℝ) (o : Fin c) : bst o - lr * (conv2d_bias_grad_has_vjp Wst (Tensor3.unflatten x)).backward bst (cnxStemCot ε γst patch dyStem) o = bst o - lr * ∑ j : Fin (c * h * w), pdiv (fun (b' : Vec c) => (conv2d Wst b' (Tensor3.unflatten x)).flatten) bst o j * cnxStemCot ε γst patch dyStem j

Stem 1×1 patchify conv bias, chain-certified.