T3 §1 fold for MobileNetV2 at 17 blocks, UN-FUSED and BATCHED — the Adam artifact's op set #

This file makes every parameter gradient node of MobileNetV2's batched train steps den-faithful — every train step the net ships, since 4c leg 2 retired the per-example SGD-inline renderer and its artifact on 2026-09-06.

⛔ MobileNetV2's two renders did not overlap the way the other four nets' do. ConvNeXt, ViT and EfficientNet each render one traversal with two endings under an adam : Bool. MobileNetV2 did not: MobileNetV2Render.lean was SGD-inline only (no adam flag anywhere in it) and MobileNetV2RenderB is AdamW/RMSProp-only, at the batched index and at batch BatchNorm. So mobilenetv2_adam_train_step, mobilenetv2_rms_train_step, mobilenetv2_adamdp_train_step and every ImageNet artifact — including mobilenetv2in_rmsdp64, whose accuracy the book quotes — are on a chain that has no fused op to un-fuse: they emit *GradB from the start. This file is therefore at the BATCHED gradient nodes, which is the "or" branch section 4b.4 allowed and, since these are the artifacts, the right one. ⭐ It was also a down-payment on 4c, and it paid: the op table below is the one the converged render kept.

⭐ One lemma per op kind certifies every optimizer tail at once — AdamW, RMSProp and the data-parallel twins all consume the same node. ⚠ The bf16 twins do NOT: they emit *GradBBf16, folded in Foundation/Bf16GradNodes.lean.

⭐ Eight of the twelve kinds were already proven, and none of them here #

ResNet34FoldB.lean and EfficientNetFoldG.lean state their folds at op kinds, not at their nets, and between them they already cover convWeightGradB, convBiasGradB, bnGammaGradB, bnBetaGradB, denseWeightGradB, denseBiasGradB, convStridedXlaWeightGradB and depthwiseWeightGradB — every one at the generality MobileNetV2 needs. The four genuinely new ones are all XLA-SAME-or-depthwise BIAS shapes that no other net emits: convStridedXlaBiasGradB, depthwiseBiasGradB, depthwiseStridedXlaWeightGradB, depthwiseStridedXlaBiasGradB.

⚠ The shipped parameter count is 158, not 210. 210 is the census at convBias := true; MobileNetV2RenderB defaults to convBias := false — the conv, depthwise and project biases are folded into the BatchNorm that follows each of them — and the parameter half of mobilenetv2_adam_train_step.mlir returns exactly 158 updated tensors: stem 3 + b1 6 + 16 blocks × 9 + head 3 + dense 2.

The op table of mobilenetv2_adam_train_step.mlir #

and the four bias kinds the render emits at convBias := true, which no committed artifact contains but which the flag can turn on: convBiasGradB (ResNet34PoCB.convBGradB_den), convStridedXlaBiasGradB, depthwiseBiasGradB, depthwiseStridedXlaBiasGradB (the three ⭐ new ones below).

⚠ XLA-SAME padding at all five stride-2 sites — the stem and the four stride-2 depthwises. These are the convStridedXla* / depthwiseStridedXla* ops, not r34's symmetric peers; the two families have identical types and identical emitted shapes, so only the certificate distinguishes them, and MobileNetV2 is the TF-origin net.

Honest residual #

• Every lemma is ∀ cot: each holds at the actual backward-chain cotangent without naming it. Pinning them is the §1a tie, and it landed 2026-09-06 as Nets/MobileNet/MobileNetV2StepTieB.lean (§4.2c). The per-example tie (MobileNetV2TiePoCPaper.lean, deleted 2026-09-08) was at the fused ops and at per-example BatchNorm, so nothing transferred.
• ⚠ The forward these nodes differentiate is batch BatchNorm (bnBatchLA), which every MobileNetV2 statement in Proofs/ was NOT when this file was written. MobileNetV2FullB.lean and MobileNetV2FullBVJP.lean (§4.2b) closed that the same day. Either way a den = certified gradient fold is about one op and its free cotangent, and says nothing about which whole-net forward produced that cotangent.
• mobilenetv2in_*dp* is four replicas: the all-reduce is emitted text outside the AST, so these lemmas are about the per-replica gradient node.