What directed endpoint arithmetic is supposed to mean #

NN.MLTheory.CROWN.BoundOps says what a scalar backend must compute; this file says what those computations mean, by interpreting an endpoint as a real number and comparing each directed operation with exact real arithmetic. The enclosure predicates and the two Lawful classes are the form in which CROWN theorems ask for that guarantee, and ℝ itself is the instance where the guarantee is trivial because no rounding happens.

Naming ℝ alongside Real.exp, Real.log, and Real.sqrt costs roughly 1700 mathlib modules, so the split is deliberate: certificate replay, the graph checker, and the trainer only ever run the executable interface and stop at BoundOps, while the soundness proofs continue on to this file.

source

class NN.MLTheory.CROWN.LawfulBoundOps (α : Type) [TorchLean.Storage α] [Context α] [BoundOps α] :

Type

Real-semantic enclosure laws for BoundOps.

The executable interface above is intentionally available without this class: a backend may be useful for diagnostics before its arithmetic has been connected to a proof. Sound CROWN theorems require LawfulBoundOps in addition to BoundOps. The interpretation toReal says what a scalar endpoint means mathematically, and the laws compare each directed operation with exact arithmetic on those real values. This is stronger than merely surrounding the backend's ordinary rounded operation.

There is a global instance for ℝ. There is deliberately no global instance for Lean Float or for all ExecFloat.Binary 8 23 bit patterns. Host Float is a trusted runtime boundary, while IEEE-754 NaNs, infinities, and overflow require finite-path hypotheses; those facts are stated at the IEEE semantics layer rather than hidden in an invalid ordered-ring instance.

toReal : α → ℝ
Mathematical value represented by an endpoint.
lt_iff (a b : α) : a < b ↔ toReal a < toReal b
Executable endpoint comparisons agree with the mathematical order.
addDown_le (a b : α) : toReal (BoundOps.addDown a b) ≤ toReal a + toReal b
le_addUp (a b : α) : toReal a + toReal b ≤ toReal (BoundOps.addUp a b)
subDown_le (a b : α) : toReal (BoundOps.subDown a b) ≤ toReal a - toReal b
le_subUp (a b : α) : toReal a - toReal b ≤ toReal (BoundOps.subUp a b)
mulDown_le (a b : α) : toReal (BoundOps.mulDown a b) ≤ toReal a * toReal b
le_mulUp (a b : α) : toReal a * toReal b ≤ toReal (BoundOps.mulUp a b)

Instances

source

def NN.MLTheory.CROWN.UnaryEnclosure {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (f : ℝ → ℝ) (transfer : α → α → Option (α × α)) :

Prop

Soundness predicate for a unary interval transfer.

Returning none is always permitted. If the transfer returns endpoints, every real input between the interpreted input endpoints must map between the interpreted output endpoints.

Instances For

source

def NN.MLTheory.CROWN.BinaryEnclosure {α : Type} [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] (f : ℝ → ℝ → ℝ) (transfer : α → α → α → α → Option (α × α)) :

Prop

Soundness predicate for a binary interval transfer.

Instances For

source

class NN.MLTheory.CROWN.LawfulNonlinearBoundOps (α : Type) [TorchLean.Storage α] [Context α] [BoundOps α] [LawfulBoundOps α] [NonlinearBoundOps α] :

Prop

Real-semantic enclosure laws for NonlinearBoundOps.

This class is deliberately separate from the executable transfer table. A backend may implement a transfer for testing before proving it; sound verification entrypoints can require this class and therefore cannot silently promote an unchecked implementation into a theorem.