Batched global average pool as a CertLayer. Globally certified — GAP is linear.

Batched dense classifier as a CertLayer. Globally certified — dense is affine.

Transport a VJP along a local equality. pdiv reads only the germ of the map at the point (it is an fderiv), so a witness for f is one for any g that agrees with f near x, with the same backward. How a map that is not globally a composite of certified pieces still gets a certified VJP: the ReLU-then-pool stem is locally a gather.

The stem pool's condition, per example: every 3×3 window of the post-ReLU stem activation has its maximum at one position, or is entirely zero (a window of dead ReLUs). A tie is a property of one image's window, so the condition is stated on each row of the batch.

Real batches have many all-zero windows, and the pool alone has no derivative at any of them; the stem layer is certified as ReLU and pool together (stemReluPoolLayer), where a dead window is locally constant. What is still excluded is a window whose maximum is POSITIVE and attained at two positions. On real ImageNet batches such windows occur in every batch, and they come from two cells reading IDENTICAL input patches (flat image regions); there the stem has no derivative in the image, so an input-gradient statement must exclude them, but the two cells are the same function of the stem's weights, so the loss is still differentiable in the parameters; the loss-gradient statements take the weaker StemPoolTwinAt, which allows them. The probe script scripts/probes/stem_pool_smooth_probe.py counts all three kinds of window.

The batched argmax gather: output (r, k) reads example r's argmax cell for k.

The batched ReLU-then-pool's VJP at a smooth-or-dead pre-activation: scatter to the argmax cells, then the ReLU mask.

The stem pool's condition along a parameter, per example: every window of the post-ReLU stem activation is dead, or has its maximum strictly above every cell at another position except the positions T r twins with it (MaxPool3s2SmoothUpTo). Weaker than StemPoolSmoothAt (stemPoolTwinAt_of_smoothAt). It is what a parameter gradient needs: twinned cells tie at every parameter value, so the pool's choice between them does not move (stemPoolRelu_param_eventuallyEq_select).

A pool selector at y: output (r, co, ho, wo) reads a cell of its own 3×3 window (example r, channel co) that holds the window's maximum. Where a window's maximum is attained once, every selector reads that cell; at a tie each picks one of the tied cells. The argmax gather maxPool3s2LocalReindexB is one selector (maxPool3s2LocalReindexB_isSelect), and so is the render's select_and_scatter with its GE select, which routes each window's cotangent to one maximal cell (the first in window order).

The gather model's VJP: scatter along σ, then the ReLU mask.

The ResNet stem, strided conv-BN-ReLU then the 3×3/s2 pool, as ONE certified layer.

It is one layer, not cbReluStridedLayer.comp of a pool layer, because the pool alone is not differentiable at a window of dead ReLUs, and real batches have many. Together they are: near the input the pooled stem is the argmax gather of the ReLU output (stemPool_eventuallyEq), so its VJP is the conv-BN-ReLU stage's after the gather's scatter, and that scatter is what the render's maxPool3s2BackB denotes (maxPool3s2FlatBackB_eq_reindex). The forward and the backward graph are the two-layer composite's, so the rendered stem is unchanged; only the certification domain grows.