Rounded forward IBP for structural operations

The equations below use exact tensor operations on the real parent coordinates. The family predicate selects operation kinds; the executable transfers retain their full shape, axis, window, and arithmetic guards.

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

The structural, axis-reduction, and pooling operation family, at every configuration.

def NN.MLTheory.CROWN.Graph.DirectedBackward.ShapedUnaryRealEquation (nodes : Array Node) (node : Node) (dims : ℕ → ℕ) (v : ℕ → ℕ → ℝ) (id : ℕ) (op : Spec.SomeTensor ℝ → Except String (Spec.SomeTensor ℝ)) : Prop

A unary tensor evaluator acts on the real parent and returns the declared real output.

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

Exact real equations for this family. Broadcast and reduction use the output shape actually computed by their transfers; concat uses the checked occurrence-wise layout. No equation mentions interval endpoints or assumes enclosure of the output.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.ibpStepNodeAt?_structural_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] [LawfulNonlinearBoundOps α] {nodes : Array Node} {ps : ParamStore α} {boxes ibp : Array (Option (FlatBox α))} {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {id : ℕ} (hsupported : ibpStructuralSupportedNode nodes[id]! = true) (heq : StructuralRealNodeEquation 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)

One structural IBP step encloses its exact real value whenever the parent boxes enclose their real values. The parent agreement interface is the same as for the basic forward step theorem. All executable guards remain in hstep, including empty-axis and finite-arithmetic checks.