Directed enclosure through shape-erased coordinate operations

The runtime implements permutations by adjacent swaps. Each swap reads one input coordinate, so the same enclosure proof applies to every accepted permutation, including empty tensors.

inductive NN.MLTheory.CROWN.Graph.DirectedBackward.SomeTensorEncloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] : Spec.SomeTensor α → Spec.SomeTensor α → Spec.SomeTensor ℝ → Prop

Shape-erased endpoint tensors have the same shape as an enclosed exact real tensor.

• mk {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s : Spec.Shape} {lo hi : TorchLean.Tensor α s} {x : TorchLean.Tensor ℝ s} (bounds : TensorEncloses lo hi x) : SomeTensorEncloses { shape := s, tensor := lo } { shape := s, tensor := hi } { shape := s, tensor := x }

def NN.MLTheory.CROWN.Graph.DirectedBackward.TensorTransferEncloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (op : Spec.SomeTensor α → Except String (Spec.SomeTensor α)) (exactOp : Spec.SomeTensor ℝ → Except String (Spec.SomeTensor ℝ)) : Prop

Successful endpoint and real evaluations preserve shape and coordinate enclosure.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.TensorEncloses.swapAdjacentAxes {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s : Spec.Shape} {lo hi : TorchLean.Tensor α s} {x : TorchLean.Tensor ℝ s} (h : TensorEncloses lo hi x) (depth : ℕ) : TensorEncloses (lo.swapAdjacentAxes depth) (hi.swapAdjacentAxes depth) (x.swapAdjacentAxes depth)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.SomeTensorEncloses.swapAdjacentAtDepth {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {lo hi : Spec.SomeTensor α} {x : Spec.SomeTensor ℝ} (h : SomeTensorEncloses lo hi x) (depth : ℕ) : SomeTensorEncloses (lo.swapAdjacentAtDepth depth) (hi.swapAdjacentAtDepth depth) (x.swapAdjacentAtDepth depth)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.SomeTensorEncloses.swapFold {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {lo hi : Spec.SomeTensor α} {x : Spec.SomeTensor ℝ} (h : SomeTensorEncloses lo hi x) (depths : List ℕ) : SomeTensorEncloses (List.foldl Spec.SomeTensor.swapAdjacentAtDepth lo depths) (List.foldl Spec.SomeTensor.swapAdjacentAtDepth hi depths) (List.foldl Spec.SomeTensor.swapAdjacentAtDepth x depths)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.permuteSomeTensor_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (perm : Array ℕ) : TensorTransferEncloses (fun (x : Spec.SomeTensor α) => IR.Graph.permuteSomeTensor x perm) fun (x : Spec.SomeTensor ℝ) => IR.Graph.permuteSomeTensor x perm

The checked permutation evaluator applies the same swaps to all three tensors.

def NN.MLTheory.CROWN.Graph.DirectedBackward.transposeTensor (axis₁ axis₂ : ℕ) {β : Type} [TorchLean.Storage β] [Context β] (x : Spec.SomeTensor β) : Except String (Spec.SomeTensor β)

Exact transpose uses the runtime's validated transposition permutation.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.transposeTensor_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (axis₁ axis₂ : ℕ) : TensorTransferEncloses (transposeTensor axis₁ axis₂) (transposeTensor axis₁ axis₂)

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.ibpMonotoneSomeTensor?_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {s t : Spec.Shape} {B box : FlatBox α} {f : ℕ → ℝ} {y : TorchLean.Tensor ℝ t} {op : Spec.SomeTensor α → Except String (Spec.SomeTensor α)} {exactOp : Spec.SomeTensor ℝ → Except String (Spec.SomeTensor ℝ)} (hop : TensorTransferEncloses op exactOp) (hB : RowEncloses B s.size f) (hy : exactOp { shape := s, tensor := realTensor s f } = Except.ok { shape := t, tensor := y }) (hbox : ibpMonotoneSomeTensor? s t op B = some box) : RowEncloses box t.size (tensorValues y)

Applying an enclosing shape-erased transfer to endpoint tensors encloses its exact result.