BackwardDot

Conv2D backward dot-level correctness (bridge lemma).

The runtime autograd engine (NN.Runtime.Autograd.Engine) computes Conv2D gradients via the handwritten spec:

• Spec.conv2d_backward_spec (kernel/bias/input)

For the analytic spec-level theorem over ℝ, Conv2D is already covered via fderiv/adjoints in:

• NN.Proofs.Autograd.Tape.Ops.Conv.FDeriv

That file provides a proof-only Conv2D node whose VJP is (fderiv forward)†, so any DAG using it is covered by the global theorem Graph.backpropVec_eq_adjoint_fderiv.

What remains here is the dot/adjointness bridge:

$$ \operatorname{dot}(\operatorname{JVP}_{\mathrm{conv2d}}(\ldots),\delta) =\operatorname{dot}(dK,g_K)+\operatorname{dot}(dB,g_B)+\operatorname{dot}(dX,g_X). $$

Here (gK, gB, gX) is the tuple returned by Spec.conv2d_backward_spec for $\delta$.

The padding-related rewrites needed for the input-gradient proof are factored into:

• NN/Spec/Layers/Utils.lean (get_at_or_zero_pad_multi_channel* lemmas)

theorem Proofs.Autograd.Conv2D.dot_add_right {s : Spec.Shape} (a b c : Spec.Tensor ℝ s) : Spec.dot a (b.addSpec c) = Spec.dot a b + Spec.dot a c

theorem Proofs.Autograd.Conv2D.dot_dim {n : ℕ} {s : Spec.Shape} (a b : Spec.Tensor ℝ (Spec.Shape.dim n s)) : Spec.dot a b = ∑ i : Fin n, Spec.dot (Spec.get a i) (Spec.get b i)

theorem Proofs.Autograd.Conv2D.dot_scalar (x y : ℝ) : Spec.dot (Spec.Tensor.scalar x) (Spec.Tensor.scalar y) = x * y

theorem Proofs.Autograd.Conv2D.dot_vec_eq_sum_get {n : ℕ} (a b : Spec.Tensor ℝ (Spec.Shape.dim n Spec.Shape.scalar)) : Spec.dot a b = ∑ i : Fin n, Spec.getAtOrZero a [↑i] * Spec.getAtOrZero b [↑i]

@[simp]

theorem Proofs.Autograd.Conv2D.get_at_or_zero_tensor_cast {s t : Spec.Shape} (h : s = t) (x : Spec.Tensor ℝ s) (idx : List ℕ) : Spec.getAtOrZero (x.castShape h) idx = Spec.getAtOrZero x idx

theorem Proofs.Autograd.Conv2D.get2_eq_get_at_or_zero {m n : ℕ} (A : Spec.Tensor ℝ (Spec.Shape.dim m (Spec.Shape.dim n Spec.Shape.scalar))) (i : Fin m) (j : Fin n) : Spec.get2 A i j = Spec.getAtOrZero A [↑i, ↑j]

theorem Proofs.Autograd.Conv2D.get_at_or_zero_get_channel {C H W : ℕ} (t : Spec.Tensor ℝ (Spec.Shape.dim C (Spec.Shape.dim H (Spec.Shape.dim W Spec.Shape.scalar)))) (c : Fin C) (i : Fin H) (j : Fin W) : Spec.getAtOrZero (Spec.get t c) [↑i, ↑j] = Spec.getAtOrZero t [↑c, ↑i, ↑j]

def Proofs.Autograd.Conv2D.biasBroadcast {outC outH outW : ℕ} (db : Spec.Tensor ℝ (Spec.Shape.dim outC Spec.Shape.scalar)) : Spec.Tensor ℝ (Spec.Shape.dim outC (Spec.Shape.dim outH (Spec.Shape.dim outW Spec.Shape.scalar)))

Broadcast a bias gradient outC across spatial axes into an outC×outH×outW tensor.

theorem Proofs.Autograd.Conv2D.conv2d_bias_deriv_get {inC outC kH kW stride padding inH inW : ℕ} {h1 : inC ≠ 0} {h2 : kH ≠ 0} {h3 : kW ≠ 0} (layer : Spec.Conv2DSpec inC outC kH kW stride padding ℝ h1 h2 h3) (input : Spec.Tensor ℝ (Spec.Shape.dim inC (Spec.Shape.dim inH (Spec.Shape.dim inW Spec.Shape.scalar)))) (δ : Spec.Tensor ℝ (Spec.Shape.dim outC (Spec.Shape.dim (Spec.Shape.slidingWindowOutDim inH kH stride padding) (Spec.Shape.dim (Spec.Shape.slidingWindowOutDim inW kW stride padding) Spec.Shape.scalar)))) (oc : Fin outC) : Spec.getAtOrZero (Spec.conv2dBiasDerivSpec layer input δ) [↑oc] = ∑ i : Fin (Spec.Shape.slidingWindowOutDim inH kH stride padding), ∑ j : Fin (Spec.Shape.slidingWindowOutDim inW kW stride padding), Spec.getAtOrZero δ [↑oc, ↑i, ↑j]

