The Chapter-4 cifarCnn forward, in flattened Vec space. The conv stack runs at spatial (2·(2h), 2·(2w)); the first maxPool halves it to (2h, 2w) (where the second conv stage runs), the second to (h, w); then three dense layers (two with ReLU). With the real CIFAR shapes ic=3, c1=32, c2=64, h=w=8, d1=512, nClasses=10, kH=kW=3 the input width is 3·32·32 = 3072 and the flattened pool output is 64·8·8 = 4096.

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

The composed backward of the full Chapter-4 forward equals the pdiv-contracted Jacobian, conditional on smoothness at the six ReLU kinks and the two MaxPools. Built by vjpCompAt through convRelu → convRelu → maxPool → convRelu → convRelu → maxPool → denseRelu → denseRelu → dense. The Chapter-4 sibling of mnistCnnNoBnHasVJPAt (two conv stages, two pools).

16 distinct positive values, 4×4 row-major ⇒ positionally injective. Typed at the 2·(2·1) spatial form so it lines up syntactically with the forward's stage-1 input shape (no 2*2 vs 2*(2*1) cast friction).

Whole-network input, the flattened T0 (Vec 16).

Every conv: 1→1, 1×1 unit kernel ⇒ identity.

Dense heads: nonnegative weights + a strictly-positive bias keep every activation off the ReLU kink.

Unconditional whole-network VJP for a concrete tiny CIFAR CNN. Every smoothness hypothesis of cifarCnnHasVJPAt is discharged — the two no-tie conditions via positional injectivity (maxPool2Smooth_of_injective, the second through pool1_inj), the six ReLU conditions via positivity — so the statement carries no side conditions and stays in the three-axiom closure.

The deeper (8-conv) CIFAR forward, flattened. Four conv→conv→pool stages (ic→c1→c1, c1→c2→c2, c2→c3→c3, c3→c4→c4) then dense 3-head.

Deeper (8-conv) CIFAR CNN (no BN) whole-network VJP at a smooth point. Conditional on the ten ReLU kinks (eight conv, hf1 … hf8; two dense, hf9, hfa) and the four MaxPools (hp1 … hp4); built by vjpCompAt through convRelu×8 / maxPool×4 / denseRelu×2 / dense. The 4-stage sibling of cifarCnnHasVJPAt. No concrete instance of this 4-stage net is proved; Tiny.cifarTinyCnnHasVJPAt is a concrete instance of the 2-stage cifarCnnHasVJPAt with every side condition discharged.

conv → per-channel-BN → relu block VJP at a smooth point. The per-channel (bnPerChannelTensor3, m=h·w) sibling of convBnReluHasVJPAt: the same two vjpCompAt chain with bnPerChannelTensor3 (vector γ/β [oc], its own block-diagonal VJP) in place of the scalar-global bnForward.

The 8-conv CIFAR forward with per-channel BatchNorm (bnPerChannelTensor3) between each conv and its ReLU, flattened: four conv→BN→relu→conv→BN→relu→pool stages, then the dense 3-layer head. The BN peer of cifarCnn8Forward.