Enclosure by the checked convolution node

The graph transfer validates the convolution geometry and reconstructs its shaped input from a flat interval. The tensor enclosure theorem then applies to the actual directed convolution folds. Flattening the result gives the same dimension-carrying enclosure used by graph certificates.

theorem NN.MLTheory.CROWN.Graph.CertSoundness.ibpConvNode_encloses_real {configuration : IR.ConvConfig} {parentShape outShape : Spec.Shape} {id : ℕ} {ps : ParamStore ℝ} {Xin Bout : FlatBox ℝ} {parameters : IR.ConvParams ℝ} {leading : Spec.Shape} (hparameters : ps.convCfg[id]? = some parameters) (hplan : planConvTransfer? configuration parameters parentShape outShape = some leading) (input : TorchLean.Tensor ℝ (parameters.input leading)) (hinput : EnclosesBox Xin { n := (parameters.input leading).size, v := input.flattenSpec }) (hout : ibpConvNode configuration parentShape outShape id ps Xin = some Bout) : EnclosesBox Bout { n := (parameters.output leading).size, v := (TorchLean.Tensor.mapLeading leading (Spec.groupedConvSpec parameters.groups parameters.spec.kernel parameters.spec.bias) input).flattenSpec }

A successful checked convolution transfer encloses the actual grouped/batched convolution of an enclosed shaped input. All geometry is the payload geometry accepted by the planner.