conv → relu block VJP at a smooth point (no BatchNorm). relu ∘ flatConv W b. The plain-conv analogue of convBnReluHasVJPAt — conv is linear (global VJP via the HasVJP3 bridge), relu carries the smoothness hypothesis.

dense → relu block VJP at a smooth point. relu ∘ dense W b.

The Chapter-3 mnistCnnNoBn forward, in flattened Vec space. Conv stage runs at spatial (2*h, 2*w); the maxPool halves it to (h, w); then three dense layers (two with ReLU).

MNIST 2D CNN (no BN) whole-network VJP at a smooth point.

The composed backward of the full Chapter-3 forward equals the pdiv-contracted Jacobian (Jacobian-transpose applied to the cotangent), conditional on smoothness at the four ReLU kinks and the one MaxPool. Built by vjpCompAt through convRelu → convRelu → maxPool → denseRelu → denseRelu → dense. The Chapter-3 sibling of cnnHasVJPAt (BN-free, no resblocks).

A concrete 3-layer MLP (dense → relu → dense → relu → dense) with all-ones weights/biases and a positive input. Every ReLU pre-activation is then strictly positive (hence ≠ 0), so both smoothness hypotheses of mlpHasVJPAt discharge. The net is non-constant, so this is a live witness (non-trivial Jacobian), not a degenerate one.

Unconditional whole-network VJP for a concrete 3-layer MLP. Both ReLU ≠ 0 hypotheses are discharged via dense_pos_of_nonneg (positive bias + nonnegative weights/input propagate strict positivity), with relu_id_of_pos collapsing the inner ReLU.

Whole-network VJP for a concrete ResNet-style CNN with BatchNorm — every smoothness hypothesis discharged: the stem produces distinct positive BN outputs (so maxpool has no ties and bn ≠ 0), and the resblock BNs use γ=0 (constant).