MobileNetV2's data-parallel step at SYNCHRONISED BatchNorm IS the single-device step at R·N #

MobileNetV2StepTieB.lean (T3) threads the label-smoothed loss cotangent down the batch-BN backward chain on ONE device and ties every parameter gradient node to the certified gradient. This is its data-parallel twin, for the render MobileNetV2RenderB emits at replicas > 1: R replicas at batch N, every one of the 52 BatchNorms synchronised, every parameter gradient all-reduced by its mean. The capstone mnv2_net_syncTiedB says that, for every parameter the render emits,

mean over the R replicas of replica r's gradient node, loss divided by B
  = the single-device gradient node at the global batch R·N, loss divided by R·B

— the gradient node mnv2_net_tiedB at N := R·N ties to the certified gradient. The right-hand side is the existing single-device chain at N := R·N, so the spec has not moved.

The same four steps as ResNet-34's twin #

ResNet34SyncStepTieB.lean is the template, and everything net-agnostic is imported from it rather than restated: the replica BN link bnSyncInB and its shard lemma, the ConvWSync / BnSync / DenseSync statements and their *_of_scaled closers, the divisor step replicaLossCot_eq, and the homogeneity of bnInB and cInB. The inverted-residual pieces it shares with EfficientNet-B0 — the depthwise, GAP and dense input-VJPs, the depthwise and XLA-SAME stem weight collectives — come from MBConvSyncTieB.lean.

1. Sharding — each replica's backward chain, handed its shard of a global cotangent, computes the shard of the global chain. The relu6 mask is pointwise (relu6MaskB_shard, by rfl); the conv, depthwise, XLA-SAME strided depthwise, GAP and dense input-VJPs are per-example maps; every BN link is bnSyncInB.
2. The collectives — the mean over replicas of each replica's gradient node is 1/R of the global node at the global cotangent. MobileNetV2 adds three kinds the ResNet-34 kit does not have: the XLA-SAME strided conv weight (the stem), the depthwise weight and its XLA-SAME strided peer (§4).
3. Homogeneity — the single-device chain and its gradient nodes are linear in the loss cotangent (§1): R × the cotangent gives R × every node.
4. The divisor — replica r's loss cotangent is R × its shard of the global one, and that R cancels the collective's 1/R at every parameter.

What the DP render emits, and what is tied #

At the committed convBias := false, MobileNetV2RenderB emits 158 parameter gradients — stem 3 (sW, sg, sbt), b1 6, sixteen blocks × 9 (eW eg ebt dW dg dbt pW pg pbt), head 3 (hW, hg, hbt), dense 2 (Wd, bd) — and the capstone ties all 158. ⚠ The 52 conv, depthwise and project BIAS nodes the single-device tie also states are not emitted at convBias := false and are not tied here (mnv2_net_tiedB keeps them for the flag).

What is NOT claimed #

⚠ The replicas' saved forward activations enter as the shards of the single-device forward's (batchShard r (mnv2PreB{k} (R*N) w X)); that the sync forward graph computes exactly those is StableHLO.mobilenetv2FwdGraphSync_full_shard, the forward half. ⚠ That the replicas' inputs are the shards of one batch is the driver's. ⚠ The lowerer's all_reduce is trusted as every other op's lowering is.

The block cotangents, each one line from the previous link's.

The gradient nodes MobileNetV2 adds to the ResNet-34 kit.