theorem Proofs.Autograd.Conv2D.dot_biasBroadcast_eq_dot_bias_deriv {inC outC kH kW stride padding inH inW : ℕ} {h1 : inC ≠ 0} {h2 : kH ≠ 0} {h3 : kW ≠ 0} (layer : Spec.Conv2DSpec inC outC kH kW stride padding ℝ h1 h2 h3) (input : Spec.Tensor ℝ (Spec.Shape.dim inC (Spec.Shape.dim inH (Spec.Shape.dim inW Spec.Shape.scalar)))) (db : Spec.Tensor ℝ (Spec.Shape.dim outC Spec.Shape.scalar)) (δ : Spec.Tensor ℝ (Spec.Shape.dim outC (Spec.Shape.dim (Spec.Shape.slidingWindowOutDim inH kH stride padding) (Spec.Shape.dim (Spec.Shape.slidingWindowOutDim inW kW stride padding) Spec.Shape.scalar)))) : Spec.dot (biasBroadcast db) δ = Spec.dot db (Spec.conv2dBiasDerivSpec layer input δ)

theorem Proofs.Autograd.Conv2D.dot3_eq_sum {C H W : ℕ} (a b : Spec.Tensor ℝ (Spec.Shape.dim C (Spec.Shape.dim H (Spec.Shape.dim W Spec.Shape.scalar)))) : Spec.dot a b = ∑ c : Fin C, ∑ i : Fin H, ∑ j : Fin W, Spec.getAtOrZero a [↑c, ↑i, ↑j] * Spec.getAtOrZero b [↑c, ↑i, ↑j]

theorem Proofs.Autograd.Conv2D.get_at_or_zero_get_outer3 {OC IC KH KW : ℕ} (k : Spec.Tensor ℝ (Spec.Shape.dim OC (Spec.Shape.dim IC (Spec.Shape.dim KH (Spec.Shape.dim KW Spec.Shape.scalar))))) (oc : Fin OC) (ic : Fin IC) (di : Fin KH) (dj : Fin KW) : Spec.getAtOrZero (Spec.get k oc) [↑ic, ↑di, ↑dj] = Spec.getAtOrZero k [↑oc, ↑ic, ↑di, ↑dj]

theorem Proofs.Autograd.Conv2D.dot4_eq_sum {OC IC KH KW : ℕ} (a b : Spec.Tensor ℝ (Spec.Shape.dim OC (Spec.Shape.dim IC (Spec.Shape.dim KH (Spec.Shape.dim KW Spec.Shape.scalar))))) : Spec.dot a b = ∑ oc : Fin OC, ∑ ic : Fin IC, ∑ di : Fin KH, ∑ dj : Fin KW, Spec.getAtOrZero a [↑oc, ↑ic, ↑di, ↑dj] * Spec.getAtOrZero b [↑oc, ↑ic, ↑di, ↑dj]

theorem Proofs.Autograd.Conv2D.sum_mul {ι : Type} [Fintype ι] (f : ι → ℝ) (a : ℝ) : (∑ i : ι, f i) * a = ∑ i : ι, f i * a

theorem Proofs.Autograd.Conv2D.mul_sum {ι : Type} [Fintype ι] (a : ℝ) (f : ι → ℝ) : a * ∑ i : ι, f i = ∑ i : ι, a * f i

theorem Proofs.Autograd.Conv2D.sum_comm {α β : Type} [Fintype α] [Fintype β] (f : α → β → ℝ) : ∑ a : α, ∑ b : β, f a b = ∑ b : β, ∑ a : α, f a b

theorem Proofs.Autograd.Conv2D.sum_third_first {α β γ : Type} [Fintype α] [Fintype β] [Fintype γ] (f : α → β → γ → ℝ) : ∑ a : α, ∑ b : β, ∑ c : γ, f a b c = ∑ c : γ, ∑ a : α, ∑ b : β, f a b c

Move the third index of a finite triple sum to the outside.

