MobileNetV4-Conv-M's whole-net input-VJP at batch BatchNorm #
MobileNetV4FullB.lean states the batch-BN forward at the 21-row Conv-M table and gives it a
typed graph. This file gives that forward a certified HasVJPAt
(mobilenetv4ForwardBFullHasVJPAt).
No accuracy is quoted for this net. The statements are about timm's mobilenetv4_conv_medium;
the artifacts are pinned to it by scripts/parity/mnv4_timm_parity.py,
scripts/parity/mnv4_forward_tie.py and scripts/parity/grad_tie.py --net mnv4.
Eight fields, not thirty-five #
ResNet-50's apex (resnet50ForwardBFullHasVJPAt) takes two structures, R50PosB and
R50SmoothAtB, whose 35 hand-written fields are a positivity bundle and a smoothness bundle per
block plus the stem's and the pool's, each smoothness field stated at its own hand-written
r50Pre_k prefix. MobileNetV4's smoothness hypothesis has eight fields — one per prefix — and the
difference is CertLayer:
0 < εat all 77 BatchNorm sites is already INSIDE the weights —UibParamscarrieshq he hd hzandMnv4BWeightscarries the stem's, the fused stage's and the head's — so no positivity hypothesis appears here at all, whereR50PosBhas seventeen fields.- every relu clause is some group's
.ok, whichCertLayer.compbuilt by conjoining each stage's condition at that stage's own input as the group was assembled. Writing them out would be 38 clauses (the relu countMobileNetV4FullBSeal's#guardchecks), each at a deeply nested activation. None is written down here.
It would be seven fewer still if the whole trunk were one CertLayer — and it cannot be. That
composition elaborates, but every later use has to peel CertLayer.comp to reach .fwd, and at
MNv4's literal resolutions that peel ends in a kernel timeout (MobileNetV4FullB.lean); the
seven prefixes are the price, and they are ResNet-50's own shape at seven stages rather than
eighteen.
The stem is the only thing composed by hand, and it has to be #
CertLayer demands a backward graph and no render emits a gradient into %x: the
artifact's backward ends at the stem conv's WEIGHT gradient. That is EfficientNet-B0's situation
exactly, so MNv4's stem stays a plain function and the apex is one vjpCompAt.
No new Foundation lemma is needed. The stem is the symmetric strided conv-bn-relu
(cbReluStridedB), so its VJP is cbReluStridedBHasVJPAt — itself bnReluStageHasVJPAt at
flatConvStride2.
Pointwise (HasVJPAt), not global: relu is kinked, at every stage including stage 0 (timm's
EdgeResidual is relu).
N is a binder, so this covers every batch size. On the data-parallel (sync-BN) artifacts,
instantiate at the global batch R·N (see MobileNetV4SyncB).
The stem's single relu site is away from the kink at x. One clause: MNv4's stem is
conv-bn-relu, where MobileNetV2's is relu6 and carries two.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The stem's VJP: cbReluStridedBHasVJPAt, the symmetric strided conv-bn-relu — zero new
analytic content.
Equations
- Proofs.StableHLO.mnv4StemBHasVJPAt N h w Ws bs εs hεs γs βs x hs = Proofs.StableHLO.cbReluStridedBHasVJPAt N Ws bs εs hεs γs βs x hs
Instances For
Everything MobileNetV4-Conv-M's whole-net VJP needs: the stem's one kink clause, and
each group's .ok at the activation that group actually sees.
Each group field is a conjunction CertLayer.comp assembled from its blocks' conditions —
each relu's condition stated at the activation THAT stage sees, in execution order. The
eighteen skips contribute their bodies' conditions unchanged (an identity skip adds no kink),
and the BN-only pre-DWs, the projects, GAP, the head casts and dense contribute nothing. 38
relu clauses in total (the stem's plus 37 across the seven .ok fields), none of which had
to be written down.
the stem's relu is away from its kink at the image.
- fused : (mnv4FusedStack N w).ok (mnv4Pre0 N w x)
the fused stage's relu at the stem's output (its project contributes
True). - g28 : (mnv4Res28Layer N w).ok (mnv4Pre1 N w x)
rows 1–2 at 56×56.
- g14a : (mnv4Res14aLayer N w).ok (mnv4Pre2 N w x)
rows 3–6 at 28×28.
- g14b : (mnv4Res14bLayer N w).ok (mnv4Pre3 N w x)
rows 7–10 at 14×14.
- g7a : (mnv4Res7aLayer N w).ok (mnv4Pre4 N w x)
rows 11–15 at 14×14.
- g7b : (mnv4Res7bLayer N w).ok (mnv4Pre5 N w x)
rows 16–21 at 7×7.
- head : (mnv4HeadStack N w).ok (mnv4Pre6 N w x)
the head's two relus at the trunk's output.
Instances For
MobileNetV4-Conv-M at batch BatchNorm has a certified input-VJP at a smooth point — the fused stage, all 21 UIB blocks and the two-conv head.
A bottom-up chain of seven vjpCompDiffAts: the stem, the fused stage, the five resolution
groups, the head. Every step below the stem is a group's .vjp — CertLayer.comp's
composition theorem already applied within it, which is CertifiedChain.lean's whole reason
for existing; only the seven joins are made here.
Pointwise, because relu is kinked (hx : Mnv4SmoothAt N w x). N and nCls are both binders, so this
covers the 10-class Imagenette artifacts and the 1000-class mnv4in ones at every batch size,
and no 0 < ε hypothesis appears — those live in the weight records.
Equations
- Proofs.StableHLO.mobilenetv4ForwardBFullHasVJPAt N w x hx = (Proofs.StableHLO.mnv4ChainB✝ N w x hx).fst
Instances For
The committed forward is differentiable at every smooth point — the chain's .snd. What the
seal's seal_differentiableAt needs.
The .correct field of mobilenetv4ForwardBFullHasVJPAt, restated: at a point satisfying
Mnv4SmoothAt, its backward is the pdiv-contracted Jacobian of mobilenetv4ForwardBFull,
at every batch size and class count.