3 MNIST: 2D CNN

The MLP wastes information, and we can do better

Chapter 2’s MLP recognized digits by flattening every 28\(\times \)28 image into a 784-dim vector and feeding it through three dense layers. It worked. But it worked by ignoring something the data was telling us. Pixel \((5, 5)\) and pixel \((5, 6)\) are neighbors: they were next to each other on the page where the digit was drawn. Pixel \((5, 5)\) and pixel \((23, 14)\) are not. The dense layer has no idea. It treats every input coordinate as an independent feature. Its weight matrix has no notion that some pairs of pixels are geometrically close. A trained MLP eventually learns to compensate, but it has to learn it from the data, with the data, by paying the full price for each unrelated feature pair.

A handwritten “5” drawn in the top-left of the image and the same “5” drawn in the bottom-right are the same digit. The MLP sees them as completely unrelated vectors. It can be trained to classify both, but each is its own learning problem, and nothing it learned about one transfers to the other for free.

Convolutional networks fix this by building three priors directly into the architecture, priors that the data has but the MLP threw away.

3.1 Run it first

Before any of the math, train the thing. Four commands and about a minute of GPU time:

lake exe cache get                            # Mathlib oleans, ~30 s
./scripts/datasets/download_mnist.sh          # ~11 MB
lake build mnist-cnn-verified
./.lake/build/bin/mnist-cnn-verified data

On one RTX 4060 Ti (CUDA 12.9), from runs/2026-09-01-cnn-verified-xla-cuda/. XLA’s startup banner is removed and one long line is wrapped:

[pjrt_ffi] XLA backend: PJRT 0.114, 1 device(s)
[pjrt_ffi] command buffers: enabled (CUDA default)
[pjrt_ffi] compiled verified_mlir/cnn_train_step.mlir
             (@cnn_train_step, 11 outputs, 1 replica) in 2566 ms
[pjrt_ffi] compiled verified_mlir/cnn_fwd.mlir
             (@cnn_fwd, 1 outputs, 1 replica) in 210 ms
MNIST-CNN via the VERIFIED renderer (conv→conv→pool→512→512→10) → XLA/PJRT → GPU
  xla/pjrt verified_mlir/cnn_train_step.mlir
  xla/pjrt verified_mlir/cnn_fwd.mlir
  train 60000, test 10000; bs 128, MNIST-CNN (10 params, 3489130 floats),
    mean-loss SGD lr=0.100000, He init
  epoch 1: loss = 0.352314, test_acc = 9295/10000 = 92.950000%
             [95% CI 92.43–93.44] (5219ms)
  epoch 2: loss = 0.094411, test_acc = 9749/10000 = 97.490000%
             [95% CI 97.16–97.78] (5072ms)
  epoch 3: loss = 0.056773, test_acc = 9800/10000 = 98.000000%
             [95% CI 97.71–98.26] (4888ms)
  epoch 4: loss = 0.038316, test_acc = 9819/10000 = 98.190000%
             [95% CI 97.91–98.43] (4672ms)
  epoch 5: loss = 0.026202, test_acc = 9838/10000 = 98.380000%
             [95% CI 98.11–98.61] (4357ms)
  epoch 6: loss = 0.018312, test_acc = 9853/10000 = 98.530000%
             [95% CI 98.27–98.75] (5069ms)
  epoch 7: loss = 0.022045, test_acc = 9857/10000 = 98.570000%
             [95% CI 98.32–98.78] (5537ms)
  epoch 8: loss = 0.011130, test_acc = 9859/10000 = 98.590000%
             [95% CI 98.34–98.80] (5390ms)
  epoch 9: loss = 0.006994, test_acc = 9869/10000 = 98.690000%
             [95% CI 98.45–98.89] (4808ms)
  epoch 10: loss = 0.006176, test_acc = 9861/10000 = 98.610000%
             [95% CI 98.36–98.82] (4351ms)
  epoch 11: loss = 0.004395, test_acc = 9867/10000 = 98.670000%
             [95% CI 98.43–98.88] (4647ms)
  epoch 12: loss = 0.033374, test_acc = 9877/10000 = 98.770000%
             [95% CI 98.53–98.97] (4981ms)
