The MNIST-MLP train step at batch N — MlpFold with the batch stated #

MlpFold certifies the six parameter outputs of mlp_train_step.mlir for ONE example. tests/TestSmallNetsBatchedEmit.lean pins that same text as the print of a graph at the batched index — batchOp lifts of dense/relu/expe/softmaxDiv/dotOut, subB, selectPosB on the whole-batch pre-activations, and the denseWeightSgdB/denseBiasSgdB nodes — so every node's den can be read at a batch of N examples. This file does that reading:

• the batched forward's slices are the per-example forward (preB0_slice, …);
• the batched loss cotangent's slices are softmax(logitsₖ) − onehotₖ (cotB_slice);
• the batched chain cotangents' slices are the per-example mlpCotOut1/mlpCotOut0 (cot1B_slice, cot0B_slice);
• each of the six parameter nodes denotes θ − lr·Σₖ (certified per-layer Jacobian at example k · that example's chain cotangent), and the output weight W₂ − lr·Σₖ ∂CE(forwardₖ)/∂W₂ (mlp_train_step_tiedB). N is a binder; the artifact is N = 128.

The chain cotangents are node-local, as in MlpFold: each parameter node is stated with its cotangent input as an .operand leaf carrying the den of the batched backward subgraph, which the slice lemmas pin. Scope otherwise as MlpFold (per-op pretty lexing; ℝ → Float32).

Per-example shorthands, at example k of the batch #

The batched graph, piece by piece (the pieces mlpTrainStepText renders) #

The backward chain: selectPosB on the whole-batch pre-activation over a dotOut lift #

The six parameter nodes at batch N #