Residual additive-fan-in backward faithfulness (general). If fBack denotes the body's VJP backward (den fBack = hf.backward x dy), then the residual backward graph denotes the proven residual_has_vjp backward, which is f.backward x dy + dy. The proof is structural — the only definitional facts are den (addV a b) = den a + den b and the identity skip's backward = dy — so it composes without a whole-net terminal rfl.

The renderable batch-norm input-grad IS the certified backward — both equal the pdiv-contracted Jacobian (bnBatchTensor4_grad_input_correct, bnBatchTensor4_has_vjp_correct).

bnBatchBack (true batch-norm backward) faithfulness. The first batched-backward primitive: bnBatchBack denotes the proven bnBatchTensor4 VJP backward (batch-COUPLED batch-norm on [N,C,H,W], reduce over [0,2,3] per channel) via the renderable three-term bnBatchTensor4_grad_input. This is the genuinely-new op the batched MBConv stages need (their bn is bnBatchLA, not a per-example batchMap); the other batched stages (conv/depthwise/SE) are batchMap of the per-example backwards already proven above. The bnBatchLA layout-reindex wrapper to the network's N·(oc·h·w) index is a thin remaining layer.

Batched conv input-VJP faithfulness. convBackBatched denotes the proven VJP of the batched conv batchMap N (flatConv W b) — i.e. the per-example conv input-grad applied independently across the batch. Conv is linear, so its backward ignores the forward activation; the batched backward is a plain batchMap of the per-example backward, matching batchMap_has_vjp. The second batch-separable stage brick (after seB); together with bnBatchBack these are the batched MBConv's per-stage backward pieces.

Batched STRIDE-2 conv input-VJP faithfulness. The stride-2 analogue of convBackBatched_faithful: convStridedBackBatched denotes the proven VJP of the batched strided conv batchMap N (flatConvStride2 W b) — i.e. the per-example strided-conv input-grad (flatConvStride2_has_vjp = zero-upsample the cotangent then the reversed-kernel conv) applied independently across the batch. Strided conv (decimate ∘ conv) is linear, so its backward ignores the forward activation; the batched backward is a plain batchMap of the per-example backward, matching batchMap_has_vjp. The downsample basic-block's stride-2 conv1 backward brick.

Batched STRIDE-2 depthwise input-VJP faithfulness. The stride-2 analogue of depthwiseBackBatched_faithful (and the depthwise analogue of convStridedBackBatched_faithful): depthwiseStridedBackBatched denotes the proven VJP of the batched strided depthwise batchMap N (depthwiseStride2Flat W b) — i.e. the per-example strided-depthwise input-grad (depthwiseStride2Flat_has_vjp = zero-upsample the cotangent then the reversed-kernel per-channel depthwise) applied independently across the batch. Strided depthwise (decimate ∘ depthwise) is linear, so its backward ignores the forward activation; the batched backward is a plain batchMap of the per-example backward, matching batchMap_has_vjp. The EfficientNet downsample MBConv's stride-2 depthwise backward brick.

Batched XLA-SAME STRIDE-2 depthwise input-VJP faithfulness. The odd-phase peer of depthwiseStridedBackBatched_faithful: depthwiseStridedXlaBackBatched (pad [p+1, p-1], the token MobileNetV2's Adam render emits at its four strided depthwises) denotes the proven VJP of batchMap N (depthwiseStride2FlatXla W b). Same proof: a scatter onto the odd positions is as linear as one onto the even ones.

Batched depthwise input-VJP faithfulness. The depthwise analogue of convBackBatched_faithful: depthwiseBackBatched denotes the proven VJP of the batched depthwise batchMap N (depthwiseFlat W b). Depthwise conv is linear, so its backward is activation-independent and the batched backward is a plain batchMap of the per-example backward. The MBConv depthwise stage's batch-separable backward brick.

bnBatchLA backward = reindex-conjugated bnBatchTensor4 backward. The network indexes at N·(oc·h·w) (left-assoc) but the proven true-BN bnBatchTensor4 lives at N·(oc·(h·w)); bnBatchLA bridges by conjugating with the associativity-cast reindexes (bnBatchLA_eq_comp). Its VJP backward is therefore: scatter the cotangent into [N,C,(H·W)], run the renderable three-term bnBatchTensor4_grad_input at the reindexed activation, scatter back. This is what a network-layout bnBatchLABack op denotes.

bnBatchLABack (network-layout true batch-norm backward) faithfulness. The den (inline scatter-conjugated bnBatchTensor4_grad_input) equals the proven bnBatchLA_has_vjp backward — the bn backward at the network's N·(oc·h·w) index. This is the layout wrapper that lets bnBatchBack compose with convBackBatched / depthwiseBackBatched (all on the left-assoc index) into batched stages.

seBackBatched (batched squeeze-excite backward) faithfulness. The den (rowwise application of the proven per-example seBlockFull VJP) equals the proven batched seB_has_vjp backward. SE is non-linear, so — unlike the linear convBackBatched/depthwiseBackBatched — the backward threads each example's forward activation v; the rowwise batchMap_has_vjp structure handles that. The fourth (and last) MBConv stage's batch-separable backward.

⭐ The tie's BN node and the emitted BN node denote one map. Every batched render emits .bnBatchBack, typed at N·(oc·(h·w)); the ties state the BN input cotangent at .bnBatchLABack, its network-layout N·(oc·h·w) twin (ResNet34TieB.bnInB). The two print the same text, and their dens differ only by the associativity relabelling reassocB: the two scatters inside bnBatchLABack's den collapse because Fin.cast is a bijection.

The certified BN input cotangent every batched T3 tie threads IS the emitted bnBatchBack node's den, read back through reassocB. This is the missing half of bnBatchLABack_faithful: that lemma certifies the tie's node, this one says the render's node computes the same numbers.

…and it IS the certified bnBatchLA VJP, for every β and every 0 < ε. This is bnBatchLABack_faithful, and it is the only step in this file's cotangent chain that is not rfl — everything else (the relu masks, the conv and strided-conv input-VJPs, the pool backward) denotes its certified backward definitionally.

…and it IS the den of the node the render emits, .bnBatchBack at the N·(oc·(h·w)) index, read back through reassocB (EnetTiePoC.den_bnBatchLABack_eq_bnBatchBack).