done (trained MNIST-CNN via the proof-rendered StableHLO).

Twelve epochs at about 4.9 seconds each, and 98.77% on the full 10,000-image test set. Two convolutions in front of Chapter 2’s classifier buy about a point over the MLP’s 97.81% (runs/2026-09-01-mlp-verified-xla-cuda/), and they do it with 3.5M parameters against the MLP’s 670K.

This is the noisiest of the three MNIST runs, and the transcript shows it. Epoch 1 landed at 92.95% here; repeated, the same twelve epochs from the same seed put it anywhere between 92.5 and 94.8%, because a convolution’s weight gradient accumulates in an order the GPU is free to vary. By epoch 12 that has largely washed out — but not in the shape the usual summary assumes, and this is the chapter to say what that means.

Run this net thirty times and twenty-nine of them land between 98.48 and 98.94%. The thirtieth lands at 97.39%. Figure 3-1 is those thirty beside the MLP’s thirty.

The MLP’s runs sit in a band; the CNN’s do too, apart from one.

Summarised as a mean and a standard deviation the CNN is \(98.73 \pm 0.27\). Summarised as a median and quartiles it is \(98.78\), with the middle half between \(98.72\) and \(98.85\). The second describes the picture above; the first does not, and the whole difference is that one run — trim the three highest and three lowest and the standard deviation falls from \(0.27\) to \(0.07\). A standard deviation assumes the spread is symmetric about the middle, and this one is not: the distribution fails a normality test outright (\(p {\lt} 10^{-4}\)), with a long left tail and nothing answering it on the right.

Three properties baked into a convolution

1. Locality. Each output value depends on only a small neighborhood of inputs. A convolution with a \(3 \times 3\) kernel computes each output pixel as a weighted sum of its 9 neighbors. Faraway pixels do not enter directly. The network only learns to combine them later, by stacking convolutions and letting receptive fields grow.

2. Translation equivariance. The same weights are applied at every spatial position, so a feature detector that recognizes the bottom-left curve of a “5” uses the same parameters whether the curve appears at row 5 or row 25, and the feature map shifts with the input. The architecture imposes the symmetry, and the data does not have to teach it. It is also why the layer is cheap: a \(3 \times 3 \times 1 \to 32\) convolution has \(3 \times 3 \times 1 \times 32 + 32 = 320\) parameters regardless of image size, where the matching fully-connected layer on a 28\(\times \)28 image would have \(28^2 \times 28^2 \times 32 \approx 20\) million.

3. Hierarchy. Digits are made of strokes, and strokes of edges. Stacking convolutions lets each layer combine the previous one’s features over a growing neighborhood, and pooling between them discards where within a window a feature fired. That is where the invariance the “5” in the corner wanted comes from: not from any one layer, but from the stack.

Concretely, a convolution computes

Each output cell is a small dot product between the kernel \(W\) and a window of the input. The sum is over a tiny \(3 \times 3\) spatial region and over input channels, usually a handful of terms rather than the 784 a dense layer touches.

The Jacobian is sparse and structured

The Jacobian of a convolution looks like a giant matrix, but it isn’t a generic giant matrix. It is mostly zeros. Specifically, \(\partial y_{c_{\text{out}}, i, j} / \partial x_{c_{\text{in}}, i', j'}\) is zero unless \((i', j')\) falls inside the kernel window centered at \((i, j)\). When it does, the entry is just the corresponding weight \(W_{c_{\text{out}}, c_{\text{in}}, k_h, k_w}\).

