The MNIST-linear train step at batch N — the fold LinearFold leaves open #

LinearFold certifies linear_train_step.mlir's two outputs for ONE example: its nodes (weightSgd/biasSgd over lossCotGraph) denote per-example values, and the file says so ("the committed module batch-contracts over B examples, which this file does not state"). This file states it. The same text is the print of a graph at the batched index — batchOp lifts of dense/expe/softmaxDiv, subB, and the denseWeightSgdB/denseBiasSgdB nodes whose den sums the per-example gradient over batchSlice n — and tests/TestSmallNetsBatchedEmit.lean pins that print byte-for-byte to linTrainStepText at the committed shape. So:

• lin_train_step_tiedB — at a batch of N examples with labels label : Fin N → Fin n, the weight output denotes W − lr·Σₖ ∂CE(dense(W,b)·xₖ, labelₖ)/∂W and the bias output b − lr·Σₖ (certified ∂dense/∂b · (softmax(zₖ) − onehotₖ)), for every N.
• lin_weight_meanlossB — at lr = α/N the weight output is one step of gradient descent at rate α on the batch-MEAN loss, which is the step the trainer takes (0.00078125 = 0.1/128).

Scope #

• per-op den ⇄ MLIR text, as in LinearFold; the committed-bytes tie is CI's regenerate-and-diff plus the batched-emit pin; ℝ → Float32 is FloatBridge.

Two node lemmas every batched dense fold uses #

denseWeightSgdB/denseBiasSgdB denote θ − lr·Σₖ (per-example gradient at slice k) by definition; these read that off at an index. The two collapse lemmas turn the certified dense Jacobian contracted with a cotangent into the closed form the node computes.

Slice lemmas for the batched backward-chain nodes #