Input subdivision for graph bounds

Subdivision reduces dependency overestimation without changing layer transfer rules. Each split covers the entire parent box, including the shared boundary. Both children must produce bounds; otherwise the parent result is retained. Combining children takes their hull, never their intersection. That hull can then be intersected with the independently computed parent bound.

This is an optional, bounded-cost refinement for any supported graph, not a new soundness claim about the underlying scalar transfers. It cannot repair an unsound transfer or guarantee strict improvement for every layer. In particular, input-independent range fallbacks may remain unchanged.

def NN.MLTheory.CROWN.Graph.Refinement.valid {α : Type} [TorchLean.Storage α] [Context α] (box : FlatBox α) : Bool

Reject reversed or unordered endpoints before combining boxes.

def NN.MLTheory.CROWN.Graph.Refinement.splitAt {α : Type} [TorchLean.Storage α] [Context α] (box : FlatBox α) (axis : Fin box.dim) (cut : α) : FlatBox α × FlatBox α

Split one coordinate at a shared boundary, leaving every other endpoint unchanged.

def NN.MLTheory.CROWN.Graph.Refinement.split? {α : Type} [TorchLean.Storage α] [Context α] (box : FlatBox α) : Option (FlatBox α × FlatBox α)

Split the widest coordinate that has a representable interior midpoint.

The halved-endpoint formula avoids overflow in lo + hi and hi - lo. The strict endpoint checks reject stagnation, unordered values, and infinite midpoints. A box with no such coordinate stays unsplit; there is no arbitrary epsilon perturbation of its domain.

def NN.MLTheory.CROWN.Graph.Refinement.combine? {α : Type} [TorchLean.Storage α] [Context α] (hull : Bool) (a b : FlatBox α) : Option (FlatBox α)

Combine compatible boxes by their coordinatewise hull or intersection.

An invalid intersection is rejected, never returned as an empty certificate. The comparison checks also prevent NaNs from disappearing through endpoint selection on native floating-point backends.

@[irreducible]

def NN.MLTheory.CROWN.Graph.Refinement.bound {α : Type} [TorchLean.Storage α] [Context α] (enclose : FlatBox α → Option (FlatBox α)) (input : FlatBox α) (budget : ℕ) : Option (FlatBox α)

Refine any box-to-box enclosure procedure using at most budget binary splits.

There are at most 2 * budget + 1 calls to bound. The budget is shared between the children, so it counts work rather than an exponentially growing depth. Zero budget returns the original result exactly. A failed child, dimension mismatch, or inconsistent intersection falls back to that result; successful siblings alone never stand in for the complete input domain.

@[simp]

theorem NN.MLTheory.CROWN.Graph.Refinement.bound_zero {α : Type} [TorchLean.Storage α] [Context α] (enclose : FlatBox α → Option (FlatBox α)) (input : FlatBox α) : bound enclose input 0 = enclose input

Disabling subdivision preserves the supplied enclosure procedure exactly.

def NN.MLTheory.CROWN.Graph.validIBPInputs {α : Type} [TorchLean.Storage α] [Context α] (g : Graph) (ps : ParamStore α) : Bool

Check that every declared graph input has a shape-compatible, ordered seed box.

def NN.MLTheory.CROWN.Graph.refinedIBPOutput? {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [NonlinearBoundOps α] (g : Graph) (ps : ParamStore α) (inputId outId budget : ℕ) : Option (FlatBox α)

Refine one graph output by subdividing the selected input box.

Every other input and parameter stays fixed. The same operation works for dense, convolutional, recurrent, attention, and mixed graphs to the extent their operators are supported by runIBP. The caller selects the input node and total split budget explicitly. Invalid node selections return none; unsupported transfers retain the ordinary IBP failure behavior.