MobileNetV4-Conv-M at TRUE BATCH-NORM — the whole net's forward and graph (T1-forward, T2) #

MobileNetV4 was the last net in planning/archive/proofs_tier_to_paper_nets.md §2's table with nothing at the net level. MobileNetV4BackB0.lean is complete at the BLOCK and STAGE level — every UIB family, both stride-2 forms, the fused stage, the head, the table-driven k = 0 dispatch and the row-typed UibParams — and this file is the tier above: a net-level ℝ forward at the 21-row Conv-M table, and the typed StableHLO graph over it at mnv4FwdChainB's own tokens. planning/archive/mnv4_proofs_tier.md is the plan; ResNet-50 closed the same two tiers on 2026-09-06 and ResNet50FullB.lean is the file this one mirrors.

⚠⚠ NO ACCURACY IS QUOTED FOR THIS NET. Conv-M has no Imagenette run and no verified ImageNet run; historical/RESULTS.md's 84.58% belongs to the SUPERSEDED Conv-S table. What the artifacts under this tier are pinned to is the reference's function: the forward tie measures max |Δ| = 3.770e-06 against jax/.lake/build/generated_mobilenet_v4.py on shared weights and the gradient tie puts 0 of 232 live parameters outside the reference's own fp32 noise floor (both re-run at the Conv-M table on 2026-09-07, planning/archive/mnv4_convm_ties_todo.md). That is what makes the tiers below statements about MobileNetV4 rather than about a net.

⭐⭐ The trunk is FIVE CertLayer groups — and the reason it is not ONE is the finding here #

ResNet-50's T1 needed sixteen r50Pre_k prefix definitions and a hand-written bottom-up have chain for its apex, because its CertLayer trunk predated the tie files' needs. MNv4 has no such legacy, so each resolution group — the fused stage, rows 1–2, 3–6, 7–10, 11–15, 16–21, the head — is assembled with CertLayer.comp and CertLayer.residual directly, and inside a group:

• .fwd is that group's forward — no second definition to keep in step;
• .ok is its smoothness hypothesis, conjoined at exactly the right activations by comp rather than written out (~60 relu clauses across the net, none of them written here);
• .vjp is its HasVJPAt (MobileNetV4FullBVJP.lean chains seven of them); and
• .faithful is its BACKWARD-graph faithfulness, for free.

⛔⛔ But composing the groups into ONE CertLayer does not work, and this cost a day to establish, so it is recorded rather than re-discovered. fused.comp (res28.comp (… .comp head)) elaborates fine and reads beautifully. Every later statement then has to peel CertLayer.comp to reach .fwd, and at MNv4's LITERAL resolutions that peel is fatal: (L₁.comp L₂).fwd = L₂.fwd ∘ L₁.fwd is rfl, and discharging it at these instances — by rfl, by simp only [CertLayer.comp_fwd], inside the T2 capstone or in a standalone lemma — costs ten minutes of elaboration and then a (kernel) deterministic timeout. Every one of those four spellings was measured. ⚠ The groups' own five-stage comp chains are completely fine; it is composing the compositions, under something that can start unfolding den, that is not.

⭐ So the top level is seven named prefixes (mnv4Pre0 … mnv4Pre6) and the forward is their nest. What it costs is the hypothesis bundle: Mnv4SmoothAt binds one .ok per group, eight fields rather than two. What it keeps is everything that mattered — R50's apex binds 33, and MNv4 binds no 0 < ε hypothesis at all, because those live inside the weight records.

▶ The general lesson, and it is not MNv4-specific: a net whose resolutions are LITERALS cannot afford the proof idioms a net with a resolution BINDER can. ResNet-50's q keeps den stuck; MNv4's 224/112/56/28/14/7 let it run. Three separate blow-ups in this file trace to exactly that — this one, the graph builders that had to be made generic in their widths, and the whole-net capstone that had to become rw instead of simp only.

