Closing the MobileNetV2 render — the depthwise / strided parameter-gradient bridges

planning/archive/mobilenetv2_close.md Item C — the "free close" (generic in the cotangent the backward chain delivers at each layer's output, the CIFAR-non-BN-style close): every MobileNetV2 train-step parameter output denotes θ − lr·(certified Jacobian · cotangent).

The MobileNetV2 train step (tests/TestMobilenetV2Train.lean) has these parameter families, and each is now certified by the bridge in the right column:

family (render SSA)	forward fn	certified by
1×1 conv W (expand eW / project pW / head hW)	conv2d (stride 1)	cnn_render_convW_certified (M3, reuse)
1×1 conv b (eb / pb / hb)	conv2d	cnn_render_convb_certified (M3, reuse)
BN γ (eg/dg/pg/hg/sg)	bnPerChannelFlat	cifar_bn_render_gamma_certified (reuse)
BN β (ebt/dbt/pbt/hbt/sbt)	bnPerChannelFlat	cifar_bn_render_beta_certified (reuse)
dense Wd / bd	matmul / +bias	weight_grad_bridge / bias_grad_bridge (M2, reuse)
stem 3×3 conv W (sW, stride 2)	flatConvStride2	mnv2_render_stem_convW_certified (new wrapper)
stem 3×3 conv b (sb, stride 2)	flatConvStride2	mnv2_render_stem_convb_certified (new)
depthwise W stride 1 (dW, blocks b2,b4)	depthwiseConv2d	mnv2_render_depthwiseW_certified (new)
depthwise b stride 1 (db, blocks b2,b4)	depthwiseConv2d	mnv2_render_depthwiseb_certified (new)
depthwise W stride 2 (dW, blocks b1,b3,b5,b6)	depthwiseStride2Flat	mnv2_render_depthwiseW_strided_certified (new)
depthwise b stride 2 (db, blocks b1,b3,b5,b6)	depthwiseStride2Flat	mnv2_render_depthwiseb_strided_certified (new)

The reuse families need no new theorem — the generic M2/M3/CIFAR-BN bridges apply verbatim at the MobileNetV2 shapes. This file supplies the genuinely-new pieces:

• Depthwise (stride-1) W/b — the .correct fields of the proven depthwise_weight_grad_has_vjp3 / depthwise_bias_grad_has_vjp (Depthwise.lean), SGD-wrapped. The "one genuinely-new bridge family" of the plan — instantiation, the VJP itself is already proven 3-axiom-clean.
• Stem strided conv W/b — wrappers of flatConvStride2_weight_grad_has_vjp (ch6) and a new strided-conv bias VJP.
• Strided depthwise W/b (4 of 6 blocks downsample) — a new strided-depthwise weight/bias VJP, the exact decimate ∘ stride-1 recipe of flatConvStride2_weight_grad_has_vjp with the depthwise kernel. (The plan's Item C list omitted these; the downsampling blocks need them for honest coverage.) Each is vjp_comp of a proven stride-1 depthwise VJP with decimateFlat's VJP.

All bridges are generic in the cotangent c/dy the backward chain delivers at the layer output (pinning that cotangent to the actual inverted-residual chain is the optional Item D). The SGD wrapping θ − lr·∇ is identical to the linear/MLP/CNN cases.

theorem Proofs.mnv2_depthwise_weight_grad_bridge {c h w kH kW : ℕ} (b : Vec c) (x : Tensor3 c h w) (W : DepthwiseKernel c kH kW) (dy : Tensor3 c h w) (ci : Fin c) (hi : Fin kH) (wi : Fin kW) : (depthwise_weight_grad_has_vjp3 b x).backward W dy ci hi wi = ∑ co : Fin c, ∑ ho : Fin h, ∑ wo : Fin w, pdiv3 (fun (W' : DepthwiseKernel c kH kW) => depthwiseConv2d W' b x) W ci hi wi co ho wo * dy co ho wo

Depthwise weight-gradient bridge. At any cotangent dy at the depthwise layer's output and any kernel W, the emitted per-channel depthwise kernel gradient equals the certified Jacobian of depthwiseConv2d viewed as a function of the kernel, contracted with dy. The .correct field of depthwise_weight_grad_has_vjp3.

theorem Proofs.mnv2_depthwise_bias_grad_bridge {c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (x : Tensor3 c h w) (b : Vec c) (dy : Vec (c * h * w)) (cc : Fin c) : (depthwise_bias_grad_has_vjp W x).backward b dy cc = ∑ j : Fin (c * h * w), pdiv (fun (b' : Vec c) => (depthwiseConv2d W b' x).flatten) b cc j * dy j

Depthwise bias-gradient bridge. Likewise the per-channel depthwise bias gradient (db[c] = Σ_spatial dy) is the certified Jacobian of depthwiseConv2d wrt the bias, contracted with dy — the .correct field of depthwise_bias_grad_has_vjp.

theorem Proofs.mnv2_render_depthwiseW_certified {c h w kH kW : ℕ} (b : Vec c) (x : Tensor3 c h w) (W : DepthwiseKernel c kH kW) (dy : Tensor3 c h w) (lr : ℝ) (ci : Fin c) (hi : Fin kH) (wi : Fin kW) : W ci hi wi - lr * (depthwise_weight_grad_has_vjp3 b x).backward W dy ci hi wi = W ci hi wi - lr * ∑ co : Fin c, ∑ ho : Fin h, ∑ wo : Fin w, pdiv3 (fun (W' : DepthwiseKernel c kH kW) => depthwiseConv2d W' b x) W ci hi wi co ho wo * dy co ho wo

Depthwise weight output, certified. Wⁿ = W − lr·(per-channel transpose-trick grad) denotes, at the kernel W, W − lr·(certified ∂(depthwiseConv2d)/∂W · cotangent). The depthwise peer of cnn_render_convW_certified.

theorem Proofs.mnv2_render_depthwiseb_certified {c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (x : Tensor3 c h w) (b : Vec c) (dy : Vec (c * h * w)) (lr : ℝ) (cc : Fin c) : b cc - lr * (depthwise_bias_grad_has_vjp W x).backward b dy cc = b cc - lr * ∑ j : Fin (c * h * w), pdiv (fun (b' : Vec c) => (depthwiseConv2d W b' x).flatten) b cc j * dy j

Depthwise bias output, certified. Likewise bⁿ = b − lr·(spatial reduce) denotes b − lr·(certified ∂(depthwiseConv2d)/∂b · cotangent).

theorem Proofs.mnv2_render_stem_convW_certified {ic oc h w kH kW : ℕ} (b : Vec oc) (x : Vec (ic * (2 * h) * (2 * w))) (v : Vec (oc * ic * kH * kW)) (dy : Vec (oc * h * w)) (lr : ℝ) (i : Fin (oc * ic * kH * kW)) : v i - lr * (flatConvStride2_weight_grad_has_vjp b x).backward v dy i = v i - lr * ∑ j : Fin (oc * h * w), pdiv (fun (v' : Vec (oc * ic * kH * kW)) => flatConvStride2 (Kernel4.unflatten v') b x) v i j * dy j

Stem conv weight output, certified. sWⁿ = sW − lr·(strided transpose-trick grad) denotes sW − lr·(certified ∂(flatConvStride2)/∂sW · cotangent), via flatConvStride2_weight_grad_has_vjp (the ch6 strided conv weight VJP).

theorem Proofs.mnv2_render_stem_convW_xla_certified {ic oc h w kH kW : ℕ} (b : Vec oc) (x : Vec (ic * (2 * h) * (2 * w))) (v : Vec (oc * ic * kH * kW)) (dy : Vec (oc * h * w)) (lr : ℝ) (i : Fin (oc * ic * kH * kW)) : v i - lr * (flatConvStride2Xla_weight_grad_has_vjp b x).backward v dy i = v i - lr * ∑ j : Fin (oc * h * w), pdiv (fun (v' : Vec (oc * ic * kH * kW)) => flatConvStride2Xla (Kernel4.unflatten v') b x) v i j * dy j

Stem conv weight output, certified — XLA-SAME phase. mnv2_render_stem_convW_certified at flatConvStride2Xla, the stem MobileNetV2 ships (every artifact since 2026-09-05; the Adam ones since 2026-08-08). ⚠ The symmetric lemma above stays: ResNet-34's PoC reuses it, and ResNet's stem is PyTorch-origin symmetric.

theorem Proofs.mnv2_render_stem_convb_certified {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (x : Vec (ic * (2 * h) * (2 * w))) (b : Vec oc) (dy : Vec (oc * h * w)) (lr : ℝ) (o : Fin oc) : b o - lr * (flatConvStride2_bias_grad_has_vjp W x).backward b dy o = b o - lr * ∑ j : Fin (oc * h * w), pdiv (fun (b' : Vec oc) => flatConvStride2 W b' x) b o j * dy j

Stem conv bias output, certified. sbⁿ = sb − lr·(spatial reduce) denotes sb − lr·(certified ∂(flatConvStride2)/∂sb · cotangent).

theorem Proofs.mnv2_render_stem_convb_xla_certified {ic oc h w kH kW : ℕ} (W : Kernel4 oc ic kH kW) (x : Vec (ic * (2 * h) * (2 * w))) (b : Vec oc) (dy : Vec (oc * h * w)) (lr : ℝ) (o : Fin oc) : b o - lr * (flatConvStride2Xla_bias_grad_has_vjp W x).backward b dy o = b o - lr * ∑ j : Fin (oc * h * w), pdiv (fun (b' : Vec oc) => flatConvStride2Xla W b' x) b o j * dy j

Stem conv bias output, certified — XLA-SAME phase.

theorem Proofs.mnv2_render_depthwiseW_strided_certified {c h w kH kW : ℕ} (b : Vec c) (x : Vec (c * (2 * h) * (2 * w))) (v : Vec (c * kH * kW)) (dy : Vec (c * h * w)) (lr : ℝ) (i : Fin (c * kH * kW)) : v i - lr * (depthwiseStride2_weight_grad_has_vjp b x).backward v dy i = v i - lr * ∑ j : Fin (c * h * w), pdiv (fun (v' : Vec (c * kH * kW)) => depthwiseStride2Flat (Tensor3.unflatten v') b x) v i j * dy j

Strided depthwise weight output, certified. Wⁿ = W − lr·(upsample-then-stride-1 grad) denotes W − lr·(certified ∂(depthwiseStride2Flat)/∂W · cotangent).

theorem Proofs.mnv2_render_depthwiseW_strided_xla_certified {c h w kH kW : ℕ} (b : Vec c) (x : Vec (c * (2 * h) * (2 * w))) (v : Vec (c * kH * kW)) (dy : Vec (c * h * w)) (lr : ℝ) (i : Fin (c * kH * kW)) : v i - lr * (depthwiseStride2Xla_weight_grad_has_vjp b x).backward v dy i = v i - lr * ∑ j : Fin (c * h * w), pdiv (fun (v' : Vec (c * kH * kW)) => depthwiseStride2FlatXla (Tensor3.unflatten v') b x) v i j * dy j

Strided depthwise weight output, certified — XLA-SAME phase. MobileNetV2's four strided depthwises. ⚠ The symmetric lemma above stays: EfficientNet-B0's strided depthwises are symmetric in render and reference alike (EfficientNetClose.lean reuses it).

theorem Proofs.mnv2_render_depthwiseb_strided_certified {c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (x : Vec (c * (2 * h) * (2 * w))) (b : Vec c) (dy : Vec (c * h * w)) (lr : ℝ) (o : Fin c) : b o - lr * (depthwiseStride2_bias_grad_has_vjp W x).backward b dy o = b o - lr * ∑ j : Fin (c * h * w), pdiv (fun (b' : Vec c) => depthwiseStride2Flat W b' x) b o j * dy j

Strided depthwise bias output, certified. bⁿ = b − lr·(spatial reduce) denotes b − lr·(certified ∂(depthwiseStride2Flat)/∂b · cotangent).

theorem Proofs.mnv2_render_depthwiseb_strided_xla_certified {c h w kH kW : ℕ} (W : DepthwiseKernel c kH kW) (x : Vec (c * (2 * h) * (2 * w))) (b : Vec c) (dy : Vec (c * h * w)) (lr : ℝ) (o : Fin c) : b o - lr * (depthwiseStride2Xla_bias_grad_has_vjp W x).backward b dy o = b o - lr * ∑ j : Fin (c * h * w), pdiv (fun (b' : Vec c) => depthwiseStride2FlatXla W b' x) b o j * dy j

Strided depthwise bias output, certified — XLA-SAME phase.