Enclosure by the directed convolution folds

The executable convolution transfer bounds each signed product and accumulates those bounds in the same channel/kernel order as groupedConvSpec. These theorems establish its enclosure over the exact real BoundOps instance, including padding, grouped channels, dilation, and arbitrary leading batch dimensions. The affine corollary uses the existing convolution matrix equality; the transfer itself continues to use its spatial folds.

theorem NN.MLTheory.CROWN.ConvProof.contains_iff_apply {s : Spec.Shape} (box : Box ℝ s) (input : TorchLean.Tensor ℝ s) : box.contains input ↔ ∀ (coordinate : s.Coord), TorchLean.Tensor.Internal.Rep.get box.lo coordinate ≤ TorchLean.Tensor.Internal.Rep.get input coordinate ∧ TorchLean.Tensor.Internal.Rep.get input coordinate ≤ TorchLean.Tensor.Internal.Rep.get box.hi coordinate

theorem NN.MLTheory.CROWN.ConvProof.box_contains_flatten_iff {s : Spec.Shape} (box : Box ℝ s) (input : TorchLean.Tensor ℝ s) : (flattenBox box).contains input.flattenSpec ↔ box.contains input

Flattening preserves and reflects every component inequality of a real tensor box.

theorem NN.MLTheory.CROWN.ConvProof.contains_iff_multiIndex (dims : List ℕ) (box : Box ℝ (Spec.Shape.ofList dims)) (input : TorchLean.Tensor ℝ (Spec.Shape.ofList dims)) : box.contains input ↔ ∀ (index : Spec.Conv.Internal.MultiIndex dims), Spec.Conv.Internal.MultiIndex.get box.lo index ≤ Spec.Conv.Internal.MultiIndex.get input index ∧ Spec.Conv.Internal.MultiIndex.get input index ≤ Spec.Conv.Internal.MultiIndex.get box.hi index

theorem NN.MLTheory.CROWN.ConvProof.contains_getAtOrZero {dims : List ℕ} {box : Box ℝ (Spec.Shape.ofList dims)} {input : TorchLean.Tensor ℝ (Spec.Shape.ofList dims)} (h : box.contains input) (indices : List ℕ) : Spec.getAtOrZero box.lo indices ≤ Spec.getAtOrZero input indices ∧ Spec.getAtOrZero input indices ≤ Spec.getAtOrZero box.hi indices

theorem NN.MLTheory.CROWN.ConvProof.foldlIndices_rel {A B : Type} (relation : A → B → Prop) (dims : List ℕ) {left : A → List ℕ → A} {right : B → List ℕ → B} (step : ∀ (a : A) (b : B) (i : List ℕ), relation a b → relation (left a i) (right b i)) {a : A} {b : B} (initial : relation a b) : relation (Spec.Conv.Internal.foldlIndices dims a left) (Spec.Conv.Internal.foldlIndices dims b right)

The spatial iterator preserves a binary relation independently of rank and empty extents.

theorem NN.MLTheory.CROWN.ConvProof.ibpConv_contains_groupedConv_real {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) (box : Box ℝ (leading.concat (Spec.Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList)))) (input : TorchLean.Tensor ℝ (leading.concat (Spec.Shape.ofList (inC :: (TorchLean.Tensor.Internal.Rep.data inSpatial).toList)))) (h : box.contains input) : (ibpConv layer dilation paddingAfter groups leading box).contains (TorchLean.Tensor.mapLeading leading (Spec.groupedConvSpec groups layer.kernel layer.bias) input)

The actual directed convolution transfer encloses the grouped convolution specification over the reals, independently in every leading batch.