MobileNetV4-Conv-M's data-parallel forward at synchronised BatchNorm — replica r is shard r #

MobileNetV4FullB.lean says the typed batch-BN graph denotes mobilenetv4ForwardBFull N w on one device. MobileNetV4RenderB's data-parallel step normalises with the GLOBAL batch's statistics at replicas > 1: every one of the 77 BatchNorm sites is the sync-BN composition — this replica's mean all-reduced, then Chan's σ²_r + (μ_r − μ)² all-reduced, packed, then bnSyncF. This file is the data-parallel twin of mnv4FwdGraphBFull_faithful: that forward graph, stated as a family over the R replicas, denotes on replica r exactly batchShard r of the single-device forward at the global batch R·N.

den (mnv4FwdGraphSyncFull R hR N epsStr w bf16 e r)
  = batchShard R N nCls (mobilenetv4ForwardBFull (R * N) w X) r

given that each replica's input is its shard of one global batch X. The spec does not move: the right-hand side is the committed mobilenetv4ForwardBFull, at N := R·N.

How it is proved #

As ResNet34SyncB.lean and MobileNetV2SyncB.lean prove theirs: one block at a time, with the shard hypothesis ∀ r, den (e r) = batchShard R N _ X r carried from block to block.

• every conv, depthwise (stride 1 and SYMMETRIC stride 2), strided conv, GAP and dense node is a per-example lift (den_batchOp_shard) — the padding lives inside the per-example map;
• relu is pointwise (den_relu_shard); the identity skip is den_addVB_shard; the head's two 1×1 relabellings are den_castIdx_shard (sharding commutes with a per-example relabel);
• every BatchNorm site is bnSyncSiteLA, whose shard lemma den_bnSyncSiteLA is DataParallel.Sync's P1 (the sync-BN forward shard identity) on the graph, read at the network index.

Same shape as MobileNetV4FullB, and for its reasons. The block lemmas are generic in the row (s : UibSpec), so every width is a projection of a variable and nothing evaluates; each one closes on the row-typed mnv4BodyOfRow (R * N) s p / mnv4StridedBodyOfRow by the dispatch hypotheses MobileNetV4FullB uses (s.preDWk ≠ 0, s.postDWk = 0, …), discharged by decide at the concrete rows. The skip is one generic combinator (mnv4SkipGraphSync, the peer of mnv4SkipGraphB), which keeps the whole-net term linear in the depth. The five resolution groups are proved against mnv4Res*Layer (R * N) w through MobileNetV4FullB's _fwd_apply peels, and the whole net is a have-chain of eight stage lemmas over mobilenetv4ForwardBFull's own prefixes — no CertLayer.comp is ever peeled at a literal width.

The index seam #

The conv/relu chain runs at the left-assoc index N·(c·h·w); bnSyncF and its statistics nodes at N·(c·(h·w)). As in ResNet-34's and MobileNetV2's twins the site is ResNet34SyncB's bnSyncSiteLA, which carries the mul_assoc relabelling as castIdx on the AST value (the emitted text does not change: skel never sees an index), and den_bnSyncSiteLA reads P1 back at the network index through batchShard_castIdx. Nothing about the seam is MobileNetV4's own.

Names #

Parameter names are MobileNetV4FullB's, read off the row (%u{p}{q,e,d,p}{W,g,bt}, %f0cW, %sW, %h1W, %hW, …), and every bias operand is the shared zero %zb{c}. A BatchNorm site with γ %u{p}qg gathers its statistics as %arsum / %armean of u{p}qgmu and u{p}qgvar, each over a [c] vector — the γ name without %, then mu / var, the tag bnFwdSite is handed.

What is not claimed here #

The backward and the parameter collectives are MobileNetV4SyncStepTieB.lean's. Every conv here is bias-free by construction: MobileNetV4RenderB has no convBias flag and binds each bias slot to the zero %zb{c}, so no bias is trained and no bias gradient is emitted (the statement is ∀ w, and zero biases are one instance). bf16 selects the conv and depthwise kinds at every site, as the single-device graph does (StableHLO.PrecisionSwitch): true is the *bf16 DP renders' graph — mnv4in_emaaccdp8x128wxdowd005bf16's trunk among them — read over ℝ through Bf16Erasure, each conv's shard step erasing the switch before the f32 proof proceeds. That the R replicas' inputs are the shards of one batch is the driver's, as in DataParallel.Sync. The lowerer's all_reduce is trusted as every other op's lowering is.