Rounded matrix and convolution enclosures

The endpoint computations use directed products and sums. Their real targets retain the runtime's coordinate maps, including batch broadcasting, vector promotion, and zero padding.

def NN.MLTheory.CROWN.Graph.DirectedBackward.pointVector (n : ℕ) (f : ℕ → ℝ) : TorchLean.Tensor ℝ [n]

The real vector described by a graph point's coordinate function.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.rowEncloses_read {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {box : FlatBox α} {n : ℕ} {f : ℕ → ℝ} (h : RowEncloses box n f) (i : ℕ) : LawfulBoundOps.toReal (Spec.getAtOrZero box.lo [i]) ≤ Spec.getAtOrZero (pointVector n f) [i] ∧ Spec.getAtOrZero (pointVector n f) [i] ≤ LawfulBoundOps.toReal (Spec.getAtOrZero box.hi [i])

An enclosed vector remains enclosed when reads outside its shape return zero.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.orderedSum_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {ι : Type} (indices : List ι) (bounds : ι → α × α) (f : ι → ℝ) (h : ∀ (i : ι), LawfulBoundOps.toReal (bounds i).1 ≤ f i ∧ f i ≤ LawfulBoundOps.toReal (bounds i).2) (acc : α × α) (total : ℝ) (hacc : LawfulBoundOps.toReal acc.1 ≤ total ∧ total ≤ LawfulBoundOps.toReal acc.2) : LawfulBoundOps.toReal (List.foldl (fun (a : α × α) (i : ι) => (BoundOps.addDown a.1 (bounds i).1, BoundOps.addUp a.2 (bounds i).2)) acc indices).1 ≤ List.foldl (fun (a : ℝ) (i : ι) => a + f i) total indices ∧ List.foldl (fun (a : ℝ) (i : ι) => a + f i) total indices ≤ LawfulBoundOps.toReal (List.foldl (fun (a : α × α) (i : ι) => (BoundOps.addDown a.1 (bounds i).1, BoundOps.addUp a.2 (bounds i).2)) acc indices).2

Directed accumulation bounds a real sum in the same list order.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.binaryMatmulBox_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (layout : IR.OpContracts.MatmulDims) {left right : FlatBox α} {n m : ℕ} {x y : ℕ → ℝ} (hx : RowEncloses left n x) (hy : RowEncloses right m y) : RowEncloses (binaryMatmulBox layout left right) layout.outShape.size fun (i : ℕ) => Spec.getAtOrZero (IR.Graph.matmulFlat layout (pointVector n x) (pointVector m y)) [i]

The actual rounded contraction encloses the real matrix product with the same index maps.

def NN.MLTheory.CROWN.Graph.DirectedBackward.BinaryMatmulNodeEquation (nodes : Array Node) (dims : ℕ → ℕ) (v : ℕ → ℕ → ℝ) (id : ℕ) : Prop

The binary product's real equation uses the same validated contraction layout.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.ibpStep_matmul_parents {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] {nodes : Array Node} {ps : ParamStore α} {boxes : Array (Option (FlatBox α))} {id : ℕ} {box : FlatBox α} (hkind : nodes[id]!.kind = IR.OpKind.matmul) (hstep : ibpStepNodeAt? nodes ps boxes id nodes[id]! = some box) : nodes[id]!.parents.size = 1 ∨ ∃ (p : ℕ) (q : ℕ), nodes[id]!.parents = #[p, q]

