Numerical certificate enclosures

Foundational source-range validation, real and IEEE enclosure semantics, replay checks, and pointwise error traces for graph numerical certificates. Most users should import NN.Proofs.RuntimeApprox.Graph.NumericalCertificate.

Raw and checked source assumptions

structure Proofs.RuntimeApprox.NumericalCertificate.SourceRange : Type

A binary32 range supplied for an input, constant, or explicit random source node.

• nodeId : ℕ
• enclosure : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) _proof_1 _proof_2 _proof_3 _proof_4)

def Proofs.RuntimeApprox.NumericalCertificate.instReprSourceRange.repr : SourceRange → ℕ → Std.Format

@[instance_reducible]

instance Proofs.RuntimeApprox.NumericalCertificate.instReprSourceRange : Repr SourceRange

structure Proofs.RuntimeApprox.NumericalCertificate.CheckedSourceRangeextends Proofs.RuntimeApprox.NumericalCertificate.SourceRange : Type

A source range after the checker has established finite, ordered endpoints.

• nodeId : ℕ
• enclosure : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) _proof_1 _proof_2 _proof_3 _proof_4)
• valid : FloatLib.Floats.ExecFloat.Binary.Interval.Valid self.enclosure

@[instance_reducible]

instance Proofs.RuntimeApprox.NumericalCertificate.instReprCheckedSourceRange : Repr CheckedSourceRange

def Proofs.RuntimeApprox.NumericalCertificate.sameIntervalBits (a b : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)) : Bool

Bitwise equality for executable binary32 intervals.

Bitwise equality is intentional: it distinguishes signed zero and preserves the exact endpoints written in a certificate. NaNs are rejected separately by Binary.Interval.Valid.

def Proofs.RuntimeApprox.NumericalCertificate.validInterval (interval : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)) : Bool

Executable counterpart of Binary.Interval.Valid.

theorem Proofs.RuntimeApprox.NumericalCertificate.leB_eq_true_iff (x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4) : FloatLib.Floats.ExecFloat.Binary.Interval.leB x y = true ↔ x ≤ y

Binary.Interval.leB decides the proposition-level IEEE non-strict order.

theorem Proofs.RuntimeApprox.NumericalCertificate.toReal_le_toReal_of_le {x y : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4} (hx : x.isFinite = true) (hy : y.isFinite = true) (hxy : x ≤ y) : x.toModel.toReal ≤ y.toModel.toReal

IEEE comparison between finite values implies the corresponding order on their real interpretations. This lemma is intentionally finite: IEEE comparisons involving NaN are unordered, and toReal is not the semantic interface for infinities.

theorem Proofs.RuntimeApprox.NumericalCertificate.validInterval_eq_true_iff (interval : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)) : validInterval interval = true ↔ FloatLib.Floats.ExecFloat.Binary.Interval.Valid interval

The executable validity test accepts exactly finite, ordered intervals.

Real semantics of the arithmetic transfers

The executable checker propagates binary32 endpoints, while the graph specification is normally read over real scalars. RealEncloses is the bridge between those views. Runtime rounding error is then composed separately by FwdGraph.eval_approx and RevGraph.backprop_approx; keeping these two claims separate prevents an interval enclosure from silently standing in for a floating-point error theorem.

def Proofs.RuntimeApprox.NumericalCertificate.RealEncloses (interval : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)) (value : ℝ) : Prop

A real scalar lies between the real interpretations of an executable interval's endpoints.

theorem Proofs.RuntimeApprox.NumericalCertificate.realEncloses_of_containsReal {interval : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)} {value : ℝ} (h : FloatLib.Numerics.Interval.ContainsReal FloatLib.Floats.ExecFloat.Binary.toRat? interval value) : RealEncloses interval value

Finite rational endpoint decoding agrees with the model's real interpretation.

