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

planning/full_width_seals.md §4.4, the last of four. MobileNetV4FullBVJP.lean proves mobilenetv4ForwardB_full_has_vjp_at: the whole-net VJP at any (w, x) satisfying eight clause bundles — the stem's relu, the fused stage's (vacuous), one per resolution group and the head's, 54 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 with genuinely nonzero weights, 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. MobileNetV4 had no witness at any depth before this; with it, every kinked net in the book is sealed on the forward its artifacts run.

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

Every kink in this net is a relu sitting directly on a bnBatchLA output, in four spellings (Mnv4StemSmoothAtB, cbReluLayer.ok, mnv4DWReluLayer.ok, mnv4DWReluStridedLayer.ok); projLayer.ok, mnv4FusedConvLayer.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. ⭐ Better still, the discharge is proved generically in the UibSpec row (sealUib_ok, sealUibStrided_ok): the k = 0 depthwise slots contribute True and the rest are the same BatchNorm fact, so 21 blocks cost two lemmas.

⭐⭐ The swish is the one thing that is not MobileNetV2 again #

planning/full_width_seals.md §4.4 called the clause bundle the package's remaining uncertainty and the CertLayer peel its real work. Both turned out cheap — CertLayer.comp_fwd_apply and the group *_fwd_apply lemmas in MobileNetV4FullB.lean already peel at variables. What was missed is the fused stage's swish, and it changes the witness:

• the other three seals ride a positionally-injective ramp, which a stem max-pool's no-tie needs. A carrier crosses their relus because relu is the identity inside the margin window;
• swish is the identity on no window at all. A gap between the two examples comes out of it as swish(a) − swish(b), which is not a multiple of a − b and — worse — is not even constant over the grid unless a and b are;
• ⭐ so this witness's base is grid-constant, not a ramp: sealX t = t • rayV. Then every activation down to the fused BatchNorm is one value per (example, channel) (BUnif), that BatchNorm puts the two values symmetrically about β (bnBatchLA_pair), and the swish's two outputs differ by swishGap β u — a function of their half-gap u alone. EDiff takes over from there and every remaining stage is multiplicative. MobileNetV4 has no pool, so nothing wanted the ramp.

The readout along the ray is therefore swishGap 160 (uF t 0) · Rr t, not t · Rr t, and the seal closes with hasDerivAt_mul_of_zero rather than hasDerivAt_mul_self_zero. ⚠ No BatchNorm variance derivative is taken anywhere: the two pre-swish factors enter through t · Q0 t and the fifteen after it through a continuous Rr; the swish's slope at β is the one honest derivative in the chain, and it is positive for every β ≥ 0.

The carrier threads seventeen BatchNorms #

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. ⛔ Counted from the net, not from prose: the other eighteen rows are CertLayer.residual, so the carrier goes round their bodies. With the project BatchNorm's β = 0 a zeroed body is the constant 0, so those rows are the EXACT identity and two of the seven groups collapse to nothing at all.

⚠⚠ 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 (planning/full_width_seals.md §3.5). ⚠ And a lemma whose spatial dims are only reachable through a Vec (… (2*h) …) argument needs them passed explicitly — 2 * ?h =?= 56 is nonlinear, and BUnif_convS2 without (h := 56) (w := 56) is a maxHeartbeats timeout in isDefEq.