ReLU backward (the rendered selectPos): keep dy i where the saved pre-activation was positive (cond i), else 0. The mask cond is fixed — the smooth-point sign pattern, which is what the ties' nonzero-kink hypotheses pin.

Smooth-activation backward (the rendered emitActBack/scale): multiply the cotangent pointwise by the saved derivative s = act'(preact). GELU, Swish/SiLU and sigmoid all have a diagonal Jacobian, so their backward is this single multiply at a fixed vector s.

Apply a per-token map f : Vec d → Vec d to every row, on the flattened Vec (n·d) (Mat.unflatten → per-row f → Mat.flatten). The whole-sequence form of a per-token op (LayerNorm, the MLP sub-block), so it can compose with a cross-token attention.

Per-token-input-aware flat lift. Each row r gets its OWN per-token map g r, rather than the single shared f of perRowFlat. The flat analogue of rowwiseHasVJPMat's row-wise lift (Tensor.lean): the seam a BACKWARD needs, because a per-token op's input-VJP depends on that token's saved activation (LayerNorm-back threads the saved input, GELU-back the saved pre-activation), so one shared map cannot carry it. perRowFlat f is the special case g = fun _ => f (perRowFlatPR_const). Read block-diagonally it is also the per-block lift — block hd gets g hd — which is the per-head form of perRowFlat (multi-head attention: heads = blocks) and the per-channel form the BN / channel-LN backwards use.

Conv backward in flat Vec space — dx = convBackDenote W dy. The emitted convolution(dy, reverse(transpose(W))) denotes a forward conv2d (reverseSwap W) 0, which in flat space is flatConv (reverseSwap W) 0. The backward of flatConv W b (Vec (oc·h·w) → Vec (ic·h·w)); convFlatBack_eq_vjp_backward ties it to the certified VJP at odd kernels, and EvenKernelConvBack.lean says why an even kernel is not its own adjoint.

Decimation backward (zero-upsampling scatter) — the certified decimateFlat VJP: route dy k to the even position decimateIdx k, 0 elsewhere. Vec (oc·h·w) → Vec (oc·2h·2w). The StableHLO lhs_dilation=[2,2] of a transposed conv.

Odd-decimation backward (zero-upsampling scatter at the odd positions) — the certified decimateOddFlat VJP: route dy k to the odd position decimateOddIdx k, 0 elsewhere. Vec (oc·h·w) → Vec (oc·2h·2w). The odd-position sibling of decimateBack; the map the emitted [p+1, p-1] transposed-conv pad of an XLA-SAME stride-2 conv denotes.

Stride-2 conv backward in flat Vec space — the input-VJP of flatConvStride2 W b = decimateFlat ∘ flatConv: zero-upsample the cotangent (decimateBack), then run the reversed-kernel conv (convFlatBack). Vec (oc·h·w) → Vec (ic·2h·2w). The symmetric-pad (ResNet) stem and down-blocks; tied by flatConvStride2Back_eq_vjp_backward.

XLA-SAME stride-2 conv backward in flat Vec space — the input-VJP of flatConvStride2Xla W b = decimateOddFlat ∘ flatConv (StridedConv.lean): scatter the cotangent onto the ODD positions (decimateOddBack), then run the reversed-kernel conv. The odd-phase peer of flatConvStride2Back — the TF-origin stems of EfficientNet-B0, MobileNetV2 and MobileNetV4; tied by flatConvStride2XlaBack_eq_vjp_backward.

Stride-4 patchify conv backward in flat Vec space — the input-VJP of flatConvStride4 W b = decimateFlat ∘ decimateOddFlat ∘ flatConv: zero-upsample the cotangent twice (decimateBack then decimateOddBack), then run the reversed-kernel conv. Vec (oc·h·w) → Vec (ic·4h·4w). The ConvNeXt 4×4/s4 stem's backward.

Spatial reversal of a depthwise kernel — reverse both spatial axes (kRev k = kH−1−k), keeping the channel axis (depthwise has no cross-channel mixing, so no transpose, unlike the regular conv's reverseSwap). The kernel the codegen feeds to the backward depthwise stablehlo.convolution (reverse [2,3], feature_group_count = c).

Depthwise conv backward in flat Vec space — the emitted reversed-kernel depthwise convolution denotes a forward depthwiseConv2d (dwReverse W) 0, which in flat space is depthwiseFlat (dwReverse W) 0. The backward of depthwiseFlat W b (Vec (c·h·w) → Vec (c·h·w), channels preserved); tied by depthwiseFlatBack_eq_vjp_backward through depthwiseConv2d_dwReverse_eq_input_grad_formula.

XLA-SAME stride-2 depthwise conv backward in flat Vec space — the input-VJP of depthwiseStride2FlatXla W b = decimateOddFlat ∘ depthwiseFlat (Depthwise.lean): scatter the cotangent onto the ODD positions, then the reversed-kernel depthwise conv (MobileNetV2's four strided depthwises, B0's strided MBConvs); tied by depthwiseStride2FlatXlaBack_eq_vjp_backward.

Global-average-pool backward — the certified GAP VJP: route dy(channel) to every spatial cell of that channel, divided by h·w. Vec c → Vec (c·h·w). The head endpoint of every conv net's backward chain (r34InputGradB, mnv2InputGradB, efficientnetInputGradBFull, …); the emitted SHlo.gapBack denotes globalAvgPoolFlatHasVJP's backward, which is this map.

3×3/s2 max-pool backward in flat Vec space — the accumulating scatter: each input cell collects dy from every output whose 3×3 window selects it. Note: maxPool2's windows TILE, so the 2×2 pool's backward (StableHLO.maxPoolBackFlat) is a lookup; 3×3/s2 windows OVERLAP, so an input cell can be the argmax of up to four outputs and this is a reduction. Spelled as the masked sum the kernel performs, which is maxPool3s2HasVJPAt3's backward reindexed (maxPool3s2FlatBack_eq_vjp_backward).

The pool VJP at a Vec point, with its backward DEFINITIONALLY maxPool3s2FlatBack. maxPool3s2FlatHasVJPAt is stated at Tensor3.flatten x, and a whole-net chain needs it at the stem's Vec output. Note: Transporting with ▸/rwa would work for the TYPE and leave a backward field behind an Eq.mpr that will not reduce. Building the structure field-by-field instead keeps backward the leaf itself, which is what lets the whole-net ties (ResNet34BackCertifiedTieB, ResNet34FullBVJP's batched pool) close by rfl at this stage rather than by a rewrite.

The 3-layer MLP input-gradient VJP at a smooth point: dy ↦ Wᵀ₀·(mask₁ ⊙ Wᵀ₁·(mask₂ ⊙ Wᵀ₂·dy)). The certified backward of dense W₂ ∘ relu ∘ dense W₁ ∘ relu ∘ dense W₀ (input gradient), the ReLU kinks read off the fixed sign masks c₁/c₂.

The batched 3×3/s2 max-pool backward — maxPool3s2FlatBack per example, on that example's OWN saved stem activation. Note: It is batchMapAux and not batchMap: a batchMap would hand example 0's argmax pattern to every example (StableHLO.batchMapAux's own header records the same trap on the emitter side). This IS den (.maxPool3s2BackB …): den_maxPool3s2BackB_eq_flatBackB below equates the two spellings of the scatter (BackLinks.mpInB is the maxPool3s2BackFlat one).