So a convolution is a linear map, like a dense layer, but its Jacobian is highly structured: each row has only \(k^2 \times C_{\text{in}}\) nonzero entries, and those entries are reused across many rows because the same kernel is used at every spatial position. The forward picture from Chapter 2 “the Jacobian of a linear map is the linear map” still holds. The Jacobian is just written in a different basis: instead of one big dense matrix it is a list of kernel weights plus a rule for where each one lives.

The backward of a convolution is another convolution

We want \(dx\), the way a small jiggle in each input pixel changes the loss, given an upstream \(dy\). Plugging into the Jacobian above and grinding through the algebra, the answer is:

That is itself a convolution. Specifically, it is a convolution of the upstream gradient \(dy\) against the same kernel \(W\), but with the spatial axes reversed and the input/output channel axes swapped, which is a “transposed convolution”. The backward of a CNN block reuses the same kind of operation as the forward, and no new primitive is needed.

The weight gradient \(dW\) similarly works out to a convolution, this time of the saved input \(x\) against the upstream gradient \(dy\) (the “transpose trick”). The bias gradient \(db\) is just \(dy\) summed over spatial positions per channel. Theorems 35, 36, and 37 formalize each of these.

Max pooling: the winner gets the gradient

The other new primitive in this chapter is max pooling. A \(2 \times 2\) max pool collapses each \(2 \times 2\) block of the input into a single output value: the max of the four. It has no parameters, and its purpose is to halve the spatial resolution while keeping the strongest local response.

The Jacobian of \(\max \) is degenerate. At a generic point, only one of the four inputs is the maximum, and the output’s slope is \(1\) with respect to that one input and \(0\) with respect to the other three. “Jiggle the max” moves the output, and “jiggle a non-max” does nothing. So the backward of max pool routes the upstream gradient back to whichever input was the winner in each window, and zeros out the rest. At a tie the emitted select_and_scatter sends the whole cotangent to the first maximal cell, which is a different convention from ReLU’s mask, and the pdiv-derived backward is \(\operatorname {fderiv}\)’s zero map there, as at ReLU’s corner. Definition 39 states this formally.

The rest of the network is Chapter 2

After two convolutions and a max pool, the feature map is \(14 \times 14 \times 32\). At that point we flatten the \(14 \cdot 14 \cdot 32 = 6272\)-dim feature vector and feed it into the same three-dense-layer head from Chapter 2, ending in 10-class logits. The backward through the dense head and the softmax-CE loss is exactly the calculation of Chapters 1 and 2, and we do not re-prove it here. The composition rule from Chapter 1 guarantees that the full network’s VJP is just the per-layer VJPs strung together in reverse order: softmax-CE backward, dense backward \(\times 3\), flatten backward, max-pool backward, conv2d backward \(\times 2\). Each piece is its own theorem, and together they form a working trainer for MNIST that respects the image’s 2-D structure.

3.2 The theorems

Figure 3-2 is the dependency graph of this section.

Those are the primitives. The rest of the section is the network: its VJP at a smooth input, then the three certificates about training it — the emitted step is the certified step, each gradient node is the loss’s derivative, and one SGD step descends.

3.3 Example: MNIST 2D CNN

Chapter 2’s MLP flattened the image and threw dense layers at it. This chapter does MNIST again with the structure kept, the way the first book’s Chapter 2 did: two plain \(3 \times 3\) convs to pull out local features, a max-pool to collapse the spatial grid, then the same dense head you already know.

Architecture

Figure 3-3 is the network.

Two convolutions lift the 1-channel grayscale input to 32 channels, maxPool halves the spatial resolution, then the flattened \(14 \times 14 \times 32 = 6272\) feature vector goes through three dense layers into 10-class logits. No batch norm yet, because BN shows up in Chapter 4.

Code: the full training program

Same format as the MLP chapter. The only thing that changes from Chapter 2’s training program is the layers list. This is the spec §3.1 actually ran.

-- 1
import LeanMlir.Verified.NetsCore
import LeanMlir.Verified.Train

