The MNIST-CNN train step at batch N — CnnFold with the batch stated #

CnnFold certifies the ten parameter outputs of cnn_train_step.mlir for ONE example. tests/TestSmallNetsBatchedEmit.lean pins that text, byte for byte, as the print of a graph at the batched index: batchOp lifts of conv/relu/maxPool/dense/expe/softmaxDiv/ dotOut, subB, selectPosB, maxPoolBackB, the convBackP descriptor (the per-example conv input-VJP spelling, at the batched index) and the convWeightSgdB/convBiasSgdB/ denseWeightSgdB/denseBiasSgdB nodes. This file reads every node's den at a batch of N:

• the batched forward's slices are the per-example forward (hc1B_slice, …, logitsB_slice);
• the batched loss cotangent's slices are softmax(logitsₖ) − onehotₖ (cotB_slice);
• the batched backward chain's slices are the per-example chain — the dense head's mlpCotOut1/mlpCotOut0, then CnnChainClose's cnnChainCotW2 (relu mask over the select-and-scatter pool-back of the head cotangent) and, for odd kernels, cnnChainCotW1 (relu mask over the reversed-kernel conv-back) — dhc2B_slice, dhc1B_slice;
• each of the ten parameter nodes denotes θ − lr·Σₖ (certified per-layer Jacobian at example k · that example's chain cotangent), the output weight at the whole loss (cnn_train_step_tiedB). N is a binder; the artifact is N = 128.

Unlike CnnFold, the chain cotangents here ARE the emitted subgraphs' denotations (the pool-back and conv-back are maxPoolBackB/convBackP nodes, not the hand-named cnnChainCot* values), so the "cotangent SSA ↔ chain-cot per-op trust" CnnFold's Scope records is closed at the batched index: dhc2B_slice/dhc1B_slice prove the two readings agree.

Scope #

• per-op den ⇄ MLIR text (shared with the suite); the committed-bytes tie is CI's regenerate-and-diff plus the batched-emit pin; ℝ → Float32 is FloatBridge.
• dhc1B_slice's identification with cnnChainCotW1 needs odd kernels (hkH, hkW): the reversed-kernel conv is the conv input-VJP only there (IR.conv_back_bridge). The node theorems themselves carry no such hypothesis; the artifact's kernels are 3×3.

Per-example shorthands at example k (the forward CnnFold states, at slice k) #

The batched forward, nested #

The batched backward chain — each piece a node over an operand leaf carrying the previous #

piece's den, as the renderer threads them

The ten parameter nodes at batch N #