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

EfficientNetStepTieG.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 EfficientNetRender emits at replicas > 1: R replicas at batch N, every one of the 49 BatchNorms synchronised (bnFwdSite / bnBackSite / bnGammaSite), every parameter gradient all-reduced by its mean. The capstone efficientnet_net_syncTiedG says that, for every parameter,

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 EnetTiePoCG.efficientnet_net_tiedG at N := R·N ties to the certified gradient. The spec it is stated against has not moved: the right-hand side is T3's chain at N := R·N — its forward prefixes, loss cotangent and block .backwards verbatim, and its in-block cotangents as named definitions (xCotEc, tCotDn, …) that unfold to enetExpTiedG's lets, so each right-hand node is T3's node by rfl.

Five steps #

ResNet-34's four (ResNet34SyncStepTieB.lean), and one B0 needs because of how its T3 is written.

0. The block VJP is the chain (§ 0). T3 threads each block's input cotangent as a certified VJP's .backward; a replica computes its own by the explicit chain, and only the explicit chain can be sharded. xCotIn_eq_vjp and its four peers say the two agree — the EfficientNetBackB0 stage graphs, read at an .operand leaf, with bnBatchLABack_faithful turning the one non-rfl link into bnBackB.
1. Sharding (§§ 2, 5). Every non-BN link is per-example — conv, depthwise and strided depthwise input-VJPs, swish and sigmoid masks, and the squeeze-excite backward: the gate cotangent gateCotB (seReduceB's den) and the fused input-VJP seInB (seBackBatched's) both read one example at a time, so they shard like ResNet-34's pool backward. The BN link is bnSyncInB, P2 on the graph, read through bnInB_eq_bnBackB onto T3's bnBackB.
2. The collectives. ResNet-34's conv, dense and BatchNorm ones, plus the depthwise, strided-depthwise and XLA-SAME stem conv weights from MBConvSyncTieB.lean, which also holds the depthwise, GAP and dense links of steps 1 and 3 that MobileNetV2 shares (§ 3 moved there).
3. Homogeneity (§§ 1, 4). Every link is linear in its cotangent; most are a certified VJP's .backward, so HasVJP.backward_smul is the whole proof.
4. The divisor. Replica r's loss cotangent is R × its shard of the global one (replicaLossCot_eq), and steps 1–3 carry that R down to cancel each collective's 1/R.

What is covered, and what is NOT claimed #

The DP render runs convBias := false, so it emits 213 parameter collectives — stem 3, b1 10, fifteen MBConv6 blocks × 13, head 5 — and all 213 are tied. T3 carries 49 more conjuncts, one per conv bias (a bnBetaGradB at the conv-output cotangent), for the convBias := true census; the DP artifacts do not emit them and they are not tied here.

⚠ The replicas' saved forward activations enter as the shards of the single-device forward's; that the sync forward graph computes exactly those is EfficientNetSyncB's efficientnetFwdGraphSync_full_shard, the forward half. ⚠ That the replicas' inputs are the shards of one batch is the driver's. ⚠ T3 states the chain without stochastic depth or classifier dropout, so this does too: the drop / dropdo DP variants add a dropPathB on each residual branch and a dropoutB before the classifier — per-example diagonal scalings, which shard and are linear, but whose chain neither tier states. The bf16 DP variants emit different gradient nodes and are not covered. ⚠ The lowerer's all_reduce is trusted as every other op's lowering is.

The tail's forward activations, from the depthwise conv output dc — enetExpTiedG's dn, dr, s, e1, z, e2, se, pc, definitionally.

The tail's backward chain from the block-output cotangent dy — enetExpTiedG's cotPbn … cotDc, definitionally.

The stride-1 expand front (b3, b5, …, and the widenings b9 / b16).

The strided front (b2, b4, b6, b12): expand at the input grid 2h×2w.

The MBConv1 front (b1): the depthwise runs on the block input.

The stem (enetStemTiedG's chain) and the head (enetHeadTiedG's).

The stage backwards, written out #

Each is the EfficientNetBackB0 stage graph's faithfulness read at an .operand leaf: the graph's den IS the chain above node for node, except the BatchNorm link, which bnBatchLABack_faithful turns into bnBackB.

Each block's input cotangent IS its certified VJP #

T3 threads the block-output cotangents by the block VJPs' .backward; the replicas compute theirs by the explicit chain. These say the two agree, so the sharding argument (which needs the explicit chain) lands on T3's own .backward terms. HasVJP.backward_unique swaps the bundle-level witness for the unfolded one, which is then the stage composition by rfl.