§B shared prerequisite: the DEPTHWISE adjoint gate + leaf ties

The §B certified-VJP ties for the three CNNs (convnext / mnv2 / efficientnet) all reverse a depthwise convolution, so they all need the depthwise twin of the conv adjoint gate IR.convBackDenote_eq_input_grad_formula. This file builds it once.

• depthwiseConv2d_dwReverse_eq_input_grad_formula — the gate: the emitted reversed-kernel forward depthwise conv depthwiseConv2d (dwReverse W) 0 equals the certified depthwise input-gradient depthwiseConv2d_input_grad_formula W, for arbitrary dims with odd kernels. The exact depthwise analogue of the conv gate — same (kh,kw) ↦ (kh+hi-pH, kw+wi-pW) partial bijection on the pad supports, MINUS the Σ co channel sum (depthwise has no cross-channel mixing, so the input channel reads only from its own kernel/gradient channel ch).
• depthwiseFlatBack_eq_vjp_backward — the stride-1 leaf tie: the backward map depthwiseFlatBack W (= depthwiseFlat (dwReverse W) 0) IS the certified depthwise input-VJP (depthwiseFlat_has_vjp W b).backward x (depthwise conv is linear ⇒ the saved activation x is ignored). The depthwise peer of convFlatBack_eq_vjp_backward.
• depthwiseStride2FlatBack_eq_vjp_backward — the strided leaf tie: depthwiseStride2FlatBack W (= depthwiseFlatBack ∘ decimateBack) IS (depthwiseStride2Flat_has_vjp W b).backward x. The depthwise peer of flatConvStride2Back_eq_vjp_backward (conv leaf + the decimateBack rfl).

theorem Proofs.depthwiseConv2d_dwReverse_eq_input_grad_formula {c h w kH kW : ℕ} (hkH : 2 * ((kH - 1) / 2) + 1 = kH) (hkW : 2 * ((kW - 1) / 2) + 1 = kW) (W : DepthwiseKernel c kH kW) (dy : Tensor3 c h w) : depthwiseConv2d (dwReverse W) (fun (x : Fin c) => 0) dy = depthwiseConv2d_input_grad_formula W dy

The depthwise conv-adjoint identity (odd kernels), all dims. The emitted reversed-kernel forward depthwise conv depthwiseConv2d (dwReverse W) 0 equals the certified depthwise input-gradient depthwiseConv2d_input_grad_formula W, for arbitrary c h w kH kW with odd kernels. The depthwise twin of IR.convBackDenote_eq_input_grad_formula: per output coordinate both sides sum over the SAME valid alignments via (kh,kw) ↦ (kh+hi-pH, kw+wi-pW); under oddness 2·pH = kH-1 the reversed-kernel index kH-1-kh matches the formula's hi+pH-ho. No Σ co (depthwise channel ch is fixed). Finset.sum_bij' over the pad-filtered supports; all index arithmetic by omega. The load-bearing leaf for the depthwise §B ties (convnext/mnv2/enet).

theorem Proofs.depthwiseFlatBack_eq_vjp_backward {c h w kH kW : ℕ} (hkH : 2 * ((kH - 1) / 2) + 1 = kH) (hkW : 2 * ((kW - 1) / 2) + 1 = kW) (W : DepthwiseKernel c kH kW) (b : Vec c) (x : Vec (c * h * w)) : depthwiseFlatBack W = (depthwiseFlat_has_vjp W b).backward x

Depthwise conv input-VJP leaf tie. The backward map depthwiseFlatBack W (= reversed-kernel forward depthwise conv) IS the certified depthwise input-VJP (depthwiseFlat_has_vjp W b).backward x (depthwise conv is linear, so the saved activation x is ignored), for odd kernels. Routes through depthwiseConv2d_dwReverse_eq_input_grad_formula; the depthwise peer of convFlatBack_eq_vjp_backward.

theorem Proofs.depthwiseStride2FlatBack_eq_vjp_backward {c h w kH kW : ℕ} (hkH : 2 * ((kH - 1) / 2) + 1 = kH) (hkW : 2 * ((kW - 1) / 2) + 1 = kW) (W : DepthwiseKernel c kH kW) (b : Vec c) (x : Vec (c * (2 * h) * (2 * w))) : depthwiseStride2FlatBack W = (depthwiseStride2Flat_has_vjp W b).backward x

Strided depthwise conv input-VJP leaf tie. depthwiseStride2FlatBack W (= depthwiseFlatBack ∘ decimateBack) IS the certified strided depthwise input-VJP (depthwiseStride2Flat_has_vjp W b).backward x, for odd kernels. Decomposes into the stride-1 depthwise leaf tie (depthwiseFlatBack_eq_vjp_backward) and the decimate leaf (decimateBack_eq_vjp, rfl), matching depthwiseStride2Flat = decimateFlat ∘ depthwiseFlat. The depthwise peer of flatConvStride2Back_eq_vjp_backward; unlocks the mnv2 stride-2 inverted-residual downsample.

theorem Proofs.depthwiseStride2FlatXlaBack_eq_vjp_backward {c h w kH kW : ℕ} (hkH : 2 * ((kH - 1) / 2) + 1 = kH) (hkW : 2 * ((kW - 1) / 2) + 1 = kW) (W : DepthwiseKernel c kH kW) (b : Vec c) (x : Vec (c * (2 * h) * (2 * w))) : depthwiseStride2FlatXlaBack W = (depthwiseStride2FlatXla_has_vjp W b).backward x

XLA-SAME strided depthwise input-VJP leaf tie. depthwiseStride2FlatXlaBack W (= depthwiseFlatBack ∘ decimateOddBack) IS the certified (depthwiseStride2FlatXla_has_vjp W b).backward x, for odd kernels. The odd-phase peer of depthwiseStride2FlatBack_eq_vjp_backward; MobileNetV2's four strided depthwises and B0's downsample depthwise, at the TF-origin convention.