PoC: the CIFAR-CNN (Chapter 4, no-BN) train step, proof-tied to the certified SGD step #

The Chapter-4 peer of CnnFold — a deeper, two-spatial-scale conv net ((conv→relu)×2 → pool → (conv→relu)×2 → pool → (dense→relu)×2 → dense; 14 params: 4 conv kernels/biases + 3 dense layers). MainCifarVerified trains on verified_mlir/cifar_train_step.mlir; this file makes its parameter updates den-faithful — each emitted SGD op denotes the certified loss-descent step.

Zero new core ops. The conv layers reuse the convWeightSgd/convBiasSgd ops added for cnn (CnnFold); the dense head reuses weightSgd/biasSgd. The only new content is the per-net den = certified capstones below.

• Conv layers (all four): convW_den/convB_den are generic in the conv dims and the cotangent c — den (convWeightSgd … (.operand _ c)) = θ − lr·(certified ∂conv/∂θ · c), the emitted op's den reduced (rfl) to the LHS of the generic cnn_render_conv{W,b}_certified. Instantiated at each conv layer's (b,x,W) and the cotangent the renderer feeds there, they certify W₁/b₁ … W₄/b₄ (one lemma each, all four layers — conv2d's weight/bias VJP is dim-generic).
• Dense head (W₅/W₆/W₇): the classifier head is a 3-layer MLP over the flattened pool output, so its cotangents are the IR mlpCotOut0/1 and its dens close via the M2 weight_grad_bridge/bias_grad_bridge — verbatim CnnFold (dW7_den, the op the tie reads).

Honest residual (same boundary as cnn/mlp/linear) #

• The conv cotangents here are free variables c (the convW_den/convB_den statement is ∀ c) — so the lemmas hold at the actual backward-chain cotangent the renderer feeds, without naming it. Pinning each c to the exact emitted backward subgraph (the CnnChainClose recipe, scaled to two stages) is the remaining polish.
• Per-op pretty lexing + ℝ → Float32.

Conv layers — generic den = certified (covers all four conv layers) #

Dense classifier head (W₅/W₆/W₇) — weightSgd/biasSgd, mirrors CnnPoC #

The head pool2 → W₅→relu→W₆→relu→W₇ is a 3-layer MLP; per-layer cotangents are the IR mlpCotOut0/1 (with (W₇,W₆,W₅) playing the MLP's (W₂,W₁,W₀)). Every head op's den = certified is Cifar8PoC.denseW_den / Cifar8PoC.denseB_den at that layer; only the output-layer weight op is stated here, as the tie reads it.

The §1a tie — the conv layers/dense head, tied through the REAL cifar forward #

The conv/dense *_den theorems above hold for a FREE cotangent (convW_den/convB_den are ∀ c; the dense head's mlpCotOut0/1 are ∀ dy). The capstones below pin those cotangents to the ones the real cifar forward + softmax-CE loss actually drives — the cifar peer of CnnFold's last three theorems (cnnLossCot_den / cnn_W5_tied_totalloss / cnn_conv_tied_certified).

cifar is the cnn shape with two conv→conv→pool stages instead of one, so its conv backward chain crosses an extra pool boundary. Three of the four conv-layer cotangents reuse the cnn chain cots verbatim (every one is generic in its downstream cotangent):

• W₄ (last conv before pool₂): cnnChainCotW2 W₅ W₆ W₇ h5 h6 ac4 hc4 g — relu₄ mask on the pool₂ input-VJP of the dense-head cotangent (the cnn conv₂ pattern, at the cifar head dims).
• W₃: cnnChainCotW1 W₄ hc3 cotW4 — relu₃ mask on conv₄'s input-VJP (the cnn conv₁ pattern).
• W₁: cnnChainCotW1 W₂ hc1 cotW2 — relu₁ mask on conv₂'s input-VJP (same pattern).

Only W₂ needs a new constructor cifarChainCotW2: its cotangent crosses pool₁ at the relu-free conv₃-input boundary, so it is relu₂ mask on maxpool₁-back(conv₃-back(W₃, cotW3)) — a conv input-VJP then a maxpool input-VJP, the step cnn (one pool) never had.