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

MobileNetV4FullBVJP.lean proves mobilenetv4ForwardBFullHasVJPAt: the whole-net VJP at any (w, x) satisfying eight clause bundles — the stem's relu, the fused stage's, one per resolution group and the head's, 38 relu sites in all (the #guard below counts them off the block table). That statement is pointwise, so it could in principle be vacuous. This file exhibits a (w, x) that discharges every clause — centre-tap kernels on the stem, the fused stage, the three channel-changing rows and the head; the eighteen skip rows zeroed, each block then the exact identity — shows the forward is not constant there, and seals the Jacobian nonzero — hence, through Training/JacobianSeal.lean, the proven backward is not the zero map at that point.

The net is timm's mobilenetv4_conv_medium: relu throughout, BN-only pre-DWs, the stride on each downsample's post-DW, and a head that pools before conv_head, whose BatchNorm therefore normalises the pooled features over the batch alone.

All 38 clauses are weight-only — and generic in the table row #

Every kink in this net is a relu sitting directly on a bnBatchLA output (Mnv4StemSmoothAtB, cbReluLayer.ok, cbReluStridedLayer.ok, mnv4DWReluLayer.ok, mnv4DWReluStridedLayer.ok); projLayer.ok, mnv4DWBnLayer.ok, castLayer.ok and CertLayer.id'.ok are True. bnBatchLA_pos bounds a BatchNorm output above β − |γ|√(N·h·w) > 0 at EVERY input, so with γ = 1, β = 160, ε = 1 the whole bundle is discharged without the activation ever being read — including conv_head's, whose BatchNorm sees N·1·1 = 2 cells.

The carrier #

The input is per-(example, channel) constant (sealX t = t • rayV), so it is an EDiff from the start: example 0 is example 1 plus t on channel 0. Every stage on the carrier's path is a centre-tap conv or depthwise then a BatchNorm, and inside the margin window every relu is the identity, so each stage multiplies the carrier by one positive istd. Seventeen BatchNorms sit on the path: the stem's, the fused stage's two, four in each of rows 1, 3 and 11 (the only rows that change channels, hence the only ones without a skip) and the head's two. The pool in front of conv_head keeps the carrier (a per-channel shift survives an average), and the two relabels are index bijections. The readout along the ray is therefore t · Rr t, with Rr the product of the seventeen istds: continuous and positive, and no BatchNorm variance derivative is taken.

Note: every collapse, every clause bundle and every block lemma here is proved at variable shapes and instantiated at the witness's numerals afterwards, never proved at them.