MobileNetV4 — the batched UIB backward, and the four families as ONE chain #

MNv4 was the last net with no backward of any kind (planning/archive/mnv4_verified.md §8): the strongest empirical evidence in the repo — forward tied at 1.423e-06, gradient at 0/147 — and nothing in Lean beyond the render. This file is its phase 1–3, and the fold falls out with it.

⭐⭐ THE ANSWER TO §8's OPEN QUESTION: the four families COLLAPSE #

§8 asked whether MNv4's four block families — ExtraDW / IB / ConvNeXt-like / FFN — "collapse to one parameterised theorem or need a case split", and called it "the difference between a small file and a large one". They collapse, and the mechanism is CertLayer.id'.

The UIB body is preDW? → expand → postDW? → project, and k = 0 omits a depthwise. Crucially both depthwise positions are channel- and shape-preserving — preDW : ic → ic, postDW : mid → mid — so an absent one is not a different composition, it is the identity layer in the same slot:

⭐ One mnv4UibBody takes the two depthwise slots as CertLayer arguments; the caller passes id' where the table says k = 0. No case split, no four proofs — and no dispatch that could silently disagree with the forward's, which is §3's trap ("a wrong k = 0 dispatch is silent… produces a valid net that trains and descends and is not MobileNetV4").

⚠ This is exactly the §6 claim — "a family from one constructor" — landing on the proof side, the way §3i records it landing on the backward render.

What was genuinely new: a depthwise-bn-RELU stage #

Measured before building: the repo had batched depthwise stages at relu6 (dwbrB, MobileNetV2) and at swish (dwbsB, EfficientNet), and none at plain relu. MNv4 is relu throughout its 21 UIB blocks (⚠ not relu6 — MobileNetV4RenderB flags this explicitly, and mnv2 sitting one file over makes it an easy thing to get wrong).

⭐ It cost almost nothing, because bnReluStage_has_vjp_at (ResNet34BackB0) is generic in the op: it takes any differentiable op with a HasVJP and builds relu ∘ bnBatchLA ∘ batchMap op. cbReluB is that at flatConv; dwbReluB is the same lemma at depthwiseFlat. Zero new analytic content — one instantiation, plus the backward graph's .selectPos (relu's one-sided mask) where mnv2's uses .selectMid.

Scope #

⚠⚠ This paragraph was WRONG from the day it was written, and a planning row copied it. It said the fused stage, the head and the strided body assembly were not built. All three landed on 2026-08-10, the same day, in the three commits that follow the one carrying this header — e25a011 (stride-2 blocks), 61eb512 (fused stage) and 411b1a5, whose own message reads "the head — MNv4 complete at stage level". Nobody came back to the header, so for four weeks the file asserted a gap its own commit log had already closed, and proofs_tier_to_paper_nets.md §3.6 priced a session against it (planning/archive/mnv4_proofs_tier.md §0 — seventh instance of that pattern, and the cheapest: the declaration list was one grep away). ▶ When a session lands a piece, edit the header that said it was missing, in the same commit.

Built here — everything at the BLOCK and STAGE level, which is this file's whole remit: the two depthwise-relu stages (stride-1 + strided) and their backward graphs; the four stage CertLayers; the family-collapsing body and the skip block; the stride-2 form (mnv4UibPreStridedBody; Conv-M has no post-strided row); the fused stage (swish, stage 0) with stemBackBatchedGraph — the symmetric-padding strided conv-bn-swish backward that closed EfficientNet's stem hole at the same time; the head (mnv4Head, its GAP and dense layers both tying by rfl); the table-driven k = 0 dispatch; and UibParams, the row-typed weight record. Nine of these are in tests/AuditAxioms.lean, 3-axiom clean.

