Conv / dense / GAP leaf ties — each per-op backward map IS the certified VJP #
The hand-composed backward chains (ResNetBackChains, the MobileNetV2 / EfficientNet / ConvNeXt /
ViT whole-back ties) are written in the per-op backward maps of BackwardMaps. This file ties each
conv-family leaf to its certified VJP, so the whole-net ties close on named maps:
| leaf | theorem |
|---|---|
| conv (odd kernel), reversed-kernel conv = input-VJP | convFlatBack_eq_vjp_backward |
stride-2 conv, symmetric padding / XLA-SAME | flatConvStride2Back_eq_vjp_backward / flatConvStride2XlaBack_eq_vjp_backward |
dense, Wᵀ·dy | dense_transpose_eq_vjp_backward |
| global average pool, broadcast ÷ | gapBack_eq_vjp_backward |
The depthwise twins are in DepthwiseBackCertifiedTie, the even-kernel conv in
EvenKernelConvBack, the 3×3/s2 max-pool leaf (maxPool3s2FlatBack_eq_vjp_backward) in
BackwardMaps.
Conv input-VJP leaf tie. The backward map convFlatBack W (= reversed-kernel forward
conv) IS the certified conv input-VJP (flatConv_has_vjp W b).backward x (conv is linear,
so the saved activation x is ignored), for odd kernels. Routes through the general
IR.convBackDenote_eq_input_grad_formula; the leaf every conv slot of the ResNet chains reduces to.
Strided conv input-VJP leaf tie. flatConvStride2Back W (= convFlatBack ∘ decimateBack)
IS the certified strided conv input-VJP (flatConvStride2_has_vjp W b).backward x, for odd
kernels. Decomposes into the conv leaf tie (convFlatBack_eq_vjp_backward) and the decimate
leaf (decimateBack_eq_vjp, rfl), matching flatConvStride2 = decimateFlat ∘ flatConv.
XLA-SAME strided conv input-VJP leaf tie. flatConvStride2XlaBack W
(= convFlatBack ∘ decimateOddBack) IS the certified (flatConvStride2Xla_has_vjp W b).backward x,
for odd kernels: the conv leaf tie and the odd-scatter leaf (decimateOddBack_eq_vjp, rfl),
matching flatConvStride2Xla = decimateOddFlat ∘ flatConv. The TF-origin stems' (B0,
MobileNetV2) leaf. ⚠ This is the theorem that fixes the odd-phase backward's DIRECTION: the
emitted transposed-conv pad [p+1, p-1] (opposite to the weight grads' [p-1, p+1]) denotes
this map, so a backward derived "by symmetry" with the weight grads cannot be tied here.
Dense head input-VJP leaf tie. The chain's dense backward dense (Wᵀ) 0 (= Wᵀ·dy)
IS the certified dense input-VJP (dense_has_vjp W b).backward x (= Mat.mulVec W dy), conv is
linear so the activation x is ignored. One mul_comm per term.
GAP input-VJP leaf tie. The backward map gapBack c h w (broadcast dy(channel)/(h·w))
IS the certified GAP input-VJP (globalAvgPoolFlat_has_vjp c h w).backward x — definitionally
the same broadcast-÷ map (the VJP ignores its primal argument).