Soundness of the executable directed transfers

These lemmas connect the interval kernels with the exact objective at a sweep frontier. All scalar operations in the coefficient and constant accumulators are the engine's directed operations; the real identities describe the graph computed by the stored parameters.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.dotBox_row_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {n : ℕ} {aB xB : FlatBox α} {a x : ℕ → ℝ} (ha : RowEncloses aB n a) (hx : RowEncloses xB n x) {lo hi : α} (hresult : Internal.directedDotBox aB xB = some (lo, hi)) : LawfulBoundOps.toReal lo ≤ dot n a x ∧ dot n a x ≤ LawfulBoundOps.toReal hi

A flat interval inner product encloses the ordinary real inner product.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.represents_consume {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {input k n : ℕ} {st : Internal.DirectedBackwardState α} {z : ℝ} (h : Represents dims v input k st z) {aB xB : FlatBox α} {a x : ℕ → ℝ} (ha : RowEncloses aB n a) (hx : RowEncloses xB n x) : (Internal.consumeDirectedObjective st aB xB).failed = true ∨ Represents dims v input k (Internal.consumeDirectedObjective st aB xB) (z + dot n a x)

Discharging an enclosed node value either fails or adds its exact objective to the constant.

def NN.MLTheory.CROWN.Graph.DirectedBackward.transposedCoeff {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {m n : ℕ} (W : TorchLean.Tensor α [m, n]) (a : ℕ → ℝ) (j : ℕ) : ℝ

The exact coefficient produced by transposing a stored matrix.

def NN.MLTheory.CROWN.Graph.DirectedBackward.biasDot {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {m : ℕ} (b : TorchLean.Tensor α [m]) (a : ℕ → ℝ) : ℝ

The exact constant split off by a stored linear bias.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.linear_row_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {m n : ℕ} {aB : FlatBox α} (W : TorchLean.Tensor α [m, n]) (b : TorchLean.Tensor α [m]) {a : ℕ → ℝ} (ha : RowEncloses aB m a) {aX : FlatBox α} {lo hi : α} (hresult : Internal.directedBackwardLinear aB W b = some (aX, lo, hi)) : RowEncloses aX n (transposedCoeff W a) ∧ LawfulBoundOps.toReal lo ≤ biasDot b a ∧ biasDot b a ≤ LawfulBoundOps.toReal hi

The flat linear-transfer result encloses its transposed coefficient and bias contribution.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.dot_linear {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {m n : ℕ} (W : TorchLean.Tensor α [m, n]) (b : TorchLean.Tensor α [m]) (a x y : ℕ → ℝ) (hy : ∀ (i : Fin m), y ↑i = ∑ j : Fin n, LawfulBoundOps.toReal (Spec.get2 W i j) * x ↑j + LawfulBoundOps.toReal (b.getScalar i)) : dot m a y = dot n (transposedCoeff W a) x + biasDot b a

Reassociating a linear node is an exact real identity before interval approximation.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.represents_linear {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {input k m n : ℕ} {st : Internal.DirectedBackwardState α} {z : ℝ} (h : Represents dims v input k st z) (pid : ℕ) (hp : pid < st.coeffs.size) (hlive : pid ∈ pending input k) (hdim : dims pid = n) {aB : FlatBox α} {a y : ℕ → ℝ} (ha : RowEncloses aB m a) (W : TorchLean.Tensor α [m, n]) (b : TorchLean.Tensor α [m]) (hy : ∀ (i : Fin m), y ↑i = ∑ j : Fin n, LawfulBoundOps.toReal (Spec.get2 W i j) * v pid ↑j + LawfulBoundOps.toReal (b.getScalar i)) {aX : FlatBox α} {lo hi : α} (hresult : Internal.directedBackwardLinear aB W b = some (aX, lo, hi)) : Represents dims v input k (Internal.addDirectedConstant (Internal.addDirectedCoeff st pid aX) lo hi) (z + dot m a y) ∧ (Internal.addDirectedConstant (Internal.addDirectedCoeff st pid aX) lo hi).failed = st.failed ∧ (Internal.addDirectedConstant (Internal.addDirectedCoeff st pid aX) lo hi).coeffs.size = st.coeffs.size

A successful linear transfer preserves the represented objective and the coefficient table size, including accumulation into an already-active parent.