theorem Proofs.Autograd.Conv2D.sum_fourth_first {α β γ δ : Type} [Fintype α] [Fintype β] [Fintype γ] [Fintype δ] (f : α → β → γ → δ → ℝ) : ∑ a : α, ∑ b : β, ∑ c : γ, ∑ d : δ, f a b c d = ∑ d : δ, ∑ a : α, ∑ b : β, ∑ c : γ, f a b c d

Move the fourth index of a finite quadruple sum to the outside.

theorem Proofs.Autograd.Conv2D.sum_eight_conv_input_order {α β γ δ ε ζ η θ : Type} [Fintype α] [Fintype β] [Fintype γ] [Fintype δ] [Fintype ε] [Fintype ζ] [Fintype η] [Fintype θ] (f : α → β → γ → δ → ε → ζ → η → θ → ℝ) : ∑ a : α, ∑ b : β, ∑ c : γ, ∑ d : δ, ∑ e : ε, ∑ z : ζ, ∑ g : η, ∑ h : θ, f a b c d e z g h = ∑ d : δ, ∑ e : ε, ∑ z : ζ, ∑ a : α, ∑ g : η, ∑ h : θ, ∑ b : β, ∑ c : γ, f a b c d e z g h

Reorder the eight indices used when expanding the Conv2D input adjoint.

paddedInput matches the forward spec’s padding convention:

• if padding = 0, it is just a shape cast; and
• otherwise it is pad_multi_channel.

PyTorch analogue: torch.nn.functional.pad (or implicit padding inside conv2d). https://pytorch.org/docs/stable/generated/torch.nn.functional.pad.html https://pytorch.org/docs/stable/generated/torch.nn.functional.conv2d.html

noncomputable def Proofs.Autograd.Conv2D.paddedInput {inC inH inW padding : ℕ} (input : Spec.Tensor ℝ (Spec.Shape.dim inC (Spec.Shape.dim inH (Spec.Shape.dim inW Spec.Shape.scalar)))) : Spec.Tensor ℝ (Spec.Shape.dim inC (Spec.Shape.dim (inH + 2 * padding) (Spec.Shape.dim (inW + 2 * padding) Spec.Shape.scalar)))

theorem Proofs.Autograd.Conv2D.get_at_or_zero_paddedInput {inC inH inW padding : ℕ} (img : Spec.Tensor ℝ (Spec.Shape.dim inC (Spec.Shape.dim inH (Spec.Shape.dim inW Spec.Shape.scalar)))) (c : Fin inC) (p q : ℕ) : Spec.getAtOrZero (paddedInput img) [↑c, p, q] = if _h : p < padding ∨ q < padding then 0 else Spec.getAtOrZero img [↑c, p - padding, q - padding]

theorem Proofs.Autograd.Conv2D.mkInputIdx_match_eq_paddedInput {inC inH inW stride padding : ℕ} (img : Spec.Tensor ℝ (Spec.Shape.dim inC (Spec.Shape.dim inH (Spec.Shape.dim inW Spec.Shape.scalar)))) (c : Fin inC) (oi di oj dj : ℕ) : (match Spec.Private.mkInputIdx? [oi, oj] [di, dj] [stride, stride] [padding, padding] with | none => 0 | some inIdx => Spec.getAtOrZero img (↑c :: inIdx)) = Spec.getAtOrZero (paddedInput img) [↑c, oi * stride + di, oj * stride + dj]

theorem Proofs.Autograd.Conv2D.sum_shift_eq_paddedInput {inC inH inW padding : ℕ} (x : Spec.Tensor ℝ (Spec.Shape.dim inC (Spec.Shape.dim inH (Spec.Shape.dim inW Spec.Shape.scalar)))) (ic : Fin inC) (p q : ℕ) : (∑ i : Fin inH, ∑ j : Fin inW, if p = ↑i + padding ∧ q = ↑j + padding then Spec.getAtOrZero x [↑ic, ↑i, ↑j] else 0) = Spec.getAtOrZero (paddedInput x) [↑ic, p, q]

theorem Proofs.Autograd.Conv2D.sum_shift_mul_eq_paddedInput_mul {inC inH inW padding : ℕ} (x : Spec.Tensor ℝ (Spec.Shape.dim inC (Spec.Shape.dim inH (Spec.Shape.dim inW Spec.Shape.scalar)))) (ic : Fin inC) (p q : ℕ) (c : ℝ) : (∑ i : Fin inH, ∑ j : Fin inW, Spec.getAtOrZero x [↑ic, ↑i, ↑j] * if p = ↑i + padding ∧ q = ↑j + padding then c else 0) = Spec.getAtOrZero (paddedInput x) [↑ic, p, q] * c