Not built here — the NET level, which is four other files as of 2026-09-07. T1 (the whole-net forward and its input-VJP) is Nets/MobileNet/MobileNetV4FullB.lean + MobileNetV4FullBVJP.lean, T2 (the typed forward graph at mnv4FwdChainB's tokens) is in the first of those, T3 (the tie at the emitted gradient nodes, all 233) is MobileNetV4StepTieB.lean, and T6 (the certified whole-net backward tie) is MobileNetV4WholeBackCertifiedTieB.lean + its float chain. Each of them consumes what is built here, block by block. planning/archive/mnv4_proofs_tier.md is the record; ResNet-50 — which was in exactly this position, block-level only with no per-example legacy — was the file-by-file precedent, closed over 2026-09-06/07.

⚠ Two things this file's certificates do NOT give you. (i) The head models ONE conv stage; Conv-M's render has two (%h1W 256→960, then %hW 960→1280), so a whole-net use composes cbReluLayer twice. (ii) The stem is not here and cannot be a CertLayer: no render emits a gradient into %x, so there is no convStridedXlaBackBatched token and hence no backward graph to be faithful to. That is B0's situation exactly, and a net-level forward must compose the stem's VJP by vjp_comp_at rather than by CertLayer.comp.

⚠⚠ The stride-1 collapse does not extend here, and the reason is the TYPE.

At stride 1 an absent depthwise is id' because the slot is shape-preserving. At stride 2 the depthwise that carries the stride maps (2h, 2w) ↦ (h, w) — a different type — so it cannot be replaced by an identity, and which depthwise carries it decides the resolution every later stage runs at. That is not a dispatch detail; it is two genuinely different compositions:

⭐ This mirrors the render exactly — uibFwdPreStridedB / uibFwdPostStridedB are two functions for the same reason (MobileNetV4RenderB: "a stride-polymorphic block cannot typecheck"). The proof side reproducing that split independently is a small piece of evidence that the split is real and not a renderer artifact.

⚠ All three stride-2 blocks change channels (ic ≠ oc), so none has a skip: the block IS the body, with no CertLayer.residual wrapper. Adding one would not typecheck, which is the good case.

MNv4's stage 0 is .fusedMbConv 32 48 4 3 2 1 false: a regular k×k conv (not a depthwise) doing expansion and downsampling at once, then a 1×1 project. 32 → mid = 32·4 = 128 → 48, stride 2, and ⚠ swish, not relu — a deliberate paper deviation that both emitters behind the 84.58% share (§1b).

⭐ Swish is smooth, so this whole stage is the globally-certified kind: ok = True, no smoothness side conditions, and the VJPs are global HasVJPs rather than _at. That makes stage 0 the cheapest part of MNv4's backward despite being the part §1b records as missed by the original scoping.

⭐⭐ The forward stage is fusedConvB, EfficientNet's stemB shape at SYMMETRIC padding. Until 2026-09-05 the two nets shared stemB (EfficientNetRenderPC) outright. B0's stem then moved to the XLA-SAME phase (flatConvStride2Xla, the TF-origin convention its render has shipped since 2026-08-08), while MNv4's fused 3×3/s2 stays symmetric — the reference's fused_ib passes an explicit (p,p) tuple and scripts/convention_audit.py reads the render at sym there — so the stage gets its own name with the same bnSwishStage_* lemmas. What was missing repo-wide was the backward graph: stemBackBatchedGraph below, at the symmetric convStridedBackBatched. ⚠ It serves MNv4's fused stage only; B0's XLA stem has no batched input-VJP token (no render emits a gradient into the image), so B0's stem stays un-graph-certified — recorded in planning/archive/proofs_tier_to_paper_nets.md.

MNv4's head is 1×1 conv (256 → 1280) → BN → relu → GAP(7×7) → dense. The conv stage is cbReluLayer again (conv-bn-relu is conv-bn-relu, and the kernel extent is a binder), so only GAP and the classifier are new.

⭐ Both tie by rfl. den of .gapBackBatched is definitionally the row-wise GAP VJP, and den of .denseRowBack is rowDenseBackFlat — which is what batchMap_has_vjp reduces to. The batchMap_has_vjp route goes through a transported equality (batchMap_eq_rowwiseFlat ▸ …), so this was worth probing rather than assuming; it discharges definitionally.

⚠ GAP's VJP is input-independent and den .gapBackBatched exploits that — it evaluates the backward at the point fun _ => 0. That is sound because GAP is linear, and it is why the tie holds for any x. A stage whose VJP did depend on its input could not be rendered this way.

⛔ What this section fixes. Above, mnv4UibBody takes its depthwise slots as arguments, so passing id' where block 4's real pre-DW belongs is well-typed and still certified — graph and VJP both move with the caller's arguments, so the theorem stays true about the wrong net. Types catch the stride split (resolution is in the type); they catch nothing about k = 0 vs k > 0, because that slot is shape-preserving — the very property that made the collapse possible. That is §3's trap, one level up from the render.

⭐ The fix is to make the slot a function of the block table's k, so the proof side runs the same k = 0 dispatch the render does, off the same mnv4Blocks list — one table, not two readings. mnv4-fwd-smoke already pins the render against that table; these #guards pin the table's own shape, so a bad edit fails at lake env lean rather than becoming a silent net.

⛔ The gap this closes. A block builder that reads the dispatch from the table but takes its weights as separate arguments lets a caller pair row 4's ks with row 7's widths. The dispatch was table-driven; the wiring was not.

⭐ Fix: index the parameter record by the row. Every width in UibParams s is a projection of s — s.ic, s.oc, s.ic * s.expand, s.preDWk, s.postDWk. A record with widths that disagree with its row cannot be constructed, so the block builder needs no side conditions and no #guard: it is impossible by typing rather than checked after the fact.

⚠ What this still does not pin, stated precisely so the next reader does not overclaim: rows 4, 5 and 10 are all 160 → 160, expand 4, and 4/10 share k = 3,3. Their records are therefore the same type, so swapping those two blocks' weights typechecks. Typing pins shape (channels, expand ratio, kernel extents, resolution); it cannot pin identity between rows that are shape-identical. Closing that needs the weights to come from one indexed array — a renderer concern, since the render already folds mnv4Blocks in order.