MobileNetV2's T3 §1a TIE at TRUE BATCH-NORM — the un-fused, batched whole-net thread #

MobileNetV2FoldPaperG.lean (4b.4) makes every parameter GRADIENT node of the batched MobileNetV2 train step den-faithful for an arbitrary cotangent. This file removes the "arbitrary": each cotangent is pinned to the one the emitted backward chain delivers, so the whole train step is den-composed forward → loss → backward with no free activation and no symbolic cotangent. With 4.2b it completes MobileNetV2's T3, and it is ResNet34StepTieB.lean's peer.

⭐⭐ The block cotangents are NOT derived here. 4.2b's mnv2{ExpOnly,Resid,Strided,NoExp}B_has_vjp_at ARE the certified block backwards, and mnv2{Body,DownBody,ResidBlock}BackBatchedGraph_faithful (MobileNetV2BackB0.lean) already prove the emitted backward subgraphs denote exactly them. The four *CotIn_eq_vjp lemmas below are those statements in this file's vocabulary, and they are what make the cross-block thread a composition of certified VJPs rather than a re-derivation.

⭐ One parameter-tie bundle covers twelve of the seventeen blocks. A skip block and a stride-1 widening have the SAME parameter cotangents — the identity skip changes only the dx handed to the previous block, which is why MobileNetV2RenderB's irBackStride1GradB is one function with a skip flag rather than two near-copies. So mnv2Stride1TiedB is stated once and instantiated at b3, b5, b6, b8–b13, b15, b16 (skip) and b11, b17 (no skip).

⭐ The loss cotangent is the LABEL-SMOOTHED one, at a general target, shared with ResNet-34: Foundation/SmoothedLossCot.lean. MobileNetV2RenderB composes it from the same six kit ops (softmaxRow → subB → scaleB → addVB → shiftB → divConstB) with α at 0.1 and the target arriving as the graph input %onehot — a soft vector under mixup or cutmix.

⭐ N is a binder. The artifacts at 32 (mobilenetv2_adam_train_step) or 64 (mobilenetv2in_rmsdp64) are instances. T3 carries no numerals.

⛔ The all-reduce, since 4d piece 2 (2026-09-07). In mobilenetv2in_rmsdp64 each *GradB node feeds allReduceMeanF — the collective as an AST node whose den is the replica MEAN of the per-replica gradient nodes; until then emitGradAllReduce, emitted text and a declared carve-out outside the SHlo AST. Every statement below is at the PER-REPLICA gradient node; DataParallelNode.lean composes it with the mean and the tail.

⚠ bnInB and bnInB_eq_bnBackB are ResNet-34's, imported rather than copied. They are the batched BatchNorm input-cotangent written as the den of the emitted backward op, and its identity with the certified bnBatchLA VJP — both net-agnostic, and they happen to live in the file that first needed them. What MobileNetV2 adds is the TWO-SIDED relu6 mask (relu6MaskB, where r34 threads the one-sided reluMaskB), the depthwise input-VJP and its XLA-SAME strided peer.

The parameter census is 158, and this file states 210 slots #

MobileNetV2RenderB defaults to convBias := false: every conv, depthwise and project bias is folded into the BatchNorm that follows it and bound to zeroBiasPrelude's shared zero constant. So mobilenetv2_adam_train_step.mlir carries 158 updated parameter tensors — stem 3 + b1 6 + 16 blocks × 9 + head 3 + dense 2 — and 210 is the census at convBias := true. The bias conjuncts below are kept (one delegation each, and they cover the flag) and are about ops the committed artifacts do not emit. Nothing here weakens a theorem: every fold is ∀-quantified over op instances, and bias = 0 is one of them.

Conventions, stated because nothing here checks them #

MobileNetV2RenderB.irBackNoExpGradB, node for node, from the block-output cotangent dyOut:

%dpc = bnBatchBack(pg, pc)   %ddr = convBackBatched(pW)   %ddm = selectMidB(dn)
%ddn = bnBatchBack(dg, dc)   %dxb = depthwiseBackBatched(dW)

with dW,db ← %ddn, dg,dbt ← %ddm, pW,pb ← %dpc, pg,pbt ← %dy.

MobileNetV2RenderB.irBackStride1GradB, node for node, from the block-output cotangent dyOut:

%dpc = bnBatchBack(pg, pc)   %ddr = convBackBatched(pW)         %ddm = selectMidB(dn)
%ddn = bnBatchBack(dg, dc)   %der = depthwiseBackBatched(dW)    %dem = selectMidB(en)
%den = bnBatchBack(eg, ec)   %dxb = convBackBatched(eW)
%dx  = if skip then addVB(%dxb, %dy) else %dxb

with eW,eb ← %den, eg,ebt ← %dem, dW,db ← %ddn, dg,dbt ← %ddm, pW,pb ← %dpc, pg,pbt ← %dy. ⭐ The skip flag touches ONLY %dx, so all twelve parameter cotangents below are shared between the skip blocks and the two stage-first widenings (b11, b17).

MobileNetV2RenderB.irBackStridedGradB: the stride-1 chain with the depthwise replaced by its XLA-SAME strided peer, so the expand half runs at the 2h × 2w input grid and %der upsamples. There is no skip, so %dx is %dxb directly.

MobileNetV2RenderB, after the seventeen block backwards:

%dsm = selectMidB(stn)   %dsn = bnBatchBack(sg, stc)

with sW,sb ← %dsn and sg,sbt ← %dsm. ⭐ There is NO conv-back past %x, and no pool: the stem is one XLA-SAME strided conv, its BatchNorm and one relu6.

MobileNetV2RenderB, from the loss cotangent g:

%dgi = denseRowBack(Wd)   %dgp = gapBackBatched   %dhm = selectMidB(hn)
%dhn = bnBatchBack(hg, hc)   %dhx = convBackBatched(hW)

with Wd,bd ← %dy, hW,hb ← %dhn, hg,hbt ← %dhm, and %dhx the cotangent handed to b17. ⚠ Unlike ResNet-34's, this head is NOT batchMap of a smooth per-example map — MobileNetV2 puts a 1x1 conv-BN-relu6 in front of the pool — so the chain is spelled here as dens, exactly as EfficientNetStepTie.enetHeadTied spells B0's identically-shaped head.

Each conjunct is MobileNetV2FoldPaperG's ∀ cot fold instantiated at the cotangent the render's chain delivers, so nothing here is a new proof: the bundles are the §1 fold with the freedom removed. reassocB bridges the conv/relu6 index N·(c·h·w) to the BatchNorm parameter ops' N·(c·(h·w)).

⚠ The BIAS conjuncts are about conv{,StridedXla}BiasGradB and depthwise{,StridedXla}BiasGradB, which the committed artifacts do NOT emit — MobileNetV2RenderB runs convBias := false and binds every bias operand to zeroBiasPrelude's zero constant. They are kept because they cost one delegation each and they cover the flag.