Semantics of arbitrary-format executable intervals #
Public entry point for semantic membership, four-corner endpoint selection, and outward-rounded
arithmetic and activation soundness over Model.Interval fmt.
Read Core and Order for finite and extended-real membership, then MinMax for endpoint
selection. Arithmetic groups negation, the four binary operations, and reciprocal; Activations
groups ReLU, absolute value, and square root. Finite supplies range-checked arithmetic for
all-words-finite encodings. Individual theorems state their IEEE and finiteness requirements.