Nodewise rounded CROWN bounds #
Sequencing the coordinate objectives produces a lower and upper affine row for every output.
If any sweep fails, the returned constant rows retain the output's IBP enclosure. The forward IBP
boxes enter through GraphPoint.ibp_encloses; directedNodeBounds_encloses_runIBP discharges it
for the boxes of runIBP.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.boundsConst_encloses
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
(n : ℕ)
(box : FlatBox α)
(x y : ℕ → ℝ)
(hy : RowEncloses box box.dim y)
:
AffineRowsEnclose (boundsConst n box.dim box.lo box.hi) x y
A constant pair of affine maps retains an interval enclosure.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.directedNodeBounds_encloses
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
{g : Graph}
{ps : ParamStore α}
{ibp : Array (Option (FlatBox α))}
{ctx : AffineCtx}
{dims : ℕ → ℕ}
{v : ℕ → ℕ → ℝ}
(point : GraphPoint g.nodes ps ibp ctx dims v)
(output : ℕ)
(houtput : output < g.nodes.size)
(hdim : dims output = g.nodes[output]!.outShape.size)
{bounds : FlatAffineBounds α}
(hresult : g.directedNodeBounds? ps ctx ibp output = some bounds)
:
The nodewise public API returns real affine enclosures for every coordinate, provided the
forward IBP boxes in point are sound. Both the coordinate-sweep branch and the constant IBP
fallback are covered.