Batched conv → bn → relu6 stage (MobileNetV2 expand), at the network layout N·(oc·h·w). Identical to EfficientNet's cbsB but with relu6 for swish.

Batched depthwise → bn → relu6 stage (MobileNetV2 depthwise), at the network layout. Identical to EfficientNet's dwbsB but with relu6 for swish.

Batched STRIDE-2 depthwise → bn → relu6 stage (MobileNetV2 downsample depthwise), at the network layout. The stride-2 analogue of dwbrB: maps the larger input spatial c·(2h)·(2w) to the output spatial c·h·w. Identical to EfficientNet's dwbsSB but with relu6 for swish.

Generic relu6-on-batched-bn-stage _at VJP. The relu6 analogue of bnSwishStage_has_vjp, but _at (relu6 only has a pointwise VJP): compose the batched-op VJP, the true-BN VJP (both global, lifted via .toHasVJPAt), and relu6's pointwise VJP at the pre-relu6 activation.

cbrB (conv-bn-relu6) _at VJP at a smooth point.

dwbrB (depthwise-bn-relu6) _at VJP at a smooth point.

dwbrBstrided (STRIDE-2 depthwise-bn-relu6) _at VJP at a smooth point. The stride-2 analogue of dwbrB_has_vjp_at: lifts depthwiseStride2FlatXla_has_vjp (the strided per-channel conv input-VJP) through the generic relu6-bn stage.

Batched conv → bn → relu6 stage backward graph (MobileNetV2 expand): convBackBatched ∘ bnBatchLABack ∘ selectMid, each at its cumulative forward activation. The relu6 analogue of cbsBackBatchedGraph — .selectMid (the relu6 two-sided-kink mask) replaces .swishBack.

Batched depthwise → bn → relu6 stage backward graph (MobileNetV2 depthwise).

Batched STRIDE-2 depthwise → bn → relu6 stage backward graph (MobileNetV2 downsample depthwise). The stride-2 analogue of dwbrBackBatchedGraph: the bn/relu6 run at the OUTPUT spatial h×w, then depthwiseStridedBackBatched maps the bn-cotangent back to the larger input c·(2h)·(2w) (zero-upsample + reversed-kernel per-channel depthwise). The relu6 back is .selectMid as before.

The conv → bn → relu6 stage as a CertLayer, certified where its pre-relu6 activation misses both kinks. The kernel extent is a binder, so the same layer is a 1×1 or a 3×3.

The depthwise → bn → relu6 stage as a CertLayer.

The stride-2 depthwise → bn → relu6 stage as a CertLayer: 2h × 2w in, h × w out.

The conv → bn stage (projB, no activation) as a CertLayer. Globally certified (ok = True): with no activation there is no kink.

Batched conv → bn → relu stage (ResNet basic-block first stage), at the network layout N·(oc·h·w). The relu analogue of MobileNetV2's cbrB (relu for relu6).

Generic relu-on-batched-bn-stage _at VJP. The relu analogue of bnRelu6Stage_has_vjp_at (and of bnSwishStage_has_vjp, but _at — relu only has a pointwise VJP): compose the batched-op VJP, the true-BN VJP (both global, lifted via .toHasVJPAt), and relu's pointwise VJP at the pre-relu activation. The smoothness hypothesis is the one-sided ≠ 0.

cbReluB (conv-bn-relu) _at VJP at a smooth point.

Batched conv → bn → relu stage backward graph (ResNet basic-block stage 1): convBackBatched ∘ bnBatchLABack ∘ selectPos, each at its cumulative forward activation. The relu analogue of MobileNetV2's cbrBackBatchedGraph — .selectPos (the relu one-sided-kink mask) replaces .selectMid.

The conv → bn → relu stage as a CertLayer, certified where its pre-relu activation misses 0. The kernel extent is a binder, so the same layer is a 1×1 or a 3×3.

Batched STRIDE-2 conv → bn → relu stage (downsample basic-block first stage), at the network layout N·(oc·h·w) ← N·(ic·(2h)·(2w)). The strided sibling of cbReluB (flatConvStride2 for flatConv); halves spatial.

cbReluStridedB (strided conv-bn-relu) _at VJP at a smooth point. The strided sibling of cbReluB_has_vjp_at (flatConvStride2 for flatConv).

Batched strided conv → bn → relu stage backward graph: convStridedBackBatched ∘ bnBatchLABack ∘ selectPos, each at its cumulative forward activation. The strided sibling of cbReluBackBatchedGraph — convStridedBackBatched (the new stride-2 batched-conv VJP) replaces convBackBatched.

The strided conv → bn → relu stage as a CertLayer — cbReluLayer with flatConvStride2.

Batched strided conv → bn projection skip (downsample basic-block skip): bnBatchLA ∘ batchMap (flatConvStride2) — the 3×3 stride-2 projection that matches the body's downsampled oc·h·w output. The strided sibling of projB (flatConvStride2 for flatConv); no activation (linear bottleneck).

Batched strided conv → bn projection-skip backward graph: convStridedBackBatched ∘ bnBatchLABack, at the skip's forward activation. The strided sibling of projBackBatchedGraph.

The strided conv → bn projection skip as a CertLayer — projLayer with flatConvStride2, globally certified.