theorem Proofs.RuntimeApprox.NumericalCertificate.add_realEncloses {a b : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)} {x y : ℝ} (ha : FloatLib.Floats.ExecFloat.Binary.Interval.Valid a) (hb : FloatLib.Floats.ExecFloat.Binary.Interval.Valid b) (hout : (FloatLib.Floats.ExecFloat.Binary.Interval.add a b).Valid) (hx : RealEncloses a x) (hy : RealEncloses b y) : RealEncloses (FloatLib.Floats.ExecFloat.Binary.Interval.add a b) (x + y)

Sound real enclosure for the canonical addition transfer.

theorem Proofs.RuntimeApprox.NumericalCertificate.sub_realEncloses {a b : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)} {x y : ℝ} (ha : FloatLib.Floats.ExecFloat.Binary.Interval.Valid a) (hb : FloatLib.Floats.ExecFloat.Binary.Interval.Valid b) (hout : (FloatLib.Floats.ExecFloat.Binary.Interval.sub a b).Valid) (hx : RealEncloses a x) (hy : RealEncloses b y) : RealEncloses (FloatLib.Floats.ExecFloat.Binary.Interval.sub a b) (x - y)

Sound real enclosure for the canonical subtraction transfer.

theorem Proofs.RuntimeApprox.NumericalCertificate.mul_realEncloses {a b : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)} {x y : ℝ} (ha : FloatLib.Floats.ExecFloat.Binary.Interval.Valid a) (hb : FloatLib.Floats.ExecFloat.Binary.Interval.Valid b) (hout : (FloatLib.Floats.ExecFloat.Binary.Interval.mul a b).Valid) (hx : RealEncloses a x) (hy : RealEncloses b y) : RealEncloses (FloatLib.Floats.ExecFloat.Binary.Interval.mul a b) (x * y)

Sound real enclosure for the canonical multiplication transfer.

def Proofs.RuntimeApprox.NumericalCertificate.sumLeftRange (count : ℕ) (range : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)) : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)

Outward left-fold enclosure, starting from the tensor reduction's positive zero.

def Proofs.RuntimeApprox.NumericalCertificate.scaledContractionRange? (count : ℕ) (left right scale : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)) : Option (FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4))

Enclose a scaled contraction without requiring its unscaled product to fit binary32.

The rational calculation rounds only its final endpoints. When the ordinary staged enclosure is finite, its endpoints widen this enclosure too. IEEE execution is still checked separately against the returned interval; this transfer does not identify a native kernel with the reference rule.

theorem Proofs.RuntimeApprox.NumericalCertificate.scaledContractionRange?_contains {count : ℕ} {left right scale output : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)} (h : scaledContractionRange? count left right scale = some output) (x y : Fin count → ℝ) (coefficient : ℝ) (hx : ∀ (i : Fin count), FloatLib.Numerics.Interval.ContainsReal FloatLib.Floats.ExecFloat.Binary.toRat? left (x i)) (hy : ∀ (i : Fin count), FloatLib.Numerics.Interval.ContainsReal FloatLib.Floats.ExecFloat.Binary.toRat? right (y i)) (hc : FloatLib.Numerics.Interval.ContainsReal FloatLib.Floats.ExecFloat.Binary.toRat? scale coefficient) : FloatLib.Numerics.Interval.ContainsReal FloatLib.Floats.ExecFloat.Binary.toRat? output ((∑ i : Fin count, x i * y i) * coefficient)

The grouped transfer contains the exact real scaled sum for every choice of its summands.

The successful outward-rounding hypothesis is essential: an unavailable finite enclosure is not a certificate. This theorem concerns the real expression; concrete IEEE values must also pass replay.