A successful matrix product has either one stored-weight parent or two tensor parents.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.ibpStep_binaryMatmul_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] {nodes : Array Node} {ps : ParamStore α} {boxes : Array (Option (FlatBox α))} {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {id p q : ℕ} (hkind : nodes[id]!.kind = IR.OpKind.matmul) (hparents : nodes[id]!.parents = #[p, q]) (heq : BinaryMatmulNodeEquation nodes dims v id) (hget : ∀ p ∈ nodes[id]!.parents, ∀ (B : FlatBox α), boxes[p]?.join = some B → RowEncloses B (dims p) (v p)) {box : FlatBox α} (hstep : ibpStepNodeAt? nodes ps boxes id nodes[id]! = some box) : RowEncloses box (dims id) (v id)

A successful two-parent matrix product encloses its real contraction.

def NN.MLTheory.CROWN.Graph.DirectedBackward.realBox {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s : Spec.Shape} (box : Box α s) : Box ℝ s

Interpret a shaped endpoint box without changing its coordinates.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.getAtOrZero_map_value {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s : Spec.Shape} (tensor : TorchLean.Tensor α s) (indices : List ℕ) : Spec.getAtOrZero (TorchLean.Tensor.map LawfulBoundOps.toReal tensor) indices = LawfulBoundOps.toReal (Spec.getAtOrZero tensor indices)

Interpretation commutes with total indexing, including the zero-padding branch.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.multiIndex_get_map_value {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {dims : List ℕ} (tensor : TorchLean.Tensor α (Spec.Shape.ofList dims)) (index : Spec.Conv.Internal.MultiIndex dims) : Spec.Conv.Internal.MultiIndex.get (TorchLean.Tensor.map LawfulBoundOps.toReal tensor) index = LawfulBoundOps.toReal (Spec.Conv.Internal.MultiIndex.get tensor index)

Interpretation commutes with the checked indices used by spatial convolution.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.ibpConv_contains_groupedConv {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {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 : (realBox box).contains input) : (realBox (ibpConv layer dilation paddingAfter groups leading box)).contains (TorchLean.Tensor.mapLeading leading (Spec.groupedConvSpec groups (TorchLean.Tensor.map LawfulBoundOps.toReal layer.kernel) (TorchLean.Tensor.map LawfulBoundOps.toReal layer.bias)) input)

The directed spatial folds enclose exact grouped convolution of the interpreted parameters, with arbitrary dilation, padding, channel groups and leading batch dimensions.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.realBox_flattenBox {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s : Spec.Shape} (box : Box α s) : realBox (flattenBox box) = flattenBox (realBox box)

Interpreting endpoints commutes with flattening a shaped box.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.rowEncloses_flatten {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s : Spec.Shape} {box : Box α s} {input : TorchLean.Tensor ℝ s} (h : (realBox box).contains input) : RowEncloses { dim := s.size, lo := box.lo.flattenSpec, hi := box.hi.flattenSpec } s.size fun (i : ℕ) => Spec.getAtOrZero input.flattenSpec [i]

A shaped enclosure gives the corresponding row enclosure after flattening.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.realBox_contains_ibpUnflatten {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s : Spec.Shape} {box : FlatBox α} {n : ℕ} {f : ℕ → ℝ} (hdim : box.dim = s.size) (hn : n = s.size) (h : RowEncloses box n f) : (realBox { lo := ibpUnflatten box.dim box.lo hdim, hi := ibpUnflatten box.dim box.hi hdim }).contains (TorchLean.Tensor.unflattenSpec s (pointVector s.size f))

A flat graph enclosure gives a shaped enclosure after the checked reshape.

noncomputable def NN.MLTheory.CROWN.Graph.DirectedBackward.convolutionPoint {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (parameters : IR.ConvParams α) (leading : Spec.Shape) (f : ℕ → ℝ) : TorchLean.Tensor ℝ [(parameters.output leading).size]

The real grouped convolution determined by a stored payload.

def NN.MLTheory.CROWN.Graph.DirectedBackward.ConvolutionNodeEquation {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (nodes : Array Node) (ps : ParamStore α) (dims : ℕ → ℕ) (v : ℕ → ℕ → ℝ) (id : ℕ) (configuration : IR.ConvConfig) : Prop

The graph's convolution equation states its spatial real semantics.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.ibpStep_convolution_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] {nodes : Array Node} {ps : ParamStore α} {boxes : Array (Option (FlatBox α))} {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {id : ℕ} {configuration : IR.ConvConfig} (hkind : nodes[id]!.kind = IR.OpKind.conv configuration) (heq : ConvolutionNodeEquation nodes ps dims v id configuration) (hget : ∀ p ∈ nodes[id]!.parents, ∀ (B : FlatBox α), boxes[p]?.join = some B → RowEncloses B (dims p) (v p)) {box : FlatBox α} (hstep : ibpStepNodeAt? nodes ps boxes id nodes[id]! = some box) : RowEncloses box (dims id) (v id)

A successful graph convolution encloses the real grouped convolution at that node.