mnv4InputGradB and the certified whole-net MobileNetV4-Conv-M input VJP #
Ties the batched input-gradient chain mnv4InputGradB to a certified VJP for
mobilenetv4ForwardBFull: the MobileNetV4 peer of MobileNetV2WholeBackCertifiedTieB.lean.
No accuracy is quoted for this net. The statements are about timm's mobilenetv4_conv_medium.
The four pieces #
- The concrete endpoint stage ties: the stem's (ResNet's symmetric strided conv-bn-relu tie),
the first head conv's (
cbReluBBack_eq_vjp_backward),conv_head's with the pool in front of it (mnv4Hc2BBack_eq_vjp_backward), and the classifier's with its relabel (mnv4ClsBBack_eq_vjp_backward). mnv4BFullHasVJPAt— the generic twenty-six-stage apexcls ∘ hc2 ∘ hc1 ∘ b21 ∘ … ∘ b1 ∘ fused ∘ stem, twenty-fivevjpCompDiffAts and nothing else, withopaqueA0 … A24naming the running activations. timm's head is three stages here:hc1(conv-bn-relu at 7×7),hc2(GAP, relabel to[N, 960, 1, 1],conv_head-bn-relu) andcls(relabel to[N, 1280], dense).mnv4InputGradB_eq_mnv4B_full_vjpandmnv4InputGradB_correct— the tie, and its reading as∑ pdiv … * dy: with its fused-stage and block slots filled by certified VJPs, the chain is the Jacobian-transpose of the twenty-six-stage composition, at every batch size and class count.mobilenetv4ForwardBFull_eq_slots— the shape check: those twenty-six stages AREmobilenetv4ForwardBFull, the forwardmnv4FwdGraphBFull_faithfulsays the typed graph denotes. Without it the tie would be a statement about variables.
What is MobileNetV4's own, and what is borrowed #
The stem is ResNet's symmetric strided conv-bn-relu, so its tie is ResNet's; the first head conv is
cbReluB. What is MobileNetV4's own is the pool stage in front of conv_head (GAP then a
Fin.cast relabel, whose certified backward along a bijection is the plain relabel,
reindex_cast_backward) and the relabel in front of the classifier.
The apex is composed at block granularity, not at MobileNetV4FullB.lean's groups #
mobilenetv4ForwardBFullHasVJPAt is a chain of seven vjpCompAts over the five
resolution-group CertLayers, because Mnv4SmoothAt wants one .ok per group. This tie wants
the finer chain — a tie whose opaque slots are groups would say nothing about which block is which —
so the stages here are the twenty-one blocks themselves, mnv4Blk0 … mnv4Blk21's
(MobileNetV4StepTieB.lean) stage functions. Peeling CertLayer.comp to reach .fwd inside a
group is cheap (comp_fwd is a generic rfl lemma and MobileNetV4FullB's five
group-faithfulness proofs each do it); what is not payable at MobileNetV4's literal resolutions is composing the compositions,
which is why there is no mnv4NetLayer and why the shape check below stops at the block.
Everything generic in its widths, instantiated only in the capstone. Both stage ties bind
{N ic oc h w kH kW} and the apex binds {s0 … s26}; MobileNetV4's 224/112/56/28/14/7 are
literals, and stating a den- or width-indexed rfl at them lets it run into kernel timeouts.
Instantiating a proven lemma is cheap.
The blocks stay opaque and there is no backward_unique step, because instantiating a tie of this shape at the concrete blocks is a KERNEL deterministic timeout when
the witnesses are HasVJPAt carrying a saved activation. B0 takes that step only because swish
has no kink. The shape check is what replaces it.
It is a smooth-point statement, and MobileNetV4's kink budget is relu, not relu6: one
clause per site, where MobileNetV2's .selectMid carries two. The stem's and the two head convs'
are bound here (conv_head's at the pooled 1×1); the ones inside the fused stage and the blocks
are CertLayer.comp's and are never written down.
The train step reads the same backwards. The cotangent MobileNetV4StepTieB.mnv4_net_tiedB
hands each block's parameter nodes is that block's certified VJP backward, one block at a time
(mnv4HeadCotIn_eq_vjp, mnv4BodyCotIn_eq_vjp with mnv4SkipCotIn_eq_vjp,
mnv4SBodyCotIn_eq_vjp, mnv4FusedCotIn_eq_vjp), wherever that block is certified. This file
composes the same layers into the whole-net input gradient.
Scope. One device's batch N: the data-parallel artifacts (mnv4in_adamdp64*) normalise
over the global batch, so this describes them only at N := R·N. It is about the input gradient;
the 233 parameter gradients are MobileNetV4StepTieB.lean's tie.
The STEM tie. batchMap (flatConvStride2Back) ∘ bnBack ∘ reluMaskBack IS mnv4StemB's
certified backward at a smooth point — the symmetric strided conv-bn-relu tie, since
mnv4StemB is cbReluStridedB at the stem's widths.
This is one step past the artifact. No render emits a gradient into %x, so
MobileNetV4's committed backward ends at the stem conv's weight gradient, whose operand is the
stem-BN cotangent mnv4StemCotN (MobileNetV4StepTieB). This lemma names the map that carries that
cotangent the rest of the way to the image.
The pool stage in front of conv_head: GAP, then the relabel to [N, c, 1, 1].
Equations
- Proofs.mnv4PoolB N h w = ⇑(Proofs.reindexCLM (Fin.cast ⋯)) ∘ Proofs.StableHLO.batchMap N (Proofs.globalAvgPoolFlat c h w)
Instances For
conv_head's stage: the pool, then conv-bn-relu at 1×1, with its VJP at a point where
that relu is away from its kink.
Equations
- One or more equations did not get rendered due to their size.
Instances For
conv_head's stage tie: GAP-back after the relabel, after conv-back ∘ BN-back ∘ relu mask
at 1×1, IS the stage's certified backward.
The classifier stage: the relabel of [N, oc, 1, 1] to [N, oc], then dense.
Equations
- Proofs.mnv4ClsB N Wd bd = Proofs.StableHLO.batchMap N (Proofs.dense Wd bd) ∘ ⇑(Proofs.reindexCLM (Fin.cast ⋯))
Instances For
Whole-network MobileNetV4-Conv-M VJP. The VJP of the twenty-six-stage chain
head ∘ hc2 ∘ hc1 ∘ b21 ∘ … ∘ b1 ∘ fused ∘ stem — twenty-five vjpCompDiffAts and
nothing else, dimension-generic and parametric in every component.
Pointwise (HasVJPAt): relu is kinked, so each stage's witness carries the
activation it sees. r34BFullHasVJPAt is the same construction at eighteen stages;
MobileNetV4 needs its own because Conv-M's ladder is longer, not because anything differs.
Equations
- One or more equations did not get rendered due to their size.
Instances For
mnv4InputGradB is the backward of the whole-net VJP at opaque blocks. The committed
backward chain, with its three BatchNorm and three relu-mask slots filled by the certified
per-op backwards and its fused-stage and twenty-one block slots filled by the supplied
witnesses' backwards (hfused, hb1 … hb21; the stages themselves left opaque), equals the
backward of mnv4BFullHasVJPAt at those twenty-six stages, at an input where the stem and
both head relu clauses (h_stem, h_h1, h_h2) hold.
N, nCls and the final side f are binders, so this covers the 10-class Imagenette
artifacts and the 1000-class mnv4in ones at every batch size, and — since 2026-10-12 — the
paper tier's mnv4in256 renders at f := 8 beside the 224 ones at f := 7 (the stages'
sides are 16f, 8f, 4f, 2f, f, the input 2·16f; MobileNetBackChains.mnv4InputGradB).
The stage ties this rewrites with were generic in h w all along, and the apex over opaque
stages binds its widths, so the side costs nothing here; mobilenetv4ForwardBFull_eq_slots,
which identifies the stages with the literal-resolution forward of MobileNetV4FullB, stays
at 224 (that file's note on resolution literals). On the data-parallel (sync-BN) artifacts,
instantiate at the global batch R·N (see MobileNetV4SyncB).
The chain is the pdiv-contracted Jacobian of the twenty-six-stage composition — at
every batch size, class count and loss cotangent, and at every input where the stem and both
head relu clauses hold (h_stem, h_h1, h_h2): the chain, with its fused-stage and
twenty-one block slots filled by the supplied certified VJPs at the running activations
(hfused, hb1 … hb21), is the Jacobian-transpose of the composition of those stages. The
stages are variables here; mobilenetv4ForwardBFull_eq_slots identifies them with the
committed forward.
The twenty-six slots the tie is about are mobilenetv4ForwardBFull. The committed
forward, regrouped into exactly the twenty-six arguments mnv4BFullHasVJPAt takes: the
symmetric stem, the fused stage, the three strided rows (1, 3, 11) as mnv4StridedBodyOfRow,
the eighteen skip rows as CertLayer.residual of mnv4BodyOfRow at their own table rows, and
the head's three stages (cn_960, the pool with conv_head, the relabelled classifier).
The tie keeps its blocks opaque, so its subject is a chain of variables and nothing in it
says which net they are; this theorem does. It also carries the block table into the tie:
every slot names its row, so rows 4/5/7, 8/10, 12/18, 13/14 and 15/19/20 — shape-identical,
hence interchangeable to every type and #guard — are pinned here by the row constant, as
mnv4FwdGraphBFull's SSA names pin them in the graph.