mnv2InputGradB and the certified whole-net MobileNetV2 input VJP at batch BatchNorm #
Ties the batched input-gradient chain mnv2InputGradB to a certified VJP for
mobilenetv2ForwardBFull, the [t,c,n,s] ladder at bnBatchLA, at a variable batch N: the
MobileNetV2 peer of ResNet34BackCertifiedTieB.lean.
One apex, every stage opaque #
mobilenetv2PaperPCHasVJPAt (below) is a twenty-one-stage chain generic in every dimension and in every stage, so the batched
net instantiates it directly: stem at mnv2StemB, the seventeen bottlenecks at the batched
block maps, and the head's three stages at cbrB / batchMap gap / batchMap dense.
opaqueA0 … A17 are OpaquePrefix.lean's. So this file defines no prefix defs —
where ResNet-34's peer had to, because its committed apex bundles the stem's pool into stem and
its head into one stage.
The three pieces #
mnv2StemBBack_eq_vjp_backwardandcbrBBack_eq_vjp_backward— the two concrete conv-BN-relu6 endpoints, onerwof a conv leaf tie and thenrfleach. The stem's is the XLA-SAMEleaf (flatConvStride2XlaBack) and the head's the plain one; that is the one convention this net and ResNet-34 do not share.mnv2InputGradB_eq_mobilenetv2B_full_vjpandmnv2InputGradB_correct— the tie, and its reading as∑ pdiv … * dy: with its seventeen block slots filled by certified block VJPs, the chain is the Jacobian-transpose of the twenty-one-stage composition, at every batch size.mobilenetv2ForwardBFull_eq_slots— the shape check: those twenty-one stages AREmobilenetv2ForwardBFull, the forwardmobilenetv2FwdGraphBFull_faithfulsays the typed graph denotes. Without it the tie would be a statement about variables.
Why the blocks stay opaque. Instantiating a tie of this shape
at the concrete blocks is a kernel deterministic timeout: the block witnesses are HasVJPAt at
opaqueA{k-1} … x and a caller's are at mnv2PreB{k-1} N w x, which is seventeen defeq
checks between seventeen-deep nested applications spelled through different definition chains.
B0's file takes that step only because swish has no kink, so its witnesses are GLOBAL HasVJP
and carry no point at all. The shape check is what replaces it.
It is a smooth-point statement: relu6 is kinked on both sides, so each of the 35 sites carries
≠ 0 ∧ ≠ 6. MobileNetV2's two clauses per block are the expand relu6 and the depthwise relu6,
both inside the body — not ResNet-34's mid-relu and post-residual outer relu. Those are
MobileNetV2FullBVJP's bundles; this file adds no hypothesis of its own.
Scope. One device's batch N: the data-parallel artifacts normalise over the global batch, so
this describes them only at N := R·N. It is about the input gradient; the parameter gradients
are MobileNetV2StepTieB.lean's tie.
The whole-network MobileNetV2 VJP at opaque stages. dns ∘ gap ∘ head ∘ b17 ∘ … ∘ b1 ∘ stem. Twenty vjpCompDiffAts and nothing else:
MobileNetV2's skips live INSIDE the block maps and its strides inside the strided bodies, so
there is no list of blocks and no separate downsample slot at any depth. Dimension-generic
and parametric in every component.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The STEM tie. batchMap (flatConvStride2XlaBack) ∘ bnBack ∘ reluMaskBack is mnv2StemB'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 vjpCompAt-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.
The HEAD's conv-BN-relu6 tie. batchMap (convFlatBack) ∘ bnBack ∘ reluMaskBack IS
cbrB's certified backward at a smooth point — the stride-1 peer of the stem's, at the plain
(non-XLA) convolution leaf. MobileNetV2's head is not hypothesis-free, unlike ResNet-34's:
it puts this relu6 in front of the pool, so the net's 35th kink site is here.
mnv2InputGradB is the backward of the whole-net VJP at opaque blocks. The committed
backward chain, with its two BatchNorm and two relu6-mask slots filled by the certified per-op
backwards and its seventeen block slots filled by the supplied block witnesses' backwards
(hb1 … hb17, blocks b1 … b17 left opaque), equals the backward of
mobilenetv2PaperPCHasVJPAt at those twenty-one stages, at an input where the stem and head
relu6 clauses (h_stem, h_head) hold.
The batched chain is the pdiv-contracted Jacobian of the twenty-one-stage composition —
at every batch size and loss cotangent, and at every input where the stem and head relu6
clauses hold (h_stem, h_head): the chain, with its seventeen block slots filled by the
supplied certified block VJPs at the running activations (hb1 … hb17), is the
Jacobian-transpose of dense ∘ gap ∘ cbrB ∘ b17 ∘ … ∘ b1 ∘ mnv2StemB. The blocks are
variables here; mobilenetv2ForwardBFull_eq_slots identifies the stages with the committed
forward.
The shape check — the twenty-one slots the tie is about are the committed forward.
mobilenetv2ForwardBFull, regrouped into exactly the twenty-one arguments
mobilenetv2PaperPCHasVJPAt takes: the XLA-SAME stem, b1 the t = 1 bottleneck,
b3/b5/b6/b8/b9/b10/b12/b13/b15/b16 the bodies under the identity skip, b2/b4/b7/b14 the
stride-2 downsamplers, b11/b17 the stride-1 bodies whose channels change, and the head's
three stages.
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 goes through mobilenetv2ForwardBFull_eq_chain
for the depth-17 half and then unfolds the named prefixes and the head.