Conv2D input-gradient adjointness

This file proves the inner-product identity for the convolution input cotangent:

⟪conv(dInput, kernel), δ⟫ = ⟪dInput, conv2dInputDeriv(kernel, δ)⟫.

The statement is over the specification tensors, not over a backend implementation. That lets the runtime proof later use this file as a clean algebraic contract for the input-gradient rule. Most of the proof is finite-sum normalization: expand both dot products, rewrite each convolution entry, and reindex the sums so every contribution to an input pixel is collected in the same place.

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

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

The left side perturbs the input and pairs the resulting output perturbation with the output cotangent δ. The right side pairs that same input perturbation with the specification-level input derivative. This is the theorem used by the tape proof to justify the input-gradient part of Conv2D backpropagation.