-- 2
def cnnVerified : VerifiedNetSpec where
  name     := "MNIST-CNN"
  slug     := "cnn"
  inC      := 1
  imageH   := 28
  imageW   := 28
  data     := .mnist
  layers   := [.conv 1 32 3 1, .relu, .conv 32 32 3 1, .relu, .maxPool 2 2,
               .flatten,
               .dense 6272 512, .relu, .dense 512 512, .relu, .dense 512 10]
  blurb    := "MNIST-CNN via the VERIFIED renderer
                (conv→conv→pool→512→512→10) → %LOWERER% → GPU"
  lossSlot := true

-- 3
def cnnConfig : VerifiedConfig where
  epochs    := 12
  batchSize := 128

-- 4
def main (argv : List String) : IO Unit :=
  cnnVerified.toNet.train cnnConfig (argv.head?.getD "data")

Walking through the numbered sections:

1. The import. Same as Chapter 2.

2. The architecture. Eleven entries: two .conv layers at 32 channels, a .maxPool, a .flatten, three .dense layers down to 10, and four .relus between them. .conv ic oc k stride takes in-channels, out-channels, kernel size and stride — no activation argument, because activations are their own entries here rather than a field on the layer that precedes them. That is why Chapter 2’s five-entry list became eleven and not seven.

The .conv2d backward pass is the theorem from earlier in this chapter (Theorem 35): the input VJP is another convolution, using the kernel reversed along both spatial axes. The max-pool backward (Definition 39) routes the gradient to the argmax position in each \(2 \times 2\) window. The dense backward is Theorem 19. Adding convolution to the model introduces no new training-loop code, only new layer types, which the framework already knows how to compose.

Two fields carry over from Chapter 2 and do the same jobs: blurb is the banner the run prints, and lossSlot declares that this render returns a trailing report-only %loss, which is the one line of verified_mlir/cnn_train_step.mlir that is not pretty of a proven graph node — the render labels it as such in a comment of its own. Everything else in the file is: Proofs.StableHLO.cnnTrainStepText emits it, and CnnFold proves that each of the ten parameter updates denotes the certified softmax cross-entropy loss-descent step derived from the Mathlib \(\operatorname {fderiv}\) math. Both convolutions, the max pool, the three dense layers and the SGD update are proof-backed operations.

3. The training hyperparameters. Twelve epochs at batch 128, SGD, no regularization and no augmentation. Note what a VerifiedConfig does not carry: the learning rate. It is baked into verified_mlir/cnn_train_step.mlir, which is §1.6’s point in a second chapter — the rate is inside the reach of the proofs, so it cannot be set to one thing and trained at another.

4. The program entry point. One line, same as the MLP chapter. cnnVerified.toNet.train cnnConfig replaces mlpVerified.toNet.train mlpConfig. That’s the whole diff.

What .conv, .maxPool and .flatten contribute.

Three more arms on Chapter 1’s toSpecs, and only one of them carries parameters:

  | conv ic oc k _ => #[(#[oc,ic,k,k],0),(#[oc],2)]   -- W, bias
  | maxPool _ _    => #[]
  | flatten        => #[]

Pooling and flattening are pure reshapes of data, so they have nothing to initialise — which is the parameter-list statement of the same fact the backward passes above make: maxPool2’s VJP routes gradient without owning any, and flatten’s is a reshape. Fold the eleven-entry list through those arms and you get the 10 params, 3489130 floats the run printed: two conv kernels and their biases, three dense matrices and theirs.

Results

The run in §3.1 is the result. Figure 3-4 is its per-epoch training loss, against Chapter 2’s MLP on the same recipe.

The CNN sits below the MLP through epoch 11 and reaches by epoch 5 a loss the MLP has not reached by twelve. Test accuracy is 98.77% against the MLP’s 97.81%.

