ConvNeXt whole-block backward-graph faithfulness (per-example / batch-1) #
The ConvNeXt analogue of mbResidBlockBackBatchedGraph_faithful (EfficientNet) and
r34*BackBatchedGraph_faithful (ResNet-34): a backward StableHLO graph that
denotes the proven whole-block VJP.
ConvNeXt's whole verified stack is per-example / batch-1 — LayerNorm here is
the per-example separable layerNormForward (= bnForward on the feature axis),
so NONE of EfficientNet's batchMap/bnBatchLA batched machinery is needed
(ConvNeXtChainClose.lean:8). So this file targets the per-example VJPs of the shipped
CHANNEL-LN net directly, modeled on the per-example section of EfficientNetBackB0.lean
(residualBackGraph, convBnSwishBackGraph).
chanLNBackGraph and its faithfulness come first, then the block, residual-block and downsample
capstones over it (§2o Part A, 2026-07-31). chanLNBackGraph_faithful is the backward peer of
§2m's chanLNGraph_faithful, and chanLNBackGraph_eq_vjp chains it through §B
(ConvNeXtBackCertifiedTie.chanLNTensor3Back_eq_chanLN_vjp), so every capstone lands on the
CERTIFIED VJP rather than on a hand-composed reverse chain. The block is residual (block body)
with an identity skip, so the brick is residualBackGraph (bodyBack …) dy, closed via
residualBackGraph_faithful.
The block body is layerScale ∘ project(1×1) ∘ gelu ∘ expand(1×1) ∘ LN ∘ depthwise(7×7); everything is smooth (GELU is smooth, conv/layerScale linear, LN
smooth given ε>0), so the body VJP is the unconditional vjp_comp chain
convNextBlockBody_has_vjp and the only side condition is the LayerNorm positivity
0 < εn. The LN backward is the one non-rfl op, closed by chanLNBackGraph_eq_vjp.
The backward peer of rowLN_affine_eq (ConvNeXtChannelLN.lean). Forward, the emitted
subtree normalises at the scalar identities %one/%zero and only then applies the real [c]
affine, so three denotations collapse onto rowLNVecFlat. Backward it is the same fold one
step earlier: the emitted rowScaleF γ applied to the COTANGENT is exactly the per-row
diagBack γ that rowLNVecFlatBack folds in, and the LN input gradient then runs at γ = 1.
β does not appear on either side — the translation's adjoint is the identity, which is the
same β-freeness §B proved for the certified backward.
One channel-LN backward site, mirroring ConvNeXtRender.lnBackSite at chLN := true
op-for-op: transpose the cotangent to [h·w, c], scale it by the real [c] γ, run the rowwise
LN input gradient at γ = 1 against the saved input's transposed view, transpose back. The two
▸ transports are the same Nat-associativity casts chanLNGraph uses.
The saved LN input enters as a VALUE (chanLNRows — its [h·w, c] view) alongside its SSA
name, exactly as the scalar bnBack carries its own: lnRowBack recomputes x̂/istd from the
input rather than saving them. The backward peer of ConvNeXtFullT.chanLNGraph.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Channel-LN backward-graph faithfulness — the den-level peer of chanLNGraph_faithful,
and the keystone the §2n drop left uncovered. Same six-step shape as the forward: the two ▸
transports through den_{un,re}assocS, the three permutation/scale ops and the row backward
through their rfl gates, and the graph's rowScaleF-then-lnRowBack pair collapsed onto
rowLNVecFlatBack by rowLNBack_affine_eq.
The channel-LN backward graph denotes the CERTIFIED VJP. chanLNBackGraph_faithful lands
on chanLNTensor3Back, the hand-composed reverse chain; §B's
chanLNTensor3Back_eq_chanLN_vjp carries it the last step onto
(chanLNTensor3_has_vjp …).backward. This is the statement every capstone below is built on,
and the reason landing §B first was worth doing — without it these would tie the graph to
another hand-written chain rather than to the certified gradient. β-free on both sides.
The channel-LN block-body backward graph — the block body's reverse chain with
chanLNBackGraph for the LayerNorm and the LN affine at Vec c, which is exactly what §2m's
flip did to the forward.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Channel-LN block-body backward-graph faithfulness. The reverse-order graph denotes
cnxBodyWith_has_vjp's backward at the shipped LayerNorm, under 0 < εn. Same proof as the
scalar peer with chanLNBackGraph_eq_vjp where bnBack_faithful_fn was — the LN is still the
one non-rfl op, it is just a whole subtree now instead of a token.
The whole channel-LN residual block backward graph (block body + identity skip).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The whole channel-LN ConvNeXt residual block: backward graph ↔ proven VJP — the capstone
the shipped net was missing, at the block the shipped stages are built from. Assembles the
body backward graph + the identity skip into cnxBlockChW_has_vjp's backward via
residualBackGraph_faithful, no hypotheses beyond 0 < p.εn.
The channel-LN stage-boundary downsample backward graph. Forward is flatConvStride2(2×2) ∘ chanLNTensor3, so the VJP in reverse order is
chanLNBackGraph ∘ convStridedBack, each at its forward input: LN is the outer backward at
x, and the strided conv's input is chanLNTensor3 … x.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The channel-LN downsample: backward graph ↔ proven VJP, under 0 < p.ε. The theorem §2n's
commit message named as the gap — restored at the LayerNorm the net actually uses.
convStridedBack is rfl-faithful; the LN goes through chanLNBackGraph_eq_vjp.