Collapse the shifted input indicator while carrying a constant scalar factor.

Output shape helpers (no dilation): these are the standard “convolution arithmetic” formulas. They are kept as definitions so later statements can share the same expression.

def Proofs.Autograd.Conv2D.outH (inH kH stride padding : ℕ) : ℕ

def Proofs.Autograd.Conv2D.outW (inW kW stride padding : ℕ) : ℕ

Output width helper (no dilation).

theorem Proofs.Autograd.Conv2D.conv2d_spec_noBias_get {inC outC kH kW stride padding inH inW : ℕ} {h1 : inC ≠ 0} {h2 : kH ≠ 0} {h3 : kW ≠ 0} (dKernel : Spec.Tensor ℝ (Spec.Shape.dim outC (Spec.Shape.dim inC (Spec.Shape.dim kH (Spec.Shape.dim kW Spec.Shape.scalar))))) (input : Spec.Tensor ℝ (Spec.Shape.dim inC (Spec.Shape.dim inH (Spec.Shape.dim inW Spec.Shape.scalar)))) (oc : Fin outC) (i : Fin (outH inH kH stride padding)) (j : Fin (outW inW kW stride padding)) : have layerK := { kernel := dKernel, bias := Spec.fill 0 (Spec.Shape.dim outC Spec.Shape.scalar) }; Spec.getAtOrZero (Spec.conv2dSpec layerK input) [↑oc, ↑i, ↑j] = ∑ ic : Fin inC, ∑ di : Fin kH, ∑ dj : Fin kW, Spec.getAtOrZero dKernel [↑oc, ↑ic, ↑di, ↑dj] * Spec.getAtOrZero (paddedInput input) [↑ic, ↑i * stride + ↑di, ↑j * stride + ↑dj]

theorem Proofs.Autograd.Conv2D.conv2d_kernel_deriv_get {inC outC kH kW stride padding inH inW : ℕ} {h1 : inC ≠ 0} {h2 : kH ≠ 0} {h3 : kW ≠ 0} (layer : Spec.Conv2DSpec inC outC kH kW stride padding ℝ h1 h2 h3) (input : Spec.Tensor ℝ (Spec.Shape.dim inC (Spec.Shape.dim inH (Spec.Shape.dim inW Spec.Shape.scalar)))) (δ : Spec.Tensor ℝ (Spec.Shape.dim outC (Spec.Shape.dim (outH inH kH stride padding) (Spec.Shape.dim (outW inW kW stride padding) Spec.Shape.scalar)))) (oc : Fin outC) (ic : Fin inC) (di : Fin kH) (dj : Fin kW) : Spec.getAtOrZero (Spec.conv2dKernelDerivSpec layer input δ) [↑oc, ↑ic, ↑di, ↑dj] = ∑ i : Fin (outH inH kH stride padding), ∑ j : Fin (outW inW kW stride padding), Spec.getAtOrZero (paddedInput input) [↑ic, ↑i * stride + ↑di, ↑j * stride + ↑dj] * Spec.getAtOrZero δ [↑oc, ↑i, ↑j]

theorem Proofs.Autograd.Conv2D.conv2d_input_deriv_get {inC outC kH kW stride padding inH inW : ℕ} {h1 : inC ≠ 0} {h2 : kH ≠ 0} {h3 : kW ≠ 0} (layer : Spec.Conv2DSpec inC outC kH kW stride padding ℝ h1 h2 h3) (input : Spec.Tensor ℝ (Spec.Shape.dim inC (Spec.Shape.dim inH (Spec.Shape.dim inW Spec.Shape.scalar)))) (δ : Spec.Tensor ℝ (Spec.Shape.dim outC (Spec.Shape.dim (outH inH kH stride padding) (Spec.Shape.dim (outW inW kW stride padding) Spec.Shape.scalar)))) (ic : Fin inC) (i : Fin inH) (j : Fin inW) : Spec.getAtOrZero (Spec.conv2dInputDerivSpec layer input δ) [↑ic, ↑i, ↑j] = ∑ oc : Fin outC, ∑ oi : Fin (outH inH kH stride padding), ∑ oj : Fin (outW inW kW stride padding), ∑ di : Fin kH, ∑ dj : Fin kW, if _h : ↑oi * stride + ↑di = ↑i + padding ∧ ↑oj * stride + ↑dj = ↑j + padding then Spec.getAtOrZero δ [↑oc, ↑oi, ↑oj] * Spec.getAtOrZero layer.kernel [↑oc, ↑ic, ↑di, ↑dj] else 0