Conv2D kernel-gradient adjointness

This file proves the inner-product identity for the convolution kernel cotangent. The result is the algebraic heart of the kernel-gradient backward rule:

⟪conv(dKernel, input), δ⟫ = ⟪dKernel, conv2dKernelDeriv(input, δ)⟫.

The proof is written over finite tensors indexed by Fin, so the main work is bookkeeping rather than analysis: expand the two dot products, commute the finite sums, and factor the candidate kernel perturbation back out. Keeping this proof separate from the input-gradient proof makes the three conv adjointness obligations easier to audit.

theorem Proofs.Autograd.Conv2D.dot_conv2d_kernel {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.MultiChannelImage inC inH inW ℝ) (dKernel : Spec.Tensor ℝ (Spec.Shape.dim outC (Spec.Shape.dim inC (Spec.Shape.dim kH (Spec.Shape.dim kW Spec.Shape.scalar))))) (δ : Spec.MultiChannelImage outC (outH inH kH stride padding) (outW inW kW stride padding) ℝ) : have layerK := { kernel := dKernel, bias := Spec.fill 0 (Spec.Shape.dim outC Spec.Shape.scalar) }; Spec.dot (Spec.conv2dSpec layerK input) δ = Spec.dot dKernel (Spec.conv2dKernelDerivSpec layer input δ)

Adjointness of the Conv2D forward map with respect to kernel perturbations.

The left side applies a no-bias convolution whose kernel is dKernel, then pairs the output with the cotangent δ. The right side pairs dKernel with the specification-level kernel derivative. This is the theorem used by the tape proof to justify the kernel part of Conv2D backpropagation.