⚠⚠ The stem sits OUTSIDE the chain, and this is EfficientNet-B0's situation exactly. CertLayer demands a backward graph, and no render emits a gradient into %x — there is no convStridedXlaBackBatched token, because the artifact's backward ends at the stem conv's WEIGHT gradient. B0's stem sits outside its chain for the same reason. So mnv4StemB is a plain function here, its VJP is bnReluStage_has_vjp_at at flatConvStride2Xla, and the net-level VJP composes the two with vjp_comp_at.

Conventions this net runs at #

⚠ N stays a binder throughout, as at r34/R50: this tier carries no batch numeral. On the data-parallel artifacts the render's N is the PER-REPLICA batch; since 2026-09-21 their BatchNorm is synchronised, and MobileNetV4SyncB.lean is this file's twin for them: replica r's forward graph denotes shard r of mobilenetv4ForwardB_full (R * N), this file's forward at the global batch. Unlike R50 there is no q binder — MNv4 ships one resolution.

⚠ Rows 4/5/10, 12/18 and 15/19/20 are shape-identical, so their UibParams records have the same TYPE and swapping their weights typechecks. Typing pins shape, not identity; what pins identity is the SSA NAMES the T2 graph writes (%u4qW vs %u10qW), which is why the graph reads its names from s.p off the table rather than taking them as arguments.

✅ Checked against the committed bytes: verified_mlir/mnv4_fwd.mlir's signature is 234 arguments = %x + 233 parameters, and every name this file writes appears there.

⚠ These are abbrevs, and the rows are NAMED rather than indexed. UibParams (mnv4Blocks[3]!) in a type would force whnf through List.get! at every use; a named reducible constant reduces to its projections directly, which is what lets CertLayer.comp line up 2 * 28 with 56 across a stride join without a single transport.

⭐ The #guard below is the whole safety of that move: these 21 constants are pinned to mnv4Blocks — the ONE table mnv4FwdChainB, the backward, the parameter signature and the BN stat list all fold over — so a typo here is a build failure rather than a proof about a different net.

⚠⚠ The trunk is built in GROUPS, and that is a proof-engineering requirement. One 24-stage CertLayer elaborates fine — it is the T2 faithfulness proof over it that does not: the whole-net rewrite chain produces a term whose KERNEL check exceeds any reasonable budget (measured: the elaboration succeeds after ~9 minutes and the kernel then reports a deterministic timeout). Split at the net's own resolution boundaries, each group's proof is small, and the whole-net theorem is six rewrites over them. ⭐ The grouping is the ladder a reader already knows — 56, 28, 14, 7 — so it costs nothing in readability and buys a bounded proof.

⛔⛔ The seven groups are composed by a PREFIX CHAIN, not by one more CertLayer.comp, and this is the single hardest thing this file learned.

A mnv4NetLayer := fused.comp (res28.comp (… .comp head)) elaborates fine and reads beautifully. But every downstream statement then has to peel CertLayer.comp to get at .fwd, and at MNv4's LITERAL resolutions that peel is fatal: (L₁.comp L₂).fwd = L₂.fwd ∘ L₁.fwd is rfl, yet discharging it at these instances — by rfl, by simp only [CertLayer.comp_fwd], inside the T2 capstone or in a standalone lemma — costs ten minutes of elaboration and then a (kernel) deterministic timeout. ⚠ The groups' OWN five-stage comp chains are fine; it is composing the compositions, under something that can start unfolding, that is not.

⭐ So the top level is seven named prefixes and the forward is their nest — ResNet-50's shape at seven stages instead of eighteen. What that costs is the hypothesis bundle: Mnv4SmoothAt binds one .ok per group (seven) rather than one for the whole trunk. What it keeps is everything that mattered — each group's .ok is still the conjunction CertLayer.comp assembled from its blocks' conditions at their own activations, so ~60 relu clauses are still never written down, and no 0 < ε hypothesis appears at all. R50's apex binds 33.