Soundness of the directed node dispatcher #
Every successful branch restores the objective removed at the frontier. Missing data and unsupported active transfers retain the engine's failure behavior.
theorem
NN.MLTheory.CROWN.Graph.DirectedBackward.backwardNode_preserves
{α : Type}
[TorchLean.Storage α]
[Context α]
[BoundOps α]
[LawfulBoundOps α]
{nodes : Array Node}
{ps : ParamStore α}
{ibp : Array (Option (FlatBox α))}
{ctx : AffineCtx}
{dims : ℕ → ℕ}
{v : ℕ → ℕ → ℝ}
(point : GraphPoint nodes ps ibp ctx dims v)
(k : ℕ)
(hk : k < nodes.size)
(st : Internal.DirectedBackwardState α)
(z : ℝ)
(hinv : SweepInvariant dims v ctx.inputId nodes.size (k + 1) z st)
:
SweepInvariant dims v ctx.inputId nodes.size k z (Internal.directedBackwardNode nodes ps ibp ctx st k)
Every executable directed node preserves the sweep invariant for a real graph point.