⭐⭐ mnv4InputGradB IS the certified whole-net MobileNetV4-Conv-M gradient #
Tier T6 of planning/archive/mnv4_proofs_tier.md §Session 3 — the last tier this net can have, and
with it MobileNetV4-Conv-M is certified from its ℝ forward (T1) through its typed graph (T2), its
233-parameter train-step tie (T3) and now its whole-net input gradient. T4 and T5 are float
budgets and planning/archive/float_budget_numbers.md closed that thread by user decision on 2026-09-05.
⚠⚠ No accuracy is quoted for this net. Conv-M has no Imagenette run and no verified ImageNet
run; what pins the artifact to the reference's function is the 2026-09-07 tie pair (forward
max |Δ| = 3.770e-06, gradient 0 of 232 live parameters outside the reference's own
relu-discontinuity floor).
The four pieces #
mnv4StemBBack_eq_vjp_backwardandcbReluBBack_eq_vjp_backward— the concrete endpoint stage ties, onerwof a conv leaf tie and thenrfleach. ⚠ The stem's is the XLA-SAMEleaf (flatConvStride2XlaBack) and the head's the plain one; MobileNetV4 carries both phases.mnv4B_full_has_vjp_at— the generic twenty-six-stage apexhead ∘ hc2 ∘ hc1 ∘ b21 ∘ … ∘ b1 ∘ fused ∘ stem, twenty-fivevjp_comp_diff_ats and nothing else, withopaqueA0 … A24naming the running activations.mnv4InputGradB_eq_mnv4B_full_vjpandmnv4InputGradB_correct— the tie, and its reading as∑ pdiv … * dy: the chain IS the Jacobian-transpose of the twenty-six-stage composition, at every batch size and both shipped class counts.mobilenetv4ForwardB_full_eq_slots— the shape check: those twenty-six stages AREmobilenetv4ForwardB_full, the forwardmnv4FwdGraphB_full_faithful(T2) says the typed graph denotes. Without it the tie would be a statement about variables.
⭐⭐ What is MobileNetV4's own, and what is borrowed #
ResNet-50's T6 was four declarations because its stem and head ARE ResNet-34's. MobileNetV4's stem
is EfficientNet-B0's (3×3/s2 at the XLA-SAME phase) with ResNet-34's activation, so the leaf
ties compose rather than transfer: flatConvStride2XlaBack_eq_vjp_backward is B0's/MobileNetV2's
and the relu mask is ResNet-34's, and the stage tie that joins them is new here. The head's two
1×1 conv-BN-relu stages are cbReluB — ResNet-34's stage vocabulary at a 1×1 kernel — and its
GAP-and-dense tail is r34HeadB verbatim, exactly as T3 reused r34HeadCotBlk/r34HeadTiedB.
So what this file adds is the two stage ties, the wider apex, and the tie itself.
⚠ Twenty-six stages, not eighteen. Conv-M's ladder is 21 UIB blocks plus a fused stage, and its head has TWO convs before the pool where MobileNetV2's has one and ResNet-34's has none.
⛔⛔ The apex is composed at BLOCK granularity, not at MobileNetV4FullB.lean's groups #
mobilenetv4ForwardB_full_has_vjp_at (T1) is a chain of seven vjp_comp_ats over the five
resolution-group CertLayers, because Mnv4SmoothAt wants one .ok per group. T6 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 T2'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 — six blow-ups across
sessions 1–2 trace to that one cause. Instantiating a proven lemma is free.
⛔ The blocks stay opaque and there is no backward_unique step, for §4.2d's measured reason:
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 stays 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; the ~60 inside the blocks are CertLayer.comp's and are never written down.
⛔ What this does NOT reach. Under mnv4in_adamdp64* every gradient is all-reduced by
allReduceMeanF (DataParallelNode.lean, §4d), so this is at the per-replica gradient. And it is
about the INPUT gradient; the 233 parameter gradients are MobileNetV4StepTieB.lean's tie (T3).
The STEM tie. batchMap (flatConvStride2XlaBack) ∘ bnBack ∘ reluMaskBack IS mnv4StemB's
certified backward at a smooth point. One rw of the odd-kernel XLA-SAME strided leaf tie,
then rfl — the stage's VJP is vjp_comp_at-built so its backward is already the
composition, and a convolution's backward ignores its primal argument, so the row-wise
batchMap lift matches at every saved input.
⚠ Plain relu, XLA-SAME padding — the two axes MobileNetV4's stem does not share with a
neighbour. MobileNetV2's stem is this map with relu6 (two mask clauses); ResNet-34's is this
map with SYMMETRIC padding (cbReluStridedBBack_eq_vjp_backward); EfficientNet-B0's is this
padding with swish. One token apart from each, and a different certificate from all three.
⛔⛔ And 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 ties (T3). This lemma names the map that carries that
cotangent the rest of the way to the image — B0's choice at the identical stem.
Whole-network MobileNetV4-Conv-M VJP. The VJP of the twenty-six-stage chain
head ∘ hc2 ∘ hc1 ∘ b21 ∘ … ∘ b1 ∘ fused ∘ stem — twenty-five vjp_comp_diff_ats and
nothing else, dimension-generic and parametric in every component.
⚠ Pointwise (HasVJPAt), and necessarily: relu is kinked, so each stage's witness carries the
activation it sees. r34B_full_has_vjp_at 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 certified whole-net MobileNetV4-Conv-M gradient. 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 UIB blocks left OPAQUE, equals the
backward of mnv4B_full_has_vjp_at at those twenty-six stages. unfold, three rws, rfl.
⭐ 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 the artifacts' N is the PER-REPLICA batch
(DataParallel.lean, §4d).
⭐⭐ The chain IS the pdiv-contracted Jacobian of the twenty-six-stage net — at every
batch size, every class count, every input, every loss cotangent and every input pixel. The
tie above read through the apex's own .correct; mobilenetv4ForwardB_full_eq_slots below is
what says those twenty-six stages are the committed forward.
The head, as its two 1×1 conv-BN-relu stages and ResNet-34's GAP-and-dense tail.
The forward at GROUP granularity — rfl, because mobilenetv4ForwardB_full IS the nest of
mnv4Pre0 … mnv4Pre6. Nothing is peeled here; the seven .fwds stay folded.
The twenty-six-stage composition, APPLIED — the apex's chain read as a nested application. Generic in every dimension and every stage, so it costs nothing here.
⭐⭐ The twenty-six slots the tie is about ARE mobilenetv4ForwardB_full. The committed
forward, regrouped into exactly the twenty-six arguments mnv4B_full_has_vjp_at takes: the
XLA-SAME stem, the fused stage, the three pre-strided rows (1, 3, 11) as
mnv4PreStridedBodyOfRow, the eighteen skip rows as CertLayer.residual of mnv4BodyOfRow
at their own table rows, the head's two cbReluBs and ResNet-34's GAP-and-dense tail.
⛔ This is the theorem that would have caught ResNet-34's wrong pool (§3.10) — the tie
keeps its blocks opaque, so its subject is a chain of VARIABLES and nothing in it says which
net they are. ⭐ And it is what carries the block table into T6: every slot names its row, so
rows 4/5/10, 12/18 and 15/19/20 — shape-identical, hence interchangeable to every type and
#guard — are pinned here by the row constant, as T2's SSA names pin them in the graph.
⭐ Seven rewrites of lemmas proved above, and every one of them was proved either at group
granularity (where nothing is peeled) or between variables. Nothing in this proof discharges
a CertLayer peel at a literal resolution, which is why it takes two seconds.