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.

The real-analysis dependencies belong to the soundness proofs. Certificate replay, the graph checker, and the trainer use the executable BoundOps interface without importing this file.

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

Real-semantic enclosure laws for BoundOps.

The executable interface BoundOps 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.

• toReal_zero : toReal 0 = 0

  The endpoint 0 means the real number 0.

• toReal_one : toReal 1 = 1

  The endpoint 1 means the real number 1.

• toReal_max (a b : α) : toReal (a ⊔ b) = max (toReal a) (toReal b)

  The backend maximum is the real maximum.

• toReal_eq_of_beq {a b : α} : (a == b) = true → toReal a = toReal b

  Endpoints that test equal denote the same real number.

• 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)

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

The backend minimum denotes the real minimum.

This supplements LawfulBoundOps for transfers that use the context's min operation. The comparison-based BoundOps.min2 needs no additional law. Ordinary negation and absolute value may round on a backend, so their exactness is deliberately not assumed here.

• toReal_min (a b : α) : LawfulBoundOps.toReal (a ⊓ b) = min (LawfulBoundOps.toReal a) (LawfulBoundOps.toReal b)

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.

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

Soundness predicate for a binary interval transfer.

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.

• divBounds_enclosure : BinaryEnclosure (fun (x1 x2 : ℝ) => x1 / x2) NonlinearBoundOps.divBounds
• expBounds_enclosure : UnaryEnclosure Real.exp NonlinearBoundOps.expBounds
• logBounds_enclosure : UnaryEnclosure Real.log NonlinearBoundOps.logBounds
• sqrtBounds_enclosure : UnaryEnclosure Real.sqrt NonlinearBoundOps.sqrtBounds
• sigmoidBounds_enclosure : UnaryEnclosure (fun (x : ℝ) => 1 / (1 + Real.exp (-x))) NonlinearBoundOps.sigmoidBounds
• tanhBounds_enclosure : UnaryEnclosure Real.tanh NonlinearBoundOps.tanhBounds
• sinBounds_enclosure : UnaryEnclosure Real.sin NonlinearBoundOps.sinBounds
• cosBounds_enclosure : UnaryEnclosure Real.cos NonlinearBoundOps.cosBounds
• layerNormAbsBound_sound {n : ℕ} {radius : α} : NonlinearBoundOps.layerNormAbsBound n = some radius → √↑n ≤ LawfulBoundOps.toReal radius
• coupledDerivatives_exact : NonlinearBoundOps.supportsIdealCoupledDerivatives α = true → BoundOps.supportsExactAffineReassociation α = true

Exact real arithmetic needs no rounding, so its lower and upper operations coincide.

@[instance_reducible]

noncomputable instance NN.MLTheory.CROWN.instBoundOpsReal : BoundOps ℝ

@[instance_reducible]

noncomputable instance NN.MLTheory.CROWN.instLawfulBoundOpsReal : LawfulBoundOps ℝ

Exact real endpoint arithmetic satisfies the directed-operation enclosure laws.

instance NN.MLTheory.CROWN.instLawfulMinBoundOpsReal : LawfulMinBoundOps ℝ

The exact real backend preserves minimum.

theorem NN.MLTheory.CROWN.min2_eq_min (a b : ℝ) : BoundOps.min2 a b = min a b

Over ℝ, the comparison-based BoundOps.min2 is min.

theorem NN.MLTheory.CROWN.max2_eq_max (a b : ℝ) : BoundOps.max2 a b = max a b

Over ℝ, the comparison-based BoundOps.max2 is max.

@[instance_reducible]

noncomputable instance NN.MLTheory.CROWN.instNonlinearBoundOpsReal : NonlinearBoundOps ℝ

Exact nonlinear interval transfers over the real numbers.