PoC: the MNIST-CNN train step, proof-tied to the certified SGD step #

The CNN analogue of LinearFold / MlpFold. MainMnistCnnVerified trains on verified_mlir/cnn_train_step.mlir; this file makes the parameter updates of that module den-faithful — each emitted SGD op denotes the certified (fderiv/VJP-derived) softmax-CE loss-descent step.

The CNN has two kinds of parameter: the dense classifier head (W₃,W₄,W₅ + biases — structurally a 3-layer MLP over the flattened pool output) and the convolution kernels/biases (W₁,W₂ + biases). The dense head reuses the weightSgd/biasSgd SHlo ops added in LinearFold (its dens certified via the M2 weight_grad_bridge/bias_grad_bridge at the mlpCotOut-style chain cotangents — the head is a 3-layer MLP, so the IR mlpCotOut0/1 apply verbatim). The conv layers use the new core ops convWeightSgd/convBiasSgd (StableHLO.lean): their den is flatten(W − lr·conv2d_weight_grad…) / b − lr·conv2d_bias_grad…, proven = certified by the chain-pinned conv bridges cnn_render_conv{W,b}{1,2}_chain_certified (CnnChainClose.lean) at the cotangents the CNN backward chain actually delivers (cnnChainCotW1/cnnChainCotW2).

(Namespace/name lengths are kept short on purpose: tests/AuditAxioms.lean's three-axiom closure check greps #print axioms output per line, which Lean wraps past ~120 cols — long qualified names would split the benign triple across lines and false-fail the check.)

What is closed here (kernel, [propext, Classical.choice, Quot.sound]) #

• cW1_den/cb1_den/cW2_den/cb2_den — the four emitted conv param ops (convWeightSgd/convBiasSgd), fed the chain cotangent, denote the certified conv kernel/bias loss-descent step. The conv tail is now "under den" exactly like the forward.
• dW5_den — the output-layer dense-head op (weightSgd) denotes the certified dense loss-descent step; the other five head ops are Cifar8PoC.denseW_den / Cifar8PoC.denseB_den at their layer.

Honest residual (the boundary shared with the forward SHlo den) #

• Cotangent subgraph ⇄ rendered SHlo. The cotangents here are the chain cotangents (cnnChainCotW1/2, mlpCotOut0/1), proven = the rendered backward form in CnnChainClose (cnnChainCotW{1,2}_eq) and IR (mlpCotOut*_denote); pinning each to the exact emitted selectPos/dotOut/convBack/maxPoolBack SHlo subgraph (as MlpPoC.cot{0,1}_den does for the MLP) is the remaining polish.
• Per-op pretty lexing (shared with the whole suite) + ℝ → Float32.

Convolution layers — the new convWeightSgd/convBiasSgd ops denote certified #

den (convWeightSgd … (.operand _ c)) is by construction flatten W − lr·conv2d_weight_grad(b,x)·c (and likewise for the bias); pinning c to the cotangent the chain delivers and applying the chain-certified conv bridge gives θ − lr·(certified ∂conv/∂θ · the-chain-cotangent). (The den reduction is definitional — rfl — exactly as LinPoC.poc_weightSgd_den_eq.)

Dense classifier head — reuse weightSgd/biasSgd (the head is a 3-layer MLP) #

The pool-output pool : Vec (c·h·w) flows through W₃→relu→W₄→relu→W₅; the per-layer cotangents are exactly 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.

Tie (dense head) — the top loss cotangent is the composed softmax-CE of the CONV forward #

The cnn *_den_certified above hold for a free top cotangent dy and a free pool output. The renderer feeds the cotangent the emitted loss graph sub(softmaxDiv(expe(logits)), onehot) produces, with logits the REAL conv-forward output mnistCnnNoBnForward … x. The lemma below pins that graph to the composed softmax-CE gradient of the conv forward (the cnn analogue of mlpLossCot_den), and the headline folds the dense output weight W₅ to the whole-loss gradient ∂CE/∂W₅ — so the output layer is tied forward(conv+dense)→softmax-CE→gradient. (The CONV layers W₁/W₂ need the conv backward chain composed — the hand-written selMask4/scatter/convBack rendered as SHlo + the conv cotangent-subgraph pins — which is the bigger conv-side work; see §1a of the planning doc.)

The CONV fold — the conv kernels/biases tied through the real conv forward #

The four conv *_den theorems above hold for FREE conv activations (ac1/ac2/hc2) and a free cotangent. The capstone below instantiates them at the real conv forward (ac1/hc1/hc2/ac2 = the actual conv₁/relu/conv₂/relu outputs, h3/h4 the dense pre-acts the head-backward reads) and the composed top cotangent g = softmax(mnistCnnNoBnForward x) − onehot (cnnLossCot_den). So all four conv param ops denote θ − lr·(certified ∂convₖ/∂θ · the conv backward-chain cotangent the real loss drives) — cnnChainCotW2 for conv₂, cnnChainCotW1 W₂ hc1 cotW2 for conv₁ (it crosses one more conv-back). Together with the dense head (cnn_W5_tied_totalloss + the *_den at the composed cotangent) the WHOLE cnn train step is now den-composed forward→loss→backward — no free activations, no symbolic cotangent. (Residual: the conv backward is rendered hand-written, so the cotangent SSA ↔ cnnChainCot correspondence is the per-op trust, same kind the whole suite carries; making it a printed SHlo subgraph with a den pin — the cnn analogue of MlpPoC.cot{0,1}_den — is the polish.)