The exception is the last point, and it is the interesting one. The CNN’s training loss bumps at epoch 7 and then jumps almost eightfold at epoch 12, from \(0.0044\) to \(0.0334\) — far enough to cross back above the MLP’s \(0.0291\). That is ordinary SGD at \(\text{lr}=0.1\) rather than a measurement artifact. And the run’s test accuracy is at its highest on that same epoch, 98.77%. Training loss and held-out accuracy are different measurements, and a figure where the two disagree this loudly is the one to remember when a later chapter asks you to read a loss curve.

Both curves come off the binaries these chapters’ theorems describe.

Why this network is still 99% dense-head

At 3,489,130 total parameters, the no-BN CNN is actually \(\sim \)5.2\(\times \) bigger than the MLP, not smaller. You might have expected the opposite, because convolutions are supposed to be parameter-efficient. They are, but the head is what’s eating the budget: the flatten of a \(14 \times 14 \times 32\) feature map produces a 6272-dim vector, and the first dense layer (6272 \(\to \) 512) alone is 3,211,776 parameters. The entire conv+maxPool backbone is 9,568 parameters, which is 0.27% of the total.

This is the same “fat FC head” pattern you’ll see in AlexNet, VGG, and YOLOv1: a compact convolutional backbone spending its parameter budget on a large fully-connected classifier. ResNet (Chapter 5) is the first architecture in this book without one: its head is a globalAvgPool followed by a single small dense layer, which is why ResNet-18 (a smaller version of ResNet-34) has \(\sim \)11M parameters for 1000-class ImageNet but Chapter 3’s 10-class MNIST CNN has 3.5M.

The fat head is fat because it can be, not because it must be

If the dense head holds 99% of the parameters, the obvious question is how many of them earn their keep. The parametric renderer answers it directly: mnist-cnn-grid holds the convolutional backbone fixed at 32 channels and sweeps only the dense head (\(\ldots {\to }d{\to }d{\to }10\)), rendering each width from the faithful CNN emitter. Figure 3-5 overlays that sweep on the MLP’s (both trained on their own verified StableHLO), and shows how little the head needs once good convolutional features exist.

The whiskers are not an interval, just the highest and lowest the configuration actually produced. Eight of the ten widths repeat to within 0.4 and their whiskers are barely visible. The other two do not: \(d=512\) dropped one run to 96.66% and \(d=4096\) one to 93.52%, which is what the two long tails are.

Those tails are the reason this curve is a median of five. A symmetric error bar would have been the wrong shape for them — four runs cluster and one falls away, so there is no spread to put a \(\pm \) on — and the 95% interval on the test set, \(\pm 0.22\) at this accuracy, would have hidden a five-point failure behind a rounding error. The MLP points are single runs, which Chapter 2 reads with half a point of give.

The cost is that a handful of runs cannot see this. Draw five of the thirty runs in §3.1, build the ordinary 95% interval on their mean, and ask whether it contains the mean of the twenty-five you did not draw: it does 79% of the time, not 95%, because five draws usually miss the tail and report a spread as small as \(0.05\) against the true \(0.27\). Chapter 2’s MLP, whose thirty runs are unremarkable, gets 92% from the same procedure. How many runs a claim needs is a property of the network, and a convolution’s is higher than a dense stack’s. The early epochs of a conv net are not a measurement; the last one is, and even then not from a single run.

The whole CNN curve sits about a point above the MLP’s, and it is flat across the entire range: an 8-wide head already reaches 98.2% at 60K parameters, beating the widest 4096-wide MLP. So the 3.2M-parameter \(6272{\to }512\) layer is not buying accuracy, because shrinking the head to \(\ldots {\to }8{\to }8{\to }10\) keeps essentially all of it. The head is fat because the flatten hands it a 6272-vector and nobody trimmed it, not because the task needs the width.

3.4 MLIR: Convolution