theorem Proofs.RuntimeApprox.NumericalCertificate.scaledProducts_real_contains {m n p : ℕ} {left right scale output : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)} (h : scaledContractionRange? n left right scale = some output) (a : TorchLean.Tensor ℝ [m, n]) (b : TorchLean.Tensor ℝ [n, p]) (coefficient : ℝ) (ha : ∀ (i : Fin m) (k : Fin n), FloatLib.Numerics.Interval.ContainsReal FloatLib.Floats.ExecFloat.Binary.toRat? left (Spec.get2 a i k)) (hb : ∀ (k : Fin n) (j : Fin p), FloatLib.Numerics.Interval.ContainsReal FloatLib.Floats.ExecFloat.Binary.toRat? right (Spec.get2 b k j)) (hc : FloatLib.Numerics.Interval.ContainsReal FloatLib.Floats.ExecFloat.Binary.toRat? scale coefficient) (i : Fin m) (j : Fin p) : FloatLib.Numerics.Interval.ContainsReal FloatLib.Floats.ExecFloat.Binary.toRat? output (Spec.get2 (Spec.Internal.scaledProducts (fun (x : Fin 1) => a) (fun (x : Fin 1) => b) coefficient) i j)

The enclosure transfer bounds each entry of the actual real grouped matrix specification. No equality between rounded staged multiplication and coefficient replay is used.

theorem Proofs.RuntimeApprox.NumericalCertificate.inv_realEncloses {a : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)} {x : ℝ} (ha : FloatLib.Floats.ExecFloat.Binary.Interval.Valid a) (hout : (FloatLib.Floats.ExecFloat.Binary.Interval.inv a).Valid) (hx : RealEncloses a x) : RealEncloses (FloatLib.Floats.ExecFloat.Binary.Interval.inv a) x⁻¹

Sound real enclosure for the canonical reciprocal transfer.

def Proofs.RuntimeApprox.NumericalCertificate.TensorEnclosed (interval : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)) {shape : Spec.Shape} : TorchLean.Tensor ℝ shape → Prop

Every scalar entry of a shape-indexed real tensor lies in one interval.

theorem Proofs.RuntimeApprox.NumericalCertificate.scaledProducts_tensorEnclosed {m n p : ℕ} {left right scale output : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)} (h : scaledContractionRange? n left right scale = some output) (a : TorchLean.Tensor ℝ [m, n]) (b : TorchLean.Tensor ℝ [n, p]) (coefficient : ℝ) (ha : ∀ (i : Fin m) (k : Fin n), FloatLib.Numerics.Interval.ContainsReal FloatLib.Floats.ExecFloat.Binary.toRat? left (Spec.get2 a i k)) (hb : ∀ (k : Fin n) (j : Fin p), FloatLib.Numerics.Interval.ContainsReal FloatLib.Floats.ExecFloat.Binary.toRat? right (Spec.get2 b k j)) (hc : FloatLib.Numerics.Interval.ContainsReal FloatLib.Floats.ExecFloat.Binary.toRat? scale coefficient) : TensorEnclosed output (Spec.Internal.scaledProducts (fun (x : Fin 1) => a) (fun (x : Fin 1) => b) coefficient)

The grouped real matrix result satisfies the tensor enclosure used by graph certificates.

def Proofs.RuntimeApprox.NumericalCertificate.unitInterval : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)

The exact executable interval [0,1].

def Proofs.RuntimeApprox.NumericalCertificate.signedUnitInterval : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)

The exact executable interval [-1,1].

def Proofs.RuntimeApprox.NumericalCertificate.nonnegativeEndpoint (x : FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4) : Bool

Executable test for a finite endpoint's nonnegative IEEE sign. Both signed zeros are accepted; all other accepted values have a clear sign bit. Finiteness is supplied by interval validity.

theorem Proofs.RuntimeApprox.NumericalCertificate.softmaxVec_tensor_enclosed {n : ℕ} (input : TorchLean.Tensor ℝ [n.succ]) : TensorEnclosed unitInterval (Activation.softmaxVecSpec input)

The stable real vector softmax is enclosed by the certificate transfer [0,1].

