Real graph equations for directed backward CROWN

The rounded verifier targets the real graph described by its stored scalars. The equations here mention node values, parameter values, and coordinate maps. They impose no condition on the verifier's coefficient arithmetic or its returned bounds.

Nodes discharged through IBP need only their given value enclosure. Direct affine and structural rules use their ordinary real equations. Connecting those equations to a separately scheduled floating-point model evaluation additionally requires a rounding-error argument for that runtime.

The core backward theorems take a GraphPoint, whose ibp_encloses field states that each forward box encloses the real node value. GraphPoint.ofRunIBPAll in DirectedIBPFullBackward derives this field from input enclosures and RealNodeEquation for every graph operation, including spatial convolution, structural tensor operations, normalization, and random realizations. It uses the complete forward theorem runIBP_encloses_all and the backend's directed arithmetic laws. The original GraphPoint.ofRunIBP remains available for the core operation family selected by ibpForwardSupported.

def NN.MLTheory.CROWN.Graph.DirectedBackward.LinearEquation {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (dims : ℕ → ℕ) (v : ℕ → ℕ → ℝ) (id pid : ℕ) {m n : ℕ} (W : TorchLean.Tensor α [m, n]) (b : TorchLean.Tensor α [m]) : Prop

The shape and coordinate equations of a stored affine node.

def NN.MLTheory.CROWN.Graph.DirectedBackward.CopyEquation (dims : ℕ → ℕ) (v : ℕ → ℕ → ℝ) (id pid : ℕ) : Prop

The shape and coordinate equations of a value-preserving unary node.

def NN.MLTheory.CROWN.Graph.DirectedBackward.UnaryEquation (dims : ℕ → ℕ) (v : ℕ → ℕ → ℝ) (id pid : ℕ) (f : ℝ → ℝ) : Prop

The shape and coordinate equations of a pointwise unary node computing f.

def NN.MLTheory.CROWN.Graph.DirectedBackward.BinaryEquation (dims : ℕ → ℕ) (v : ℕ → ℕ → ℝ) (id p q : ℕ) (f : ℝ → ℝ → ℝ) : Prop

The shape and coordinate equations of a pointwise binary node computing f.

def NN.MLTheory.CROWN.Graph.DirectedBackward.PermutationEquation (dims : ℕ → ℕ) (v : ℕ → ℕ → ℝ) (id pid : ℕ) (outputShape : Spec.Shape) (forwardPerm : Array ℕ) : Prop

The inverse coordinate map identifies every output coordinate with its source coordinate.

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

Real coordinate equations for a node, using the same successful parameter/layout lookups as the executable dispatcher. Failed lookups require no equation because they reject the sweep. Pointwise nonlinear nodes state their real function. Inputs, random nodes, and the operations with a layout or reduction semantics not written here (pools, broadcasts, axis reductions, BatchNorm, LayerNorm, softmax, mseLoss, safeLog) get True.

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

A topologically ordered real graph point with enclosed IBP values. Each direct node rule satisfies its ordinary coordinate equation; all other active nodes may use their IBP enclosure. GraphPoint.ofRunIBP builds one from a rounded runIBP pass on supported graphs.

• input_lt : ctx.inputId < nodes.size

  The designated input exists in the graph.

• input_dim : dims ctx.inputId = ctx.inputDim

  Its width agrees with the affine interface.

• input_kind : nodes[ctx.inputId]!.kind = IR.OpKind.input

  The designated input is an input node.

• node_id (id : ℕ) : id < nodes.size → nodes[id]!.id = id

  Stored node identifiers agree with their array positions.

• parent_lt (id : ℕ) : id < nodes.size → ∀ p ∈ nodes[id]!.parents, p < id

  Every parent precedes its consumer. Repeated parents are allowed.

• ibp_encloses (id : ℕ) : id < nodes.size → ∀ (box : FlatBox α), ibp[id]! = some box → RowEncloses box (dims id) (v id)

  Every available interval encloses the corresponding real node value.

• equation (id : ℕ) : id < nodes.size → NodeEquation nodes ps ibp dims v id

  Directly propagated nodes obey their real coordinate equations.