Arithmetic of the rounded backward sweep

The backward engine stores intervals for coefficients and for its accumulated constant. These lemmas interpret the engine's operations over the reals. Ordinary backend addition, subtraction, and multiplication need not be exact.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.foldl_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {ι : Type} (indices : List ι) (lo hi : ι → α) (f : ι → ℝ) (initialLo initialHi : α) (initial : ℝ) (hlo : LawfulBoundOps.toReal initialLo ≤ initial) (hhi : initial ≤ LawfulBoundOps.toReal initialHi) (hterms : ∀ i ∈ indices, LawfulBoundOps.toReal (lo i) ≤ f i ∧ f i ≤ LawfulBoundOps.toReal (hi i)) : LawfulBoundOps.toReal (List.foldl (fun (acc : α) (i : ι) => BoundOps.addDown acc (lo i)) initialLo indices) ≤ initial + (List.map f indices).sum ∧ initial + (List.map f indices).sum ≤ LawfulBoundOps.toReal (List.foldl (fun (acc : α) (i : ι) => BoundOps.addUp acc (hi i)) initialHi indices)

Directed accumulation encloses the mathematical sum, including a nonzero initial constant.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.coeffAffine_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {l u al au : α} {x a : ℝ} (hl : LawfulBoundOps.toReal l ≤ x) (hu : x ≤ LawfulBoundOps.toReal u) (hal : LawfulBoundOps.toReal al ≤ a) (hau : a ≤ LawfulBoundOps.toReal au) : LawfulBoundOps.toReal (Internal.directedCoeffAffine l u al au).1.1 * x + LawfulBoundOps.toReal (Internal.directedCoeffAffine l u al au).1.2 ≤ a * x ∧ a * x ≤ LawfulBoundOps.toReal (Internal.directedCoeffAffine l u al au).2.1 * x + LawfulBoundOps.toReal (Internal.directedCoeffAffine l u al au).2.2

A selected slope and its directed correction bound every coefficient and input in their boxes.

For a box crossing zero, the correction uses the negative input endpoint. Its multiplication reverses the inequality for the coefficient width, hence the opposite direction on subtraction.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.sum_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {n : ℕ} (lo hi : Fin n → α) (f : Fin n → ℝ) (hterms : ∀ (i : Fin n), LawfulBoundOps.toReal (lo i) ≤ f i ∧ f i ≤ LawfulBoundOps.toReal (hi i)) : LawfulBoundOps.toReal (List.foldl (fun (acc : α) (i : Fin n) => BoundOps.addDown acc (lo i)) 0 (List.finRange n)) ≤ ∑ i : Fin n, f i ∧ ∑ i : Fin n, f i ≤ LawfulBoundOps.toReal (List.foldl (fun (acc : α) (i : Fin n) => BoundOps.addUp acc (hi i)) 0 (List.finRange n))

Directed summation over all coordinates encloses the finite real sum.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.dotBox_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {n : ℕ} (aLo aHi bLo bHi : TorchLean.Tensor α [n]) (a b : Fin n → ℝ) (ha : ∀ (i : Fin n), LawfulBoundOps.toReal (aLo.getScalar i) ≤ a i ∧ a i ≤ LawfulBoundOps.toReal (aHi.getScalar i)) (hb : ∀ (i : Fin n), LawfulBoundOps.toReal (bLo.getScalar i) ≤ b i ∧ b i ≤ LawfulBoundOps.toReal (bHi.getScalar i)) {lo hi : α} (hresult : Internal.directedDotBox { dim := n, lo := aLo, hi := aHi } { dim := n, lo := bLo, hi := bHi } = some (lo, hi)) : LawfulBoundOps.toReal lo ≤ ∑ i : Fin n, a i * b i ∧ ∑ i : Fin n, a i * b i ≤ LawfulBoundOps.toReal hi

The executable interval dot product encloses the dot product of any two enclosed vectors.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.linear_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {m n : ℕ} (aLo aHi : TorchLean.Tensor α [m]) (W : TorchLean.Tensor α [m, n]) (b : TorchLean.Tensor α [m]) (a : Fin m → ℝ) (ha : ∀ (i : Fin m), LawfulBoundOps.toReal (aLo.getScalar i) ≤ a i ∧ a i ≤ LawfulBoundOps.toReal (aHi.getScalar i)) {aX : FlatBox α} {cLo cHi : α} (hresult : Internal.directedBackwardLinear { dim := m, lo := aLo, hi := aHi } W b = some (aX, cLo, cHi)) : aX.dim = n ∧ (∀ (j : Fin n), LawfulBoundOps.toReal (Spec.getAtOrZero aX.lo [↑j]) ≤ ∑ i : Fin m, a i * LawfulBoundOps.toReal (Spec.get2 W i j) ∧ ∑ i : Fin m, a i * LawfulBoundOps.toReal (Spec.get2 W i j) ≤ LawfulBoundOps.toReal (Spec.getAtOrZero aX.hi [↑j])) ∧ LawfulBoundOps.toReal cLo ≤ ∑ i : Fin m, a i * LawfulBoundOps.toReal (b.getScalar i) ∧ ∑ i : Fin m, a i * LawfulBoundOps.toReal (b.getScalar i) ≤ LawfulBoundOps.toReal cHi

Each coefficient produced by the linear transfer encloses the exact transposed matrix product; its constant contribution encloses the exact bias dot product.

def NN.MLTheory.CROWN.Graph.DirectedBackward.affineValue {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {n : ℕ} (aff : AffineVec α n 1) (x : Fin n → ℝ) : ℝ

Interpret a scalar affine form using exact real addition and multiplication.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.inputAffines_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {n : ℕ} (xLo xHi aLo aHi : TorchLean.Tensor α [n]) (cLo cHi : α) (x a : Fin n → ℝ) (c : ℝ) (hx : ∀ (i : Fin n), LawfulBoundOps.toReal (xLo.getScalar i) ≤ x i ∧ x i ≤ LawfulBoundOps.toReal (xHi.getScalar i)) (ha : ∀ (i : Fin n), LawfulBoundOps.toReal (aLo.getScalar i) ≤ a i ∧ a i ≤ LawfulBoundOps.toReal (aHi.getScalar i)) (hc : LawfulBoundOps.toReal cLo ≤ c ∧ c ≤ LawfulBoundOps.toReal cHi) {lower upper : AffineVec α n 1} (hresult : Internal.directedInputAffines n { dim := n, lo := xLo, hi := xHi } { dim := n, lo := aLo, hi := aHi } cLo cHi = some (lower, upper)) : affineValue lower x ≤ ∑ i : Fin n, a i * x i + c ∧ ∑ i : Fin n, a i * x i + c ≤ affineValue upper x

The engine's final affine conversion encloses every objective represented by its input coefficient intervals and accumulated constant.