A mean of losses is differentiable where its summands are.

⭐ The gradient of a mean is the mean of the gradients. Linearity of pdiv, and the only analysis in this file: pdiv_const_smul pulls the 1/M out and pdiv_finset_sum splits the sum. Everything downstream is this lemma read at two index meanings.

⭐⭐ What the collective computes, named as a gradient. The all-reduced mean of the R per-replica gradients IS the gradient of the mean of the R per-replica losses.

No hypothesis on the losses beyond differentiability — in particular this holds for a training-mode BatchNorm net, where each L r genuinely depends on the whole of replica r's slice. That is the point: it names what a data-parallel run minimises without claiming that function is the global-batch loss (dpMeanGrad_ne_globalBatchGrad).

⭐⭐ Sharding a per-example loss is invisible to the mean. If replica r's loss is the mean over its own N examples, then the mean of the R replica losses is the mean over all R·N examples — as FUNCTIONS, before any derivative is taken.

Stated at an arbitrary e, so which examples land on which replica does not enter: the contiguous slices the DP shim cuts (finProdFinEquiv), the interleave ds.shard produces for the sharded producers, and any other partition all give the same theorem.

⭐⭐ For a net with no batch coupling the data-parallel step IS the single-device step at the global batch R·N. meanLoss_shard under lossGrad.

"No batch coupling" is the hypothesis's shape, not a side condition: it is spelled by giving replica r the loss meanLoss (fun n => ℓ (e (r, n))) — a mean of per-example terms — which a training-mode BatchNorm net's replica loss is not.

The contiguous shard — replica r owns examples [N·r, N·r + N) — as an instance. This is the split VerifiedTrain.lean's DP path cuts (elems / replicas).

⚠ The two shards ARE the global batch, under the contiguous split — replica r owns example r. Without this the witness below would be comparing two unrelated datasets and would prove nothing; a comparison against a re-derivation tests the re-derivation.

The gradient of a linear form, which is all bnToyLoss needs.

bnToyLoss's gradient is the squared slice mean, at every coordinate of Vec 1.

⛔⛔ With batch coupling the previous section is FALSE, and here is the witness. Two replicas, one example each — slices {0} and {2}, global batch {0, 2}. The data-parallel mean gradient is (0² + 2²)/2 = 2; the gradient of the global-batch loss is 1² = 1.

So a training-BN net trained data-parallel did NOT take a step on the batch-R·N loss, at any learning rate and however small the gradients. What it took a step on is the mean of the R per-replica batch-BN losses, which is dpMeanGrad_eq_grad_meanLoss — a different function, and the only honest answer to "what trained". ⚠ The witness needs no BatchNorm: ANY nonlinear read of a per-slice statistic separates the two, which is why the split is structural rather than a property of the normalisation's formula.

The replica mean of the shard sums is 1/R of the global sum. Pure re-indexing: the R shard sums together run over every one of the R·N examples exactly once.

⭐⭐ The positive twin of dpMeanGrad_ne_globalBatchGrad: with SYNCHRONISED statistics the data-parallel step IS the single-device step at the global batch R·N.

Write the global-batch gradient as a mean of per-example terms, (1/(R·N)) Σ_m c m — the shared-weight batch sum every *GradB node denotes, at the cotangent the global backward delivers to example m. Under sync-BN each c m depends on the WHOLE batch through the all-reduced statistics; that is allowed, and it is what separates this from dpMeanGrad_eq_globalBatchGrad_of_perExample, whose c m had to be a per-example loss's own gradient. What sync-BN buys (P1–P3, PerChannelBN.lean / DataParallelSync.lean) is that replica r's backward is the shard-r block of the global one, so replica r's gradient node is (1/N) Σ_n c (e (r, n)) — ITS examples' terms of the global sum. Then the collective's mean over R of those is the global mean: meanLoss_shard's arithmetic, for vectors.

⛔ Per-replica BatchNorm fails exactly here: replica r's cotangents are then NOT the shard-r block of any global backward, and the witness above is the two-example case.

The contiguous shard — replica r owns examples [N·r, N·r + N) — as an instance, the split VerifiedTrain.lean's DP path cuts.

From a shared state, one DP step lands every replica on the same state again — the induction step, and it is definitional: the all-reduced gradient does not depend on r, and neither does the state the tail is applied to.

⭐⭐ The lockstep induction. Identical initial states and an identical (all-reduced) update keep the R copies equal at every step, so n steps of the R-replica system are n steps of the single-device one. This is the property VerifiedTrain.lean relies on when it checkpoints from replica 0 — the checkpoint is not "replica 0's answer", it is every replica's.

⚠ The shared start is a HYPOTHESIS (the fun _ => st on the left). That the driver broadcasts it, and that replica_groups names all R devices, is calling logic and the *-dp-check gates are its evidence.

⭐⭐ What function trained, in one statement. When each replica's gradient is the certified gradient of its own loss, one data-parallel step is one ordinary step on the MEAN of the R per-replica losses.

⭐⭐ n steps of R replicas ARE n steps of single-device training on the mean loss. The lockstep induction and the gradient mean, composed — the closing statement of §4d piece 1, and the one that answers the disclaimer every tie in the repo carries.

⚠ Differentiability is asked for at EVERY point, not just at θ, because the trajectory passes through states the statement cannot name. For a relu net that is the one place this file is stronger than it needs to be: the honest weakening is differentiability along the trajectory, and it costs a mutual induction the payoff does not justify.