Rounded IBP for pointwise operations and mean squared error

The scalar softplus and safeLog laws follow from the existing directed arithmetic and nonlinear contracts. Box transfers preserve coordinate enclosures, and mean squared error uses the directed sum and count folds to divide by the exact number of coordinates.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.softplusBounds_enclosure {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] : UnaryEnclosure (fun (x : ℝ) => Real.log (1 + Real.exp x)) NonlinearBoundOps.softplusBounds

The coarse softplus interval encloses log (1 + exp x) using only directed addition.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.safeLogBounds_enclosure {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] [LawfulNonlinearBoundOps α] : BinaryEnclosure (fun (x epsilon : ℝ) => Real.log (Real.log (1 + Real.exp x) + epsilon)) NonlinearBoundOps.safeLogBounds

Both safeLog paths enclose log (softplus x + epsilon), including its varying epsilon.

The executable positivity check supplies the logarithm's domain. If the logarithm transfer declines, directed reciprocal bounds give 1 - 1/z ≤ log z ≤ z - 1.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.directed_abs_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {lo hi : α} {x : ℝ} (hlo : LawfulBoundOps.toReal lo ≤ x) (hhi : x ≤ LawfulBoundOps.toReal hi) : LawfulBoundOps.toReal (if lo < 0 then if 0 < hi then 0 else BoundOps.subDown 0 hi else lo) ≤ |x| ∧ |x| ≤ LawfulBoundOps.toReal (BoundOps.max2 (BoundOps.subUp 0 lo) hi)

Directed negation encloses absolute value without assuming that ordinary abs is exact.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.boxAbs_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {x : FlatBox α} {n : ℕ} {f : ℕ → ℝ} (hx : RowEncloses x n f) : RowEncloses (boxAbs x) n fun (i : ℕ) => |f i|

The directed absolute-value box encloses the absolute value of every coordinate.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.boxSafeLog?_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] [LawfulNonlinearBoundOps α] {x epsilon box : FlatBox α} {n : ℕ} {f e : ℕ → ℝ} (hx : RowEncloses x n f) (he : RowEncloses epsilon 1 e) (hbox : boxSafeLog? x epsilon = some box) : RowEncloses box n fun (i : ℕ) => Real.log (Real.log (1 + Real.exp (f i)) + e 0)

SafeLog uses the same enclosed scalar epsilon at every input coordinate.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.boxMaxElem_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {x y : FlatBox α} {n : ℕ} {f g : ℕ → ℝ} (hx : RowEncloses x n f) (hy : RowEncloses y n g) : RowEncloses (boxMaxElem x y) n fun (i : ℕ) => max (f i) (g i)

Componentwise maximum preserves enclosure in both operands.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.boxMinElem_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [LawfulMinBoundOps α] {x y : FlatBox α} {n : ℕ} {f g : ℕ → ℝ} (hx : RowEncloses x n f) (hy : RowEncloses y n g) : RowEncloses (boxMinElem x y) n fun (i : ℕ) => min (f i) (g i)

Componentwise minimum preserves enclosure in both operands.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.boxSquare_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {x : FlatBox α} {n : ℕ} {f : ℕ → ℝ} (hx : RowEncloses x n f) : RowEncloses (boxSquare x) n fun (i : ℕ) => f i ^ 2

Squaring uses directed endpoint products, with zero as a lower bound across zero.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.boxMean?_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] [LawfulNonlinearBoundOps α] {x box : FlatBox α} {n : ℕ} {f g : ℕ → ℝ} (hx : RowEncloses x n f) (hg : g 0 = (∑ i : Fin n, f ↑i) / ↑n) (hbox : boxMean? x = some box) : RowEncloses box 1 g

A successful mean transfer divides the enclosed sum by the exact coordinate count.

def NN.MLTheory.CROWN.Graph.DirectedBackward.ibpPointwiseSupportedNode (node : Node) : Bool

Node kinds handled by the remaining pointwise IBP transfers.

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

Real semantics missing from NodeEquation for this family.

SafeLog is log (log (1 + exp x) + epsilon) with one scalar epsilon parent. MSE is the exact mean of squared differences; a zero-length mean cannot yield a successful IBP transfer. Random values are the actual seeded real Spec tensors. Uniform nodes have no parents. A mask has one existing scalar parent whose value is the keep probability. These requirements are explicit because the coarse random IBP transfer does not reject malformed parent lists. Other kinds use True here and retain their existing NodeEquation.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.ibpStepNodeAt?_pointwise_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] [LawfulNonlinearBoundOps α] [LawfulMinBoundOps α] {nodes : Array Node} {ps : ParamStore α} {boxes ibp : Array (Option (FlatBox α))} {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {id : ℕ} (hsupported : ibpPointwiseSupportedNode nodes[id]! = true) (heq : NodeEquation nodes ps ibp dims v id) (hpointwise : PointwiseRealNodeEquation nodes dims v id) (hagree : ∀ p ∈ nodes[id]!.parents, boxes[p]?.join = ibp[p]!) (henc : ∀ p ∈ nodes[id]!.parents, ∀ (box : FlatBox α), ibp[p]! = some box → RowEncloses box (dims p) (v p)) {box : FlatBox α} (hstep : ibpStepNodeAt? nodes ps boxes id nodes[id]! = some box) : RowEncloses box (dims id) (v id)

A successful pointwise IBP step encloses the node's real value.

Parent boxes use the same agreement and enclosure interface as the basic step theorem. The existing NodeEquation supplies abs, min, max, and softplus semantics; safeLog, MSE, and seeded random operations use the supplemental real equations. Random support follows from the source.