What is already proven. mnistCnnNoBnForward is the conv \(\to \) relu \(\to \) conv \(\to \) relu \(\to \) maxPool \(\to \) flatten \(\to \) dense network, and mnistCnnNoBnHasVJPAt (Theorem 40) proves its reverse-mode derivative by chaining the per-layer VJPs: the dense backward (Theorem 19), the max-pool backward (maxPool2HasVJP3, Definition 39), and the convolution backward (conv2dHasVJP3, Theorem 35), all through the IR-level chain rule vjpCompAt. The convolution’s reverse-mode derivative is the chapter’s headline result: the input VJP of a conv2d is another conv2d, against the kernel with its in- and out-channels swapped and both spatial axes reversed. The parameter gradients are pinned by conv2dWeightGradHasVJP (the transpose trick) and the dense grads (Theorems 20, 21), and the loss gradient by softmaxCE_grad (Theorem 22). So what the convolution’s gradient is, is not in question.

The gap and how we close it. The emitted backward convolution is given a denotation \([\! [\cdot ]\! ]\) valued in the proofs’ own tensor type,

where \(\bar k = K - 1 - k\) is the spatial flip, and the bridge theorem

says the denotation of that graph is the proven conv input-VJP. It holds at every channel count, image size and odd kernel size at once: per output coordinate the reversed-kernel sum and the gradient formula of Theorem 35 are the same finite sum under the reindexing \(k \leftrightarrow K-1-k\) (reverseSlab_eq_gradSlab), and that reindexing is a bijection exactly when \(K - 1 - p = p\), which is oddness (hkH, hkW).

The committed step of the chapter’s network, verified_mlir/cnn_train_step.mlir, carries that graph at the trained shape, \(1{\to }32{\to }32\) channels at \(28\times 28\), batch 128. Here are the three operators the chapter added, as the backward pass meets them: the max-pool, the second ReLU, and the second convolution’s input gradient (SSA names the artifact’s, default precision dropped, lines wrapped, the select_and_scatter body elided):

%v50 = stablehlo.reshape %v17 : (tensor<128x25088xf32>)
      -> tensor<128x32x28x28xf32>
%v51 = stablehlo.reshape %v49 : (tensor<128x6272xf32>)
      -> tensor<128x32x14x14xf32>
