Conv2D Backward as a RuntimeApprox Reverse Node

The previous files prove pointwise bounds for the bias, kernel, and input-gradient pieces. This file packages those pieces into the RevNode interface used by the generic reverse-graph approximation theorems, so Conv2D backward can participate in end-to-end NeuralFloat runtime proofs.

noncomputable def Proofs.RuntimeApprox.NFBackend.conv2dRevNode {β : TorchLean.Floats.NeuralRadix} {fexp : ℤ → ℤ} [TorchLean.Floats.NeuralValidExp fexp] {rnd : ℝ → ℤ} [TorchLean.Floats.NeuralValidRndToNearest rnd] {Γ : List Spec.Shape} {inC outC kH kW stride padding inH inW : ℕ} {h1 : inC ≠ 0} {h2 : kH ≠ 0} {h3 : kW ≠ 0} (kernelIdx : Idx Γ (Spec.Shape.dim outC (Spec.Shape.dim inC (Spec.Shape.dim kH (Spec.Shape.dim kW Spec.Shape.scalar))))) (biasIdx : Idx Γ (Spec.Shape.dim outC Spec.Shape.scalar)) (inputIdx : Idx Γ (Spec.Shape.dim inC (Spec.Shape.dim inH (Spec.Shape.dim inW Spec.Shape.scalar)))) : RevNode toSpec Γ (Spec.Shape.dim outC (Spec.Shape.dim (conv2dOutH inH kH stride padding) (Spec.Shape.dim (conv2dOutW inW kW stride padding) Spec.Shape.scalar)))

Package Conv2D forward + backward (VJP) as a RevNode for RevGraph.backprop_approx.

The node uses the forward bound from conv2d_forward and the three gradient bounds proved in this file (kernel/bias/input) to provide a compositional reverse-mode approximation theorem.