Data parallelism, piece 2: the collective as an AST node #
DataParallel.lean (piece 1) is the ℝ-level half: dpMean, the replica mean of gradients, IS
the gradient of the mean of the per-replica losses, and that mean is the global-batch loss for a
net with no batch coupling and provably is not for a batch-BN net. What it could not say was
anything about the ARTIFACT, because the collective was ViTRender.emitGradAllReduce — emitted
text outside the SHlo AST, a declared trusted carve-out that every train-step tie in the repo
disclaimed in its own header.
Since 2026-09-07 the collective is SHlo.allReduceMeanF: R graphs of one skeleton (the same
program on R replicas, each with its own values — SPMD), reduced by all_reduce(add) and
divided by R. Its den is (1/R) Σ_r den (g r), its skel reads replica 0, its emit is the
old text verbatim (allReduceMeanText), and the parser round-trip has its case
(StableHLOParse.parseStack). Every batched render now calls prettyAllReduceMean where it
called the text function, and every committed *dp* artifact re-rendered byte-identically.
This file is what the node BUYS, stated once:
den_allReduceMeanF_eq_dpMean— the node denotesdpMeanof its operands' denotations, which is the definition piece 1 is about.skel_allReduceMeanF_of_spmd— under the SPMD hypothesis (∀ r, skel (g r) = skel (g 0), free in every render because a render's operand family is.operand gradat everyr) the node's skeleton is each replica's, soprettyprints ONE program.den_allReduceMeanF_eq_lossGrad_meanLoss— piece 1 composed: if each replica's node denotes its own loss gradient, the all-reduced node denotes the gradient of the MEAN loss.den_allReduceMeanF_convWeightGradB— 4b's fold composed: the all-reduced conv weight-gradient node denotes the replica mean of the certifiedΣ_ngradients. One op kind shown; every other*GradBcomposes the same way, byFinset.sum_congrover the replicas and its own fold lemma.adamW_at_allReduceMeanF— the tail composed:den (adamW tail (allReduceMeanF …))isadamWStepatdpMeanof the per-replica gradient nodes. That isplanning/archive/proofs_tier_to_paper_nets.md§4d piece 2's target statement.
What is NOT claimed #
⚠ Piece 3 is untouched: that the R graphs' values are the replica slices of ONE host batch,
that every replica starts from the same parameters and that replica_groups names all R
devices are the driver's (VerifiedTrain.lean, ffi/pjrt_ffi.c) and the *-dp-check gates'.
⚠ The per-replica gradient node's operand values differ per replica by construction; nothing
here says what they are. ⚠ The lowerer's all_reduce is trusted exactly as every other op's
lowering is.
The node denotes dpMean of its operands. Definitional: den's arm is piece 1's formula.
SPMD: the R graphs of one skeleton. Under the hypothesis that every replica's operand
graph has replica 0's skeleton — free in every render, whose operand family is .operand grad
at every r, and the content of "the same program on R replicas" — the node's skeleton is
each replica's, so pretty prints ONE program and den sums R of them.
⭐ Piece 1 composed with the node. If each replica's gradient node denotes the gradient of
that replica's loss, the all-reduced node denotes the gradient of the MEAN of the per-replica
losses — the function a data-parallel run minimises (dpMeanGrad_eq_grad_meanLoss).
⭐ 4b's fold composed with the node. The all-reduced conv weight-gradient node denotes the
replica mean of the certified batched Σ_n gradients, each at its own replica's activations
and cotangent. One op kind; every other *GradB composes identically (Finset.sum_congr
over the replicas, then its own fold lemma).
⭐⭐ The optimizer tail at the all-reduced node — §4d piece 2's target statement:
den (tail (allReduceMeanF R g)) is adamWStep at dpMean of the per-replica gradient
nodes. adamW_triple_faithful is ∀ e, so this is that theorem at e := allReduceMeanF …
and the node's den; the same one line closes it for every other certified tail
(mom_pair_faithful, rmsProp_triple_faithful, lamb_triple_faithful).