Rounded CROWN soundness from the complete forward pass

The actual real equations used by the full IBP proof also imply the equations used by the backward sweep. Convolution coefficients preserve the stored weights, and structural operations use the same checked coordinate maps in both directions.

GraphPoint.ofRunIBPAll derives every intermediate enclosure from the input boxes. The resulting CROWN theorems have no operation-family restriction and require no second equation for a node.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.RealNodeEquation.nodeEquation {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] {nodes : Array Node} {ps : ParamStore α} {ibp : Array (Option (FlatBox α))} {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {id : ℕ} (heq : RealNodeEquation nodes ps ibp dims v id) (hparents : ∀ p ∈ nodes[id]!.parents, p < nodes.size) (hdims : ∀ p ∈ nodes[id]!.parents, ∀ (box : FlatBox α), ibp[p]! = some box → box.dim = dims p) : NodeEquation nodes ps ibp dims v id

Real node semantics supplies each equation consumed by the backward sweep.

The legacy sum equation also records parent row widths. hdims supplies this shape fact; GraphPoint.ofRunIBPAll derives it from the completed forward pass.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.GraphPoint.ofRunIBPAll {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] [LawfulNonlinearBoundOps α] [LawfulMinBoundOps α] {g : Graph} {ps : ParamStore α} {ctx : AffineCtx} {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} (input_lt : ctx.inputId < g.nodes.size) (input_dim : dims ctx.inputId = ctx.inputDim) (input_kind : g.nodes[ctx.inputId]!.kind = IR.OpKind.input) (node_id : ∀ id < g.nodes.size, g.nodes[id]!.id = id) (parent_lt : ∀ id < g.nodes.size, ∀ p ∈ g.nodes[id]!.parents, p < id) (hepsilon : 0 ≤ LawfulBoundOps.toReal TorchLean.normalizationEpsilon) (hinputs : InputsInBoxes g.nodes ps dims v) (equation : ∀ id < g.nodes.size, RealNodeEquation g.nodes ps (g.runIBP ps) dims v id) : GraphPoint g.nodes ps (g.runIBP ps) ctx dims v

Build a backward graph point from input enclosures and the actual real node equations.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.runCROWNBackwardObjective_encloses_runIBP_all {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] [LawfulNonlinearBoundOps α] [LawfulMinBoundOps α] (hrounded : BoundOps.supportsExactAffineReassociation α = false) {g : Graph} {ps : ParamStore α} {ctx : AffineCtx} {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} (input_lt : ctx.inputId < g.nodes.size) (input_dim : dims ctx.inputId = ctx.inputDim) (input_kind : g.nodes[ctx.inputId]!.kind = IR.OpKind.input) (node_id : ∀ id < g.nodes.size, g.nodes[id]!.id = id) (parent_lt : ∀ id < g.nodes.size, ∀ p ∈ g.nodes[id]!.parents, p < id) (hepsilon : 0 ≤ LawfulBoundOps.toReal TorchLean.normalizationEpsilon) (hinputs : InputsInBoxes g.nodes ps dims v) (equation : ∀ id < g.nodes.size, RealNodeEquation g.nodes ps (g.runIBP ps) dims v id) (output : ℕ) (houtput : output < g.nodes.size) (obj : FlatTensor α) (hdim : obj.n = dims output) {bounds : FlatAffineBounds α} (hresult : g.runCROWNBackwardObjective ps ctx (g.runIBP ps) output obj = some bounds) : bounds.inDim = ctx.inputDim ∧ bounds.outDim = 1 ∧ AffineRowsEnclose bounds (v ctx.inputId) fun (x : ℕ) => dot (dims output) (fun (i : ℕ) => LawfulBoundOps.toReal (Spec.getAtOrZero obj.v [i])) (v output)

A successful rounded backward objective encloses the real objective after the full IBP pass. All intermediate enclosures follow from the input boxes and real node equations.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.directedNodeBounds_encloses_runIBP_all {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] [LawfulNonlinearBoundOps α] [LawfulMinBoundOps α] {g : Graph} {ps : ParamStore α} {ctx : AffineCtx} {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} (input_lt : ctx.inputId < g.nodes.size) (input_dim : dims ctx.inputId = ctx.inputDim) (input_kind : g.nodes[ctx.inputId]!.kind = IR.OpKind.input) (node_id : ∀ id < g.nodes.size, g.nodes[id]!.id = id) (parent_lt : ∀ id < g.nodes.size, ∀ p ∈ g.nodes[id]!.parents, p < id) (hepsilon : 0 ≤ LawfulBoundOps.toReal TorchLean.normalizationEpsilon) (hinputs : InputsInBoxes g.nodes ps dims v) (equation : ∀ id < g.nodes.size, RealNodeEquation g.nodes ps (g.runIBP ps) dims v id) (output : ℕ) (houtput : output < g.nodes.size) (hdim : dims output = g.nodes[output]!.outShape.size) {bounds : FlatAffineBounds α} (hresult : g.directedNodeBounds? ps ctx (g.runIBP ps) output = some bounds) : bounds.inDim = ctx.inputDim ∧ bounds.outDim = dims output ∧ AffineRowsEnclose bounds (v ctx.inputId) (v output)

Nodewise rounded CROWN bounds enclose the real output after the full forward pass.