MobileNetV2's non-degeneracy seal, on the full-width batched net (levels 2 and 3) #

MobileNetV2FullBVJP.lean proves mobilenetv2ForwardBFullHasVJPAt: the whole-net VJP at any (w, x) satisfying 19 clause bundles — the stem's relu6, one per bottleneck, and the head's — covering 35 relu6 sites, each a two-sided window ≠ 0 ∧ ≠ 6. A conditional theorem of that shape says nothing unless its hypotheses are jointly satisfiable at a point with a nonzero Jacobian. This file exhibits such a point on mobilenetv2ForwardBFull itself: the seventeen bottlenecks of the [t,c,n,s] table, 32→1280 channels, XLA-SAME stride-2 padding, batch BatchNorm, at 224×224.

The witness #

Weights are structural, not trained:

• ε = 1 and γ = 1/64 at all 52 BatchNorms; β = 3 wherever a relu6 follows, β = 0 at the seventeen linear-bottleneck projections, which no activation follows;
• the ten residual bottlenecks have all three kernels zeroed. A zero kernel gives a constant channel, batch BN of a constant channel is β, and the block's last β is 0 — so a residual block is the exact identity (sealResB_eq), simpler than ResNet's a ↦ a + 1;
• the seven channel-changing blocks (b1, b2, b4, b7, b11, b14, b17), the stem and the head carry the signal: every 1×1 expand and project is a centre-tap broadcast (BatchSeal.ctK), every 3×3 depthwise a centre-tap identity (BatchSeal.ctDW);
• the head reads channel 0 into class 0, so 0 < nCls is the only constraint on the class count.

N = 2, and the input is the shared ray sealX t = rayX … t.

Every one of the 35 clauses is weight-only #

Better than ResNet-34, whose post-residual relu still needed 0 ≤ activation. Two facts compose: every relu6 in this net sits directly on a BatchNorm output, and BatchSeal.bnBatchLA_window bounds a BN output inside (0, 6) at every input once |γ|·√(N·h·w) < β = 3; and the linear bottleneck has no relu after the residual add, so there is no post-residual clause at all. The margin holds at every site because the widest is 2·112² = 25 088 and √25 088 / 64 < 2.48 (BatchSeal.margin192). Consequence: no nonnegativity layer, no positional injectivity, and — with no max-pool anywhere in this net — no no-tie argument.

The carrier threads twenty-two BatchNorms #

MobileNetV2's channel-changing blocks have no skip — the body is the block — so unlike ResNet's carrier, which saw only the projection of each downsample, this one crosses every BN inside them: 1 (stem) + 2 (b1) + 3 × 6 + 1 (head). The ten residual blocks pass it through untouched. BatchSeal.EDiff is the invariant, BatchSeal.bnBatchLA_exdiff the step that survives per-channel batch BN, and BatchSeal.eDiff_dw is the one new shape: a depthwise cannot broadcast, so where a centre-tap conv collapses the carrier to fun _ => s · δ 0 at every output channel, a centre-tap depthwise scales the whole function δ channel by channel. The class-0 output difference between the two examples is t · Rr t with Rr a 22-fold product of 1/64 · istd, continuous and positive, so g'(0) = Rr 0 ≠ 0.

Note: every collapse below is stated at variable N, h, w, ic, mid, oc and instantiated at the witness's numerals afterwards, never proved at them.