%v52 = stablehlo.constant dense<0.0> : tensor<f32>
%v53 = "stablehlo.select_and_scatter"(%v50, %v51, %v52) ({
// ...
%v58 = stablehlo.compare GT, %v56, %v57 : (tensor<128x32x28x28xf32>,
      tensor<128x32x28x28xf32>) -> tensor<128x32x28x28xi1>
%v59 = stablehlo.select %v58, %v55, %v57 : tensor<128x32x28x28xi1>,
      tensor<128x32x28x28xf32>
// ...
%v62 = stablehlo.transpose %W2, dims = [1, 0, 2, 3]
      : (tensor<32x32x3x3xf32>) -> tensor<32x32x3x3xf32>
%v63 = stablehlo.reverse %v62, dims = [2, 3] : tensor<32x32x3x3xf32>
%v64 = stablehlo.convolution(%v61, %v63)
      dim_numbers = [b, f, 0, 1]x[o, i, 0, 1]->[b, f, 0, 1],
      window = {stride = [1, 1], pad = [[1, 1], [1, 1]],
      lhs_dilate = [1, 1], rhs_dilate = [1, 1]}
      {batch_group_count = 1 : i64, feature_group_count = 1 : i64}
      : (tensor<128x32x28x28xf32>, tensor<32x32x3x3xf32>)
      -> tensor<128x32x28x28xf32>

Read it against the graph, bottom up. %v62 is the transpose dims [1,0,2,3] that swaps the kernel’s out- and in-channel axes, and %v63 is the reverse dims [2,3] that flips both spatial axes (\(\bar k_h, \bar k_w\)). Together they build reverseSwap \(W_2\). The convolution at %v64 convolves the incoming cotangent %v61 against that kernel, exactly \(\texttt{conv2d}\, (\texttt{reverseSwap}\, W_2)\), the \(32 \leftarrow 32\) adjoint of the forward conv, under the same pad = [[1, 1], [1, 1]] the forward used. Above it, %v58/%v59 is the ReLU mask at the saved pre-activation %v56, the second convolution’s output, and %v53 is the max-pool backward: select_and_scatter walks each \(2\times 2\) window of the pre-pool activation %v50 with a GE select, which picks the window’s first maximal cell, and scatters the pooled cotangent %v51 onto it with add. That is the lowest-index tie-break of Definition 39 written as an operation.

Three theorems cover the three. conv_back_bridge is the convolution; maxPoolBack_faithful says the select_and_scatter denotes maxPoolFlatHasVJPAt’s backward wherever every window has a single maximum (MaxPool2Smooth); the ReLU mask is Chapter 2’s relu_back_bridge. Theorem 41 then composes them at batch 128. Its slice lemmas identify example \(k\)’s slice of %v61, the cotangent entering the second convolution’s backward, with the certified chain (dhc2B_slice), and the slice of %v70, the cotangent at the first convolution’s output once the first ReLU’s mask %v69 is applied to %v64, with the certified chain through conv_back_bridge (dhc1B_slice), which is where the odd-kernel hypothesis enters. The cotangent each convolution’s weight update is stated at is the slice of these emitted operations, not a hand-named value beside them. One detail of printing: this per-example renderer writes transpose then reverse, and the batched renderers of Chapters 5 onward write reverse then transpose. The two kernels are the same tensor, since swapping the channel axes and flipping the spatial ones commute, and the batched graph Theorem 41 reads this file at carries a descriptor (convBackP) for exactly this order, so that the printed text does not change.

Caveats.

• The convolution bridge holds at every input, for odd kernels. A convolution is linear, so there is no hypothesis on \(x\); the one hypothesis is on the kernel shape, \(k_H\) and \(k_W\) odd, and every kernel in Chapters 3–7 is. Where a net has an even kernel (ConvNeXt’s \(4\times 4\) stem and \(2\times 2\) downsamples, Chapter 8) the tie passes the kernel zero-extended to the next odd size (padOdd), which is the asymmetric pad the emitter writes there.

• ReLU is a smooth-point bridge (no pre-activation exactly zero), stated only off that set, which is null for generic weights.

• Max-pool is a smooth-point bridge too. It holds where every \(2\times 2\) window attains its maximum at one cell (MaxPool2Smooth); the other cells may tie with each other. An all-zero post-ReLU window fails it, so for pooling the excluded set is not null the way ReLU’s corner is, and the whole-net theorem states it as a hypothesis (h_mp in Theorem 40).

• Shape. The listing is the trained net; the bridge theorems are shape-general and the tie is stated at batch 128.

3.5 Recap

Two operations, and the first whole-network theorem with a hypothesis in it. The convolution is a linear map, so its backward needs no hypothesis on the input: for an odd kernel it is a convolution of the cotangent against the kernel with its channel axes swapped and its spatial axes flipped, which is what the emitted transpose and reverse compute. The max-pool is the second convention after ReLU’s, argmax ties broken by the lowest index, and its bridge holds where every window has one maximum. An all-zero window after ReLU fails that, so the excluded set is not null, and Theorem 40 carries it as a stated hypothesis rather than hiding it. Theorems 41 and 42 tie the four convolution updates and every gradient node to the loss’s derivative, ties included, and Theorem 43 is the descent through the convolutions.

The network is two convolutions deep, and that is as deep as this recipe goes: the MNIST head holds nearly every parameter, and the width sweep shows the head barely matters once the features are good. Going deeper, on a harder dataset, is where two things start to bite that nothing so far has needed, a normalization inside the stack and a choice of optimizer. The next chapter adds the one operator whose gradient needs real analysis to bound.