Rounded forward soundness for every graph operation

RealNodeEquation describes the real operation at each node. Tensor operations use their actual coordinate maps, reductions, normalization formulas, and interpreted stored parameters. Random nodes use the seeded real Spec operations. Full-tensor sum equations hold independently of IBP row availability.

runIBP_encloses_all proves enclosure for every successful entry of the executable pass. It has no operation-family restriction and assumes no enclosure for intermediate nodes. Invalid shapes, missing parameters, and unavailable arithmetic transfers can still return none.

def NN.MLTheory.CROWN.Graph.DirectedBackward.RealNodeEquation {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (nodes : Array Node) (ps : ParamStore α) (ibp : Array (Option (FlatBox α))) (dims : ℕ → ℕ) (v : ℕ → ℕ → ℝ) (id : ℕ) : Prop

The real semantics of every graph operation.

The spatial convolution and structural equations stand on their own. In particular, they do not assume a second affine equation about coefficients computed by the verifier. Unary stored-weight and binary tensor matrix multiplication share an operation tag; their parent counts distinguish the two equations. Stored linear nodes use vector affine equations; the public IR bridge for linear requires vector-shaped parents.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.ibpStepNodeAt?_all_encloses {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] [LawfulNonlinearBoundOps α] [LawfulMinBoundOps α] (hepsilon : 0 ≤ LawfulBoundOps.toReal TorchLean.normalizationEpsilon) {nodes : Array Node} {ps : ParamStore α} {boxes ibp : Array (Option (FlatBox α))} {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} {id : ℕ} (hinput : nodes[id]!.kind = IR.OpKind.input → ∀ (box : FlatBox α), ps.inputBoxes[id]? = some box → RowEncloses box (dims id) (v id)) (heq : RealNodeEquation nodes ps ibp 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)

Every successful IBP transfer encloses the corresponding real operation.

The epsilon premise concerns the backend's fixed default normalization constant. Stored normalization payloads retain the executable positivity checks on their own epsilon.

theorem NN.MLTheory.CROWN.Graph.DirectedBackward.runIBP_encloses_all {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] [LawfulNonlinearBoundOps α] [LawfulMinBoundOps α] (g : Graph) (ps : ParamStore α) (hepsilon : 0 ≤ LawfulBoundOps.toReal TorchLean.normalizationEpsilon) {dims : ℕ → ℕ} {v : ℕ → ℕ → ℝ} (hparent : ∀ id < g.nodes.size, ∀ p ∈ g.nodes[id]!.parents, p < id) (hinputs : InputsInBoxes g.nodes ps dims v) (hequation : ∀ id < g.nodes.size, RealNodeEquation g.nodes ps (g.runIBP ps) dims v id) (id : ℕ) : id < g.nodes.size → ∀ (box : FlatBox α), (g.runIBP ps)[id]! = some box → RowEncloses box (dims id) (v id)

The complete rounded forward pass encloses every real node value for which it returns a box.

Inputs lie in their seeded boxes, parents precede consumers, and nodes obey their actual real equations. The proof supplies all intermediate enclosures by induction, including convolution, binary matrix multiplication, structural operations, normalization, and random realizations.