theorem Proofs.RuntimeApprox.NumericalCertificate.relu_realEncloses {a : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)} {x : ℝ} (ha : FloatLib.Floats.ExecFloat.Binary.Interval.Valid a) (hx : RealEncloses a x) : RealEncloses (FloatLib.Floats.ExecFloat.Binary.Interval.relu a) (max x 0)

Sound real enclosure for the canonical ReLU interval transfer.

theorem Proofs.RuntimeApprox.NumericalCertificate.abs_realEncloses {a : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)} {x : ℝ} (ha : FloatLib.Floats.ExecFloat.Binary.Interval.Valid a) (hx : RealEncloses a x) : RealEncloses (FloatLib.Floats.ExecFloat.Binary.Interval.abs a) |x|

Sound real enclosure for the canonical absolute-value interval transfer.

theorem Proofs.RuntimeApprox.NumericalCertificate.sqrt_realEncloses {a : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)} {x : ℝ} (ha : FloatLib.Floats.ExecFloat.Binary.Interval.Valid a) (hlo : nonnegativeEndpoint a.lo = true) (hout : (FloatLib.Floats.ExecFloat.Binary.Interval.sqrt a).Valid) (hx : RealEncloses a x) : RealEncloses (FloatLib.Floats.ExecFloat.Binary.Interval.sqrt a) √x

Sound real enclosure for directed interval square root. Only the lower endpoint needs a nonnegative sign; the upper one then follows from interval order.

theorem Proofs.RuntimeApprox.NumericalCertificate.tensor_map_enclosed (op : ℝ → ℝ) (input output : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)) (sound : ∀ {x : ℝ}, RealEncloses input x → RealEncloses output (op x)) {shape : Spec.Shape} {x : TorchLean.Tensor ℝ shape} : TensorEnclosed input x → TensorEnclosed output (TorchLean.Tensor.map op x)

Lift a sound unary scalar transfer to tensors of arbitrary rank.

theorem Proofs.RuntimeApprox.NumericalCertificate.tensor_relu_enclosed {shape : Spec.Shape} {x : TorchLean.Tensor ℝ shape} {a : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)} (ha : FloatLib.Floats.ExecFloat.Binary.Interval.Valid a) (hx : TensorEnclosed a x) : TensorEnclosed (FloatLib.Floats.ExecFloat.Binary.Interval.relu a) (TorchLean.Tensor.map (fun (value : ℝ) => max value 0) x)

Tensor-level soundness of the ReLU interval transfer.

theorem Proofs.RuntimeApprox.NumericalCertificate.tensor_abs_enclosed {shape : Spec.Shape} {x : TorchLean.Tensor ℝ shape} {a : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)} (ha : FloatLib.Floats.ExecFloat.Binary.Interval.Valid a) (hx : TensorEnclosed a x) : TensorEnclosed (FloatLib.Floats.ExecFloat.Binary.Interval.abs a) (TorchLean.Tensor.map abs x)

Tensor-level soundness of the absolute-value interval transfer.

theorem Proofs.RuntimeApprox.NumericalCertificate.tensor_sqrt_enclosed {shape : Spec.Shape} {x : TorchLean.Tensor ℝ shape} {a : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)} (ha : FloatLib.Floats.ExecFloat.Binary.Interval.Valid a) (hlo : nonnegativeEndpoint a.lo = true) (hout : (FloatLib.Floats.ExecFloat.Binary.Interval.sqrt a).Valid) (hx : TensorEnclosed a x) : TensorEnclosed (FloatLib.Floats.ExecFloat.Binary.Interval.sqrt a) (TorchLean.Tensor.map Real.sqrt x)

Tensor-level soundness of directed interval square root.

theorem Proofs.RuntimeApprox.NumericalCertificate.tensor_map2_enclosed (op : ℝ → ℝ → ℝ) (a b out : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)) (sound : ∀ {x y : ℝ}, RealEncloses a x → RealEncloses b y → RealEncloses out (op x y)) {shape : Spec.Shape} {x y : TorchLean.Tensor ℝ shape} : TensorEnclosed a x → TensorEnclosed b y → TensorEnclosed out (TorchLean.Tensor.map2Spec op x y)

