TorchLean API

FloatLib.Floats.Formats.BinaryInterchange.IntervalSemantics

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.