Real convolution and its affine representation

The coefficient matrix uses the same grouped channel and dilated spatial relation as the convolution specification. The equalities in this module concern real arithmetic; they do not assert agreement between different floating-point reduction orders.

theorem NN.MLTheory.CROWN.ConvProof.mkDilatedInputIdx?_kernel_unique {outIdx left right stride dilation padding inputIdx : List ℕ} (hdil : ∀ d ∈ dilation, 0 < d) (hl : Spec.Conv.Internal.mkDilatedInputIdx? outIdx left stride dilation padding = some inputIdx) (hr : Spec.Conv.Internal.mkDilatedInputIdx? outIdx right stride dilation padding = some inputIdx) : left = right

Positive dilation makes the spatial input-index relation injective in the kernel index.

theorem NN.MLTheory.CROWN.ConvProof.convKernelCoefficient_eq_sum (kernel outIdx inputIdx stride dilation padding : List ℕ) (weight : List ℕ → ℝ) : convKernelCoefficient kernel outIdx inputIdx stride dilation padding weight = ∑ k : (Spec.Shape.ofList kernel).Coord, if Spec.Conv.Internal.mkDilatedInputIdx? outIdx (Spec.Shape.Coord.toList (Spec.Shape.ofList kernel) k) stride dilation padding = some inputIdx then weight (Spec.Shape.Coord.toList (Spec.Shape.ofList kernel) k) else 0

Direct selection and the zero-dilation fallback both give the real coefficient sum.

theorem NN.MLTheory.CROWN.ConvProof.convKernelCoefficient_map {α β : Type} [TorchLean.Storage α] [Context α] [TorchLean.Storage β] [Context β] (f : α → β) (hf : f 0 = 0) (kernel outIdx inputIdx stride dilation padding : List ℕ) (weight : List ℕ → α) (hdil : ∀ d ∈ dilation, 0 < d) : (convKernelCoefficient kernel outIdx inputIdx stride dilation padding fun (k : List ℕ) => f (weight k)) = f (convKernelCoefficient kernel outIdx inputIdx stride dilation padding weight)

For positive dilation, selecting a stored coefficient commutes with any scalar map that preserves zero.

theorem NN.MLTheory.CROWN.ConvProof.conv_linear_matrix_add_bias_eq_grouped_conv {d inC outC : ℕ} {kernel stride padding inSpatial : TorchLean.Tensor ℕ [d]} (layer : Spec.ConvSpec d inC outC kernel stride padding ℝ) (dilation paddingAfter : TorchLean.Tensor ℕ [d]) (groups : ℕ) (leading : Spec.Shape) (input : TorchLean.Tensor ℝ (leading.concat (Spec.Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList)))) : (Spec.matVecMulSpec (convLinearMatrix layer dilation paddingAfter groups leading) input.flattenSpec).addSpec (convBiasBroadcast layer.bias leading) = (TorchLean.Tensor.mapLeading leading (Spec.groupedConvSpec groups layer.kernel layer.bias) input).flattenSpec

The CROWN convolution matrix and broadcast bias compute the flattened real convolution.

The statement includes grouped channels, dilation, asymmetric zero padding, and any leading batch shape. It is an equality of the total mathematical definitions; graph execution additionally validates the convolution configuration. It makes no floating-point reduction-order claim.