Lift a sound binary scalar transfer to tensors of arbitrary rank.

theorem Proofs.RuntimeApprox.NumericalCertificate.tensor_add_enclosed {shape : Spec.Shape} {x y : TorchLean.Tensor ℝ shape} {a b : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)} (ha : FloatLib.Floats.ExecFloat.Binary.Interval.Valid a) (hb : FloatLib.Floats.ExecFloat.Binary.Interval.Valid b) (hout : (FloatLib.Floats.ExecFloat.Binary.Interval.add a b).Valid) (hx : TensorEnclosed a x) (hy : TensorEnclosed b y) : TensorEnclosed (FloatLib.Floats.ExecFloat.Binary.Interval.add a b) (x.addSpec y)

Tensor-level soundness of outward-rounded interval addition.

theorem Proofs.RuntimeApprox.NumericalCertificate.tensor_sub_enclosed {shape : Spec.Shape} {x y : TorchLean.Tensor ℝ shape} {a b : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)} (ha : FloatLib.Floats.ExecFloat.Binary.Interval.Valid a) (hb : FloatLib.Floats.ExecFloat.Binary.Interval.Valid b) (hout : (FloatLib.Floats.ExecFloat.Binary.Interval.sub a b).Valid) (hx : TensorEnclosed a x) (hy : TensorEnclosed b y) : TensorEnclosed (FloatLib.Floats.ExecFloat.Binary.Interval.sub a b) (x.subSpec y)

Tensor-level soundness of outward-rounded interval subtraction.

theorem Proofs.RuntimeApprox.NumericalCertificate.tensor_mul_enclosed {shape : Spec.Shape} {x y : TorchLean.Tensor ℝ shape} {a b : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)} (ha : FloatLib.Floats.ExecFloat.Binary.Interval.Valid a) (hb : FloatLib.Floats.ExecFloat.Binary.Interval.Valid b) (hout : (FloatLib.Floats.ExecFloat.Binary.Interval.mul a b).Valid) (hx : TensorEnclosed a x) (hy : TensorEnclosed b y) : TensorEnclosed (FloatLib.Floats.ExecFloat.Binary.Interval.mul a b) (x.mulSpec y)

Tensor-level soundness of outward-rounded interval multiplication.

Replay against bit-level graph execution

def Proofs.RuntimeApprox.NumericalCertificate.tensorWithinRange (interval : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)) {shape : Spec.Shape} : TorchLean.Tensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4) shape → Bool

Executable check that every binary32 tensor entry lies in an interval.

def Proofs.RuntimeApprox.NumericalCertificate.IEEETensorEnclosed (interval : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)) {shape : Spec.Shape} : TorchLean.Tensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4) shape → Prop

Proposition expressed by tensorWithinRange.

theorem Proofs.RuntimeApprox.NumericalCertificate.tensorWithinRange_eq_true_iff (interval : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)) {shape : Spec.Shape} (tensor : TorchLean.Tensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4) shape) : tensorWithinRange interval tensor = true ↔ IEEETensorEnclosed interval tensor

The executable tensor range check is exact for the IEEE comparison semantics.

From checked ranges to explicit error bounds

def Proofs.RuntimeApprox.NumericalCertificate.DecodedTensorEnclosed (interval : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)) {shape : Spec.Shape} : TorchLean.Tensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4) shape → Prop

Decode an executable tensor entrywise and state that the resulting real tensor lies in an interval. Unlike IEEETensorEnclosed, this predicate talks directly about the real values used by the approximation layer.

theorem Proofs.RuntimeApprox.NumericalCertificate.decodedTensorEnclosed_of_ieee {interval : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)} (valid : FloatLib.Floats.ExecFloat.Binary.Interval.Valid interval) {shape : Spec.Shape} {tensor : TorchLean.Tensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4) shape} : IEEETensorEnclosed interval tensor → DecodedTensorEnclosed interval tensor

