Soundness of the rounded backward objective

The executable reverse sweep encloses its output objective at every real graph point satisfying the stored-parameter equations and enclosed by the forward IBP boxes. Those boxes are assumed, not derived from the rounded forward pass. The proof includes coefficient rounding, repeated-parent accumulation, bias rounding, node discharge, and the crossing-zero correction used when converting the input coefficient intervals to affine bounds.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.runDirectedBackwardObjective_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) (obj : FlatTensor α) (hdim : obj.n = dims output) {lower upper : AffineVec α ctx.inputDim 1} (hresult : Internal.runDirectedBackwardObjective g ps ctx ibp output obj = some (lower, upper)) : (affineValue lower fun (i : Fin ctx.inputDim) => v ctx.inputId ↑i) ≤ dot (dims output) (fun (i : ℕ) => LawfulBoundOps.toReal (Spec.getAtOrZero obj.v [i])) (v output) ∧ dot (dims output) (fun (i : ℕ) => LawfulBoundOps.toReal (Spec.getAtOrZero obj.v [i])) (v output) ≤ affineValue upper fun (i : Fin ctx.inputDim) => v ctx.inputId ↑i

A successful rounded backward sweep returns affine bounds on the exact real output objective. The hypotheses specify real node equations, directed scalar laws, and sound forward IBP boxes, never local soundness of the verifier's backward steps.