A successful IEEE range check decodes to an ordinary real enclosure. Finiteness is an explicit part of IEEETensorEnclosed, so this theorem never assigns a real meaning to NaN or infinity.

def Proofs.RuntimeApprox.NumericalCertificate.TensorErrorLe (eps : ℝ) {shape : Spec.Shape} : TorchLean.Tensor ℝ shape → TorchLean.Tensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4) shape → Prop

Pointwise absolute error between a real specification tensor and an executable binary32 tensor. The shape index is shared, so no runtime shape cast is hidden in the relation.

noncomputable def Proofs.RuntimeApprox.NumericalCertificate.intervalWidth (interval : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)) : ℝ

Width of a finite executable interval, interpreted in the reals.

theorem Proofs.RuntimeApprox.NumericalCertificate.intervalWidth_nonneg {interval : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)} (valid : FloatLib.Floats.ExecFloat.Binary.Interval.Valid interval) : 0 ≤ intervalWidth interval

A valid interval has nonnegative real width.

theorem Proofs.RuntimeApprox.NumericalCertificate.tensor_error_le_width_of_enclosed {interval : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)} {shape : Spec.Shape} {exact : TorchLean.Tensor ℝ shape} {computed : TorchLean.Tensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4) shape} : TensorEnclosed interval exact → DecodedTensorEnclosed interval computed → TensorErrorLe (intervalWidth interval) exact computed

Two tensors enclosed by the same interval differ entrywise by at most its width.

This is the elementary bridge from range analysis to approximation analysis. It is deliberately pointwise; a later norm theorem can package the same statement as an L∞ bound without changing the checker or its certificate format.

theorem Proofs.RuntimeApprox.NumericalCertificate.tensor_error_le_width_of_check {interval : FloatLib.Numerics.Interval (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4)} (valid : FloatLib.Floats.ExecFloat.Binary.Interval.Valid interval) {shape : Spec.Shape} {exact : TorchLean.Tensor ℝ shape} {computed : TorchLean.Tensor (FloatLib.Floats.ExecFloat.Binary 8 23 FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee (FloatLib.Floats.Formats.BinaryInterchange.FloatFormat.Encoding.ieee.defaultBias 8) SourceRange._proof_1 SourceRange._proof_2 SourceRange._proof_3 SourceRange._proof_4) shape} (hexact : TensorEnclosed interval exact) (hcheck : tensorWithinRange interval computed = true) : TensorErrorLe (intervalWidth interval) exact computed

A successful executable range check and a real enclosure proof yield a concrete pointwise error bound. This theorem is the tensor-level core used by graph-wide numerical certificates.

def Proofs.RuntimeApprox.NumericalCertificate.checkSources (sources : Array SourceRange) : Except String (Array CheckedSourceRange)

Check source ranges once, rejecting malformed intervals and duplicate node ids.

def Proofs.RuntimeApprox.NumericalCertificate.findSource (sources : Array CheckedSourceRange) (nodeId : ℕ) : Except String CheckedSourceRange

Find the checked assumption for a source node.

def Proofs.RuntimeApprox.NumericalCertificate.opUsesSourceRange : NN.IR.OpKind → Bool

Whether a graph node obtains its enclosure directly from a certificate source assumption.

def Proofs.RuntimeApprox.NumericalCertificate.checkSourceOwnership (graph : NN.IR.Graph) (sources : Array CheckedSourceRange) : Except String Unit

Reject source assumptions that do not name a source-like node in the checked graph.

Unused assumptions do not make interval propagation unsound, but they make artifacts ambiguous: an exporter may have attached a valid range to the wrong node id without noticing. Requiring every row to be consumed gives source arrays one canonical interpretation and catches that error before range propagation begins.