Numerical certificates for TorchLean graphs

This module joins three existing parts of TorchLean without introducing another graph or another floating-point representation:

• NN.IR.Graph remains the program being analysed;
• IEEE32Exec.Interval32 supplies executable, outward-rounded binary32 intervals;
• NN.Backend.ExecutionAudit records the kernel capsules selected by backend planning.

A raw certificate is proof-free data that an application may construct or decode using its own artifact format; this module does not prescribe a JSON schema. check does not trust its node ranges. It reconstructs the canonical range trace from the graph and source assumptions, checks every interval for finite ordered endpoints, replans the graph under the named backend profile, and compares the result with the raw artifact. Successful checking returns a CheckedCertificate, whose node ranges carry finite-endpoint and ordering proofs. This executable check does not by itself prove enclosure of the exact-real graph denotation; that evidence is the separate CheckedRealExecution value used by CheckedExecution.errorTrace.

The range trace deliberately starts with operations whose enclosure is already provided by the sound Interval32 core. Unsupported operations fail with the node id and operation name. They are not assigned [-inf,+inf], because that would turn a missing numerical theorem into an apparently successful certificate.

The numerical conventions follow IEEE Std 754-2019. Outward-rounded interval propagation follows IEEE Std 1788-2015 and the standard inclusion principle for interval arithmetic. For the error model that composes local bounds across forward and reverse graphs, see ForwardApprox.lean and BackwardApprox.lean; the organization follows the local-error/global-error distinction in N. J. Higham, Accuracy and Stability of Numerical Algorithms, 2nd ed., 2002.

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 : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32

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

@[implicit_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 : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32
• valid : self.enclosure.Valid

@[implicit_reducible]

instance Proofs.RuntimeApprox.NumericalCertificate.instReprCheckedSourceRange : Repr CheckedSourceRange

def Proofs.RuntimeApprox.NumericalCertificate.sameIntervalBits (a b : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32) : 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 Interval32.Valid.

def Proofs.RuntimeApprox.NumericalCertificate.validInterval (interval : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32) : Bool

Executable counterpart of Interval32.Valid.

theorem Proofs.RuntimeApprox.NumericalCertificate.leB_eq_true_iff (x y : TorchLean.Floats.IEEE754.IEEE32Exec) : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32.leB x y = true ↔ x.le y

Interval32.leB decides the proposition-level IEEE non-strict order.

theorem Proofs.RuntimeApprox.NumericalCertificate.toReal_le_toReal_of_le {x y : TorchLean.Floats.IEEE754.IEEE32Exec} (hx : x.isFinite = true) (hy : y.isFinite = true) (hxy : x.le y) : x.toReal ≤ y.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.toReal_neg_of_isFinite {x : TorchLean.Floats.IEEE754.IEEE32Exec} (hx : x.isFinite = true) : x.neg.toReal = -x.toReal

Negation of a finite executable binary32 value decodes to real negation.

theorem Proofs.RuntimeApprox.NumericalCertificate.isFinite_neg_of_isFinite {x : TorchLean.Floats.IEEE754.IEEE32Exec} (hx : x.isFinite = true) : x.neg.isFinite = true

Flipping the sign bit preserves finiteness.

theorem Proofs.RuntimeApprox.NumericalCertificate.validInterval_eq_true_iff (interval : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32) : validInterval interval = true ↔ interval.Valid

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 : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32) (value : ℝ) : Prop

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

theorem Proofs.RuntimeApprox.NumericalCertificate.realEncloses_of_eReal_bounds {interval : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32} {value : ℝ} (valid : interval.Valid) (bounds : interval.lo.toEReal ≤ ↑value ∧ ↑value ≤ interval.hi.toEReal) : RealEncloses interval value

Convert the extended-real endpoint form used by the interval soundness library into an ordinary real interval when the output endpoints are finite.

theorem Proofs.RuntimeApprox.NumericalCertificate.add_realEncloses {a b : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32} {x y : ℝ} (ha : a.Valid) (hb : b.Valid) (hout : (a.add b).Valid) (hx : RealEncloses a x) (hy : RealEncloses b y) : RealEncloses (a.add b) (x + y)

Sound real enclosure for the canonical addition transfer.

theorem Proofs.RuntimeApprox.NumericalCertificate.sub_realEncloses {a b : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32} {x y : ℝ} (ha : a.Valid) (hb : b.Valid) (hout : (a.sub b).Valid) (hx : RealEncloses a x) (hy : RealEncloses b y) : RealEncloses (a.sub b) (x - y)

Sound real enclosure for the canonical subtraction transfer.

theorem Proofs.RuntimeApprox.NumericalCertificate.mul_realEncloses {a b : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32} {x y : ℝ} (ha : a.Valid) (hb : b.Valid) (hout : (a.mul b).Valid) (hx : RealEncloses a x) (hy : RealEncloses b y) : RealEncloses (a.mul b) (x * y)

Sound real enclosure for the canonical multiplication transfer.

theorem Proofs.RuntimeApprox.NumericalCertificate.inv_realEncloses {a : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32} {x : ℝ} (ha : a.Valid) (hout : a.inv.Valid) (hx : RealEncloses a x) : RealEncloses a.inv x⁻¹

Sound real enclosure for the canonical reciprocal transfer.

def Proofs.RuntimeApprox.NumericalCertificate.TensorEnclosed (interval : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32) {shape : Spec.Shape} : Spec.Tensor ℝ shape → Prop

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

def Proofs.RuntimeApprox.NumericalCertificate.unitInterval : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32

The exact executable interval [0,1].

def Proofs.RuntimeApprox.NumericalCertificate.signedUnitInterval : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32

The exact executable interval [-1,1].

def Proofs.RuntimeApprox.NumericalCertificate.nonnegativeEndpoint (x : TorchLean.Floats.IEEE754.IEEE32Exec) : 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 : Spec.Tensor ℝ (Spec.Shape.dim n.succ Spec.Shape.scalar)) : 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 : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32} {x : ℝ} (ha : a.Valid) (hx : RealEncloses a x) : RealEncloses a.relu (max x 0)

Sound real enclosure for the canonical ReLU interval transfer.

theorem Proofs.RuntimeApprox.NumericalCertificate.abs_realEncloses {a : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32} {x : ℝ} (ha : a.Valid) (hx : RealEncloses a x) : RealEncloses a.abs |x|

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

theorem Proofs.RuntimeApprox.NumericalCertificate.toReal_sqrtDown_le {x : TorchLean.Floats.IEEE754.IEEE32Exec} (hfin : x.isFinite = true) (hdomain : nonnegativeEndpoint x = true) (hout : x.sqrtDown.isFinite = true) : x.sqrtDown.toReal ≤ √x.toReal

A directed lower square-root endpoint lies below the exact real square root. Signed zero is handled separately because IEEE preserves its sign, while the general directed-rounding theorem is stated for sign-bit-false inputs.

theorem Proofs.RuntimeApprox.NumericalCertificate.toReal_sqrtUp_ge {x : TorchLean.Floats.IEEE754.IEEE32Exec} (hfin : x.isFinite = true) (hdomain : nonnegativeEndpoint x = true) (hout : x.sqrtUp.isFinite = true) : √x.toReal ≤ x.sqrtUp.toReal

Upper counterpart of toReal_sqrtDown_le.

theorem Proofs.RuntimeApprox.NumericalCertificate.sqrt_realEncloses {a : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32} {x : ℝ} (ha : a.Valid) (hlo : nonnegativeEndpoint a.lo = true) (hhi : nonnegativeEndpoint a.hi = true) (hout : a.sqrt.Valid) (hx : RealEncloses a x) : RealEncloses a.sqrt √x

Sound real enclosure for directed interval square root.

theorem Proofs.RuntimeApprox.NumericalCertificate.tensor_map_enclosed (op : ℝ → ℝ) (input output : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32) (sound : ∀ {x : ℝ}, RealEncloses input x → RealEncloses output (op x)) {shape : Spec.Shape} {x : Spec.Tensor ℝ shape} : TensorEnclosed input x → TensorEnclosed output (Spec.Tensor.mapSpec op x)

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

theorem Proofs.RuntimeApprox.NumericalCertificate.tensor_relu_enclosed {shape : Spec.Shape} {x : Spec.Tensor ℝ shape} {a : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32} (ha : a.Valid) (hx : TensorEnclosed a x) : TensorEnclosed a.relu (Spec.Tensor.mapSpec (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 : Spec.Tensor ℝ shape} {a : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32} (ha : a.Valid) (hx : TensorEnclosed a x) : TensorEnclosed a.abs (Spec.Tensor.mapSpec abs x)

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

theorem Proofs.RuntimeApprox.NumericalCertificate.tensor_sqrt_enclosed {shape : Spec.Shape} {x : Spec.Tensor ℝ shape} {a : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32} (ha : a.Valid) (hlo : nonnegativeEndpoint a.lo = true) (hhi : nonnegativeEndpoint a.hi = true) (hout : a.sqrt.Valid) (hx : TensorEnclosed a x) : TensorEnclosed a.sqrt (Spec.Tensor.mapSpec Real.sqrt x)

Tensor-level soundness of directed interval square root.

theorem Proofs.RuntimeApprox.NumericalCertificate.tensor_map2_enclosed (op : ℝ → ℝ → ℝ) (a b out : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32) (sound : ∀ {x y : ℝ}, RealEncloses a x → RealEncloses b y → RealEncloses out (op x y)) {shape : Spec.Shape} {x y : Spec.Tensor ℝ shape} : TensorEnclosed a x → TensorEnclosed b y → TensorEnclosed out (Spec.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 : Spec.Tensor ℝ shape} {a b : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32} (ha : a.Valid) (hb : b.Valid) (hout : (a.add b).Valid) (hx : TensorEnclosed a x) (hy : TensorEnclosed b y) : TensorEnclosed (a.add b) (x.addSpec y)

Tensor-level soundness of outward-rounded interval addition.

theorem Proofs.RuntimeApprox.NumericalCertificate.tensor_sub_enclosed {shape : Spec.Shape} {x y : Spec.Tensor ℝ shape} {a b : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32} (ha : a.Valid) (hb : b.Valid) (hout : (a.sub b).Valid) (hx : TensorEnclosed a x) (hy : TensorEnclosed b y) : TensorEnclosed (a.sub b) (x.subSpec y)

Tensor-level soundness of outward-rounded interval subtraction.

theorem Proofs.RuntimeApprox.NumericalCertificate.tensor_mul_enclosed {shape : Spec.Shape} {x y : Spec.Tensor ℝ shape} {a b : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32} (ha : a.Valid) (hb : b.Valid) (hout : (a.mul b).Valid) (hx : TensorEnclosed a x) (hy : TensorEnclosed b y) : TensorEnclosed (a.mul b) (x.mulSpec y)

Tensor-level soundness of outward-rounded interval multiplication.

Replay against bit-level graph execution

def Proofs.RuntimeApprox.NumericalCertificate.tensorWithinRange (interval : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32) {shape : Spec.Shape} : Spec.Tensor TorchLean.Floats.IEEE754.IEEE32Exec shape → Bool

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

def Proofs.RuntimeApprox.NumericalCertificate.IEEETensorEnclosed (interval : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32) {shape : Spec.Shape} : Spec.Tensor TorchLean.Floats.IEEE754.IEEE32Exec shape → Prop

Proposition expressed by tensorWithinRange.

theorem Proofs.RuntimeApprox.NumericalCertificate.tensorWithinRange_eq_true_iff (interval : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32) {shape : Spec.Shape} (tensor : Spec.Tensor TorchLean.Floats.IEEE754.IEEE32Exec 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 : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32) {shape : Spec.Shape} : Spec.Tensor TorchLean.Floats.IEEE754.IEEE32Exec 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 : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32} (valid : interval.Valid) {shape : Spec.Shape} {tensor : Spec.Tensor TorchLean.Floats.IEEE754.IEEE32Exec 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} : Spec.Tensor ℝ shape → Spec.Tensor TorchLean.Floats.IEEE754.IEEE32Exec 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 : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32) : ℝ

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

theorem Proofs.RuntimeApprox.NumericalCertificate.intervalWidth_nonneg {interval : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32} (valid : interval.Valid) : 0 ≤ intervalWidth interval

A valid interval has nonnegative real width.

theorem Proofs.RuntimeApprox.NumericalCertificate.tensor_error_le_width_of_enclosed {interval : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32} {shape : Spec.Shape} {exact : Spec.Tensor ℝ shape} {computed : Spec.Tensor TorchLean.Floats.IEEE754.IEEE32Exec 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 : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32} (valid : interval.Valid) {shape : Spec.Shape} {exact : Spec.Tensor ℝ shape} {computed : Spec.Tensor TorchLean.Floats.IEEE754.IEEE32Exec 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.

Canonical local transfer rules

inductive Proofs.RuntimeApprox.NumericalCertificate.RangeRule : Type

How a node enclosure was obtained from source assumptions or earlier nodes.

The rule is recorded to make certificate diagnostics useful. It is not accepted on faith: check reconstructs the rule and endpoints from the graph.

• source : RangeRule
• preserve (parent : ℕ) : RangeRule
• add (left right : ℕ) : RangeRule
• sub (left right : ℕ) : RangeRule
• mul (left right : ℕ) : RangeRule
• inv (parent : ℕ) : RangeRule
• hull (parents : List ℕ) : RangeRule
• hullZero (parent : ℕ) : RangeRule
• sumLeft (parent count : ℕ) : RangeRule
• meanLeft (parent count : ℕ) : RangeRule
• matmulLeft (left right innerDim : ℕ) : RangeRule
• averageWindowLeft (parent windowSize : ℕ) (includesPadding : Bool) : RangeRule
• mseLeft (prediction target count : ℕ) : RangeRule
• layerNormLeft (parent axis normalizedSize : ℕ) : RangeRule
• softmaxUnit (parent axis : ℕ) : RangeRule
• relu (parent : ℕ) : RangeRule
• abs (parent : ℕ) : RangeRule
• sqrtNonnegative (parent : ℕ) : RangeRule
• unitBound (parent : ℕ) : RangeRule
• signedUnitBound (parent : ℕ) : RangeRule

def Proofs.RuntimeApprox.NumericalCertificate.instDecidableEqRangeRule.decEq (x✝ x✝¹ : RangeRule) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance Proofs.RuntimeApprox.NumericalCertificate.instDecidableEqRangeRule : DecidableEq RangeRule

def Proofs.RuntimeApprox.NumericalCertificate.instReprRangeRule.repr : RangeRule → ℕ → Std.Format

@[implicit_reducible]

instance Proofs.RuntimeApprox.NumericalCertificate.instReprRangeRule : Repr RangeRule

structure Proofs.RuntimeApprox.NumericalCertificate.NodeRange : Type

Proof-free data for one graph node's numerical range.

• nodeId : ℕ
• outShape : Spec.Shape
• rule : RangeRule
• enclosure : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32

@[implicit_reducible]

instance Proofs.RuntimeApprox.NumericalCertificate.instReprNodeRange : Repr NodeRange

def Proofs.RuntimeApprox.NumericalCertificate.instReprNodeRange.repr : NodeRange → ℕ → Std.Format

structure Proofs.RuntimeApprox.NumericalCertificate.CheckedNodeRangeextends Proofs.RuntimeApprox.NumericalCertificate.NodeRange : Type

A node range whose executable interval has passed the finite/order check.

• nodeId : ℕ
• outShape : Spec.Shape
• rule : RangeRule
• enclosure : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32
• valid : self.enclosure.Valid

@[implicit_reducible]

instance Proofs.RuntimeApprox.NumericalCertificate.instReprCheckedNodeRange : Repr CheckedNodeRange

def Proofs.RuntimeApprox.NumericalCertificate.dvalWithinRange (range : CheckedNodeRange) (value : NN.IR.DVal TorchLean.Floats.IEEE754.IEEE32Exec) : Bool

Check a dynamic graph value against the declared shape and interval of one certificate row.

def Proofs.RuntimeApprox.NumericalCertificate.RealDValEnclosed (range : CheckedNodeRange) (value : NN.IR.DVal ℝ) : Prop

A real dynamic graph value has the shape declared by a certificate row and is enclosed by its interval. The equality witness makes the dependent tensor cast explicit.

def Proofs.RuntimeApprox.NumericalCertificate.DValErrorLe (range : CheckedNodeRange) (exact : NN.IR.DVal ℝ) (computed : NN.IR.DVal TorchLean.Floats.IEEE754.IEEE32Exec) : Prop

Pointwise approximation relation for real and IEEE dynamic graph values at one certificate row.

theorem Proofs.RuntimeApprox.NumericalCertificate.dval_error_le_of_range_check {range : CheckedNodeRange} {exact : NN.IR.DVal ℝ} {computed : NN.IR.DVal TorchLean.Floats.IEEE754.IEEE32Exec} (hexact : RealDValEnclosed range exact) (hcomputed : dvalWithinRange range computed = true) : DValErrorLe range exact computed

One successful dynamic replay row yields a pointwise error bound whenever the corresponding real graph value has the proved enclosure.

def Proofs.RuntimeApprox.NumericalCertificate.executionWithinRangesList : List CheckedNodeRange → List (NN.IR.DVal TorchLean.Floats.IEEE754.IEEE32Exec) → Bool

List-level replay check. Its structural recursion is also the proof interface for composing per-node numerical guarantees over a complete execution trace.

def Proofs.RuntimeApprox.NumericalCertificate.executionWithinRanges (ranges : Array CheckedNodeRange) (values : Array (NN.IR.DVal TorchLean.Floats.IEEE754.IEEE32Exec)) : Bool

Check every value produced by IR.Graph.denoteAll against the corresponding certificate row.

theorem Proofs.RuntimeApprox.NumericalCertificate.executionWithinRangesList_eq_true_iff (ranges : List CheckedNodeRange) (values : List (NN.IR.DVal TorchLean.Floats.IEEE754.IEEE32Exec)) : executionWithinRangesList ranges values = true ↔ List.Forall₂ (fun (range : CheckedNodeRange) (value : NN.IR.DVal TorchLean.Floats.IEEE754.IEEE32Exec) => dvalWithinRange range value = true) ranges values

Proof-level meaning of a complete successful IEEE replay trace.

inductive Proofs.RuntimeApprox.NumericalCertificate.ExecutionErrorTrace : List CheckedNodeRange → List (NN.IR.DVal ℝ) → List (NN.IR.DVal TorchLean.Floats.IEEE754.IEEE32Exec) → Prop

Graph-wide pointwise approximation evidence, one row per intermediate value.

• nil : ExecutionErrorTrace [] [] []
• cons {range : CheckedNodeRange} {ranges : List CheckedNodeRange} {exact : NN.IR.DVal ℝ} {exacts : List (NN.IR.DVal ℝ)} {computed : NN.IR.DVal TorchLean.Floats.IEEE754.IEEE32Exec} {computeds : List (NN.IR.DVal TorchLean.Floats.IEEE754.IEEE32Exec)} : DValErrorLe range exact computed → ExecutionErrorTrace ranges exacts computeds → ExecutionErrorTrace (range :: ranges) (exact :: exacts) (computed :: computeds)

theorem Proofs.RuntimeApprox.NumericalCertificate.executionErrorTrace_of_enclosed {ranges : List CheckedNodeRange} {exact : List (NN.IR.DVal ℝ)} {computed : List (NN.IR.DVal TorchLean.Floats.IEEE754.IEEE32Exec)} (hexact : List.Forall₂ RealDValEnclosed ranges exact) (hcomputed : List.Forall₂ (fun (range : CheckedNodeRange) (value : NN.IR.DVal TorchLean.Floats.IEEE754.IEEE32Exec) => dvalWithinRange range value = true) ranges computed) : ExecutionErrorTrace ranges exact computed

Compose real enclosure proofs and successful IEEE replay checks into an error trace.

theorem Proofs.RuntimeApprox.NumericalCertificate.execution_error_trace_of_check {ranges : Array CheckedNodeRange} {exact : Array (NN.IR.DVal ℝ)} {computed : Array (NN.IR.DVal TorchLean.Floats.IEEE754.IEEE32Exec)} (hexact : List.Forall₂ RealDValEnclosed ranges.toList exact.toList) (hcomputed : executionWithinRanges ranges computed = true) : ExecutionErrorTrace ranges.toList exact.toList computed.toList

Array-facing whole-trace theorem used by checked graph executions.

def Proofs.RuntimeApprox.NumericalCertificate.sameNodeRange (checked : CheckedNodeRange) (raw : NodeRange) : Bool

Compare a checked canonical row with untrusted raw certificate data.

def Proofs.RuntimeApprox.NumericalCertificate.parentRange (ranges : Array CheckedNodeRange) (nodeId : ℕ) : Except String TorchLean.Floats.IEEE754.IEEE32Exec.Interval32

Read a previously checked parent enclosure. Graph well-formedness guarantees that successful lookups refer only to earlier rows; the explicit error still protects this API when called alone.

def Proofs.RuntimeApprox.NumericalCertificate.parentNodeRange (ranges : Array CheckedNodeRange) (nodeId : ℕ) : Except String CheckedNodeRange

Read the complete checked row for a parent node.

def Proofs.RuntimeApprox.NumericalCertificate.sumLeftRange (count : ℕ) (range : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32) : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32

Outward-rounded left-fold range for a sum of count values from one enclosure. The initial point interval at positive zero matches Tensor.sumSpec.

def Proofs.RuntimeApprox.NumericalCertificate.meanLeftRange (count : ℕ) (range : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32) : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32

Left-fold mean range, using the same binary32 conversion of the divisor as the tensor context.

def Proofs.RuntimeApprox.NumericalCertificate.nodeNumericalPolicy (plan : NN.Backend.AcceptedGraphPlan) (nodeId : ℕ) : Option NN.Backend.NumericalPolicy

Numerical policy selected for a runtime-relevant graph node.

def Proofs.RuntimeApprox.NumericalCertificate.requireFixedLeftReduction (plan : NN.Backend.AcceptedGraphPlan) (node : NN.IR.Node) : Except String Unit

Reductions are propagated only when the selected capsule promises the same fixed left fold as the canonical tensor semantics. Other schedules need the order-independent reduction bound from NN.Floats.IEEEExec.Reductions and are rejected here rather than mislabeled as deterministic.

def Proofs.RuntimeApprox.NumericalCertificate.matmulInnerDim (left right : Spec.Shape) : Except String ℕ

Inner accumulation length for the rank-2 and batched rank-3 matrix products implemented by IR.Graph.denoteAll. The graph shape checker has already validated matching dimensions; retaining the checks here gives callers of deriveNodeRange a precise error instead of relying on that ambient invariant.

def Proofs.RuntimeApprox.NumericalCertificate.hullParents (ranges : Array CheckedNodeRange) : List ℕ → Except String TorchLean.Floats.IEEE754.IEEE32Exec.Interval32

Hull of a nonempty list of parent ranges.

Graph range contracts

Architectures do not participate in range propagation directly. They lower to NN.IR.Graph, and each graph node is handled by a reusable operation contract. This keeps MLPs, convolutional networks, transformers, and future model families on one checker path: adding a model requires no new certificate traversal, while adding a genuinely new primitive requires one local contract.

The registry is an explicit value rather than global mutable state. Certificate generation and checking therefore use the same inspectable rule set, and downstream projects may extend it without changing TorchLean's graph walker.

inductive Proofs.RuntimeApprox.NumericalCertificate.NumericalOpKey : Type

Stable key for a numerical range contract.

Input-like nodes share the source contract, detach uses the structural identity contract, and runtime operations use the same BackendOp vocabulary as kernel capsules and execution plans.

• source : NumericalOpKey
• structural : NumericalOpKey
• wholeSum : NumericalOpKey
• maxPool : NumericalOpKey
• maxPoolPad : NumericalOpKey
• averagePool : NumericalOpKey
• averagePoolPad : NumericalOpKey
• backend (op : NN.Backend.BackendOp) : NumericalOpKey
• unclassified : NumericalOpKey

@[implicit_reducible]

instance Proofs.RuntimeApprox.NumericalCertificate.instDecidableEqNumericalOpKey : DecidableEq NumericalOpKey

def Proofs.RuntimeApprox.NumericalCertificate.instDecidableEqNumericalOpKey.decEq (x✝ x✝¹ : NumericalOpKey) : Decidable (x✝ = x✝¹)

def Proofs.RuntimeApprox.NumericalCertificate.instReprNumericalOpKey.repr : NumericalOpKey → ℕ → Std.Format

@[implicit_reducible]

instance Proofs.RuntimeApprox.NumericalCertificate.instReprNumericalOpKey : Repr NumericalOpKey

def Proofs.RuntimeApprox.NumericalCertificate.numericalOpKey : NN.IR.OpKind → NumericalOpKey

Classify an IR operation for numerical-contract lookup.

structure Proofs.RuntimeApprox.NumericalCertificate.NumericalRangeContext : Type

Read-only state supplied to one local range transfer.

• sources : Array CheckedSourceRange
• plan : NN.Backend.AcceptedGraphPlan
• ranges : Array CheckedNodeRange

@[reducible, inline]

abbrev Proofs.RuntimeApprox.NumericalCertificate.RangeTransferResult : Type

Result computed by one numerical operation contract.

structure Proofs.RuntimeApprox.NumericalCertificate.GraphRangeContract : Type

Executable range transfer for one operation family.

The proof-facing meaning of the resulting row remains RealDValEnclosed; local soundness lemmas for interval arithmetic and NF approximation are kept in their mathematical modules. The contract contains only executable dispatch and a stable key, so serializable certificates cannot inject proof evidence.

• key : NumericalOpKey
• name : String
• derive : NumericalRangeContext → NN.IR.Node → Except String RangeTransferResult

structure Proofs.RuntimeApprox.NumericalCertificate.GraphRangeRegistry : Type

Deterministic registry used by graph certificate generation and replay.

• name : String
• contracts : List GraphRangeContract

def Proofs.RuntimeApprox.NumericalCertificate.GraphRangeRegistry.empty (name : String) : GraphRangeRegistry

Empty named registry for downstream composition.

def Proofs.RuntimeApprox.NumericalCertificate.GraphRangeRegistry.find? (registry : GraphRangeRegistry) (key : NumericalOpKey) : Option GraphRangeContract

Find the unique contract associated with a numerical operation key.

def Proofs.RuntimeApprox.NumericalCertificate.GraphRangeRegistry.register (registry : GraphRangeRegistry) (contract : GraphRangeContract) : Except String GraphRangeRegistry

Add one contract, rejecting duplicate keys so dispatch never depends on list order.

def Proofs.RuntimeApprox.NumericalCertificate.GraphRangeRegistry.ofList (name : String) (contracts : List GraphRangeContract) : Except String GraphRangeRegistry

Build a registry while checking key uniqueness.

structure Proofs.RuntimeApprox.NumericalCertificate.MissingNumericalContract : Type

One graph node for which a numerical registry has no local transfer.

• nodeId : ℕ
• operation : String
• key : NumericalOpKey

def Proofs.RuntimeApprox.NumericalCertificate.instReprMissingNumericalContract.repr : MissingNumericalContract → ℕ → Std.Format

@[implicit_reducible]

instance Proofs.RuntimeApprox.NumericalCertificate.instReprMissingNumericalContract : Repr MissingNumericalContract

structure Proofs.RuntimeApprox.NumericalCertificate.NumericalCoverageReport : Type

Architecture-independent coverage report obtained after lowering a model to NN.IR.Graph.

• registryName : String
• nodeCount : ℕ
• coveredCount : ℕ
• missing : List MissingNumericalContract

def Proofs.RuntimeApprox.NumericalCertificate.instReprNumericalCoverageReport.repr : NumericalCoverageReport → ℕ → Std.Format

@[implicit_reducible]

instance Proofs.RuntimeApprox.NumericalCertificate.instReprNumericalCoverageReport : Repr NumericalCoverageReport

def Proofs.RuntimeApprox.NumericalCertificate.numericalCoverage (registry : GraphRangeRegistry) (graph : NN.IR.Graph) : NumericalCoverageReport

Inspect contract coverage without attempting interval propagation.

def Proofs.RuntimeApprox.NumericalCertificate.requireNumericalCoverage (registry : GraphRangeRegistry) (graph : NN.IR.Graph) : Except String NumericalCoverageReport

Reject a graph before propagation when any primitive lacks a numerical contract.

def Proofs.RuntimeApprox.NumericalCertificate.arityError (contractName : String) (node : NN.IR.Node) (expected : String) : String

Standard diagnostic for a contract whose graph arity does not match its operation.

def Proofs.RuntimeApprox.NumericalCertificate.sourceContract : GraphRangeContract

Shared source-node contract. The source interval remains an explicit certificate assumption.

def Proofs.RuntimeApprox.NumericalCertificate.structuralContract : GraphRangeContract

Structural identity used by detach.

def Proofs.RuntimeApprox.NumericalCertificate.preserveContract (op : NN.Backend.BackendOp) : GraphRangeContract

Reusable contract constructor for value-preserving graph operations.

def Proofs.RuntimeApprox.NumericalCertificate.binaryContract (op : NN.Backend.BackendOp) (rule : ℕ → ℕ → RangeRule) (transfer : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32 → TorchLean.Floats.IEEE754.IEEE32Exec.Interval32 → TorchLean.Floats.IEEE754.IEEE32Exec.Interval32) : GraphRangeContract

Reusable contract constructor for pointwise binary interval operations.

def Proofs.RuntimeApprox.NumericalCertificate.hullContract (op : NN.Backend.BackendOp) : GraphRangeContract

Reusable contract for operations whose output is enclosed by the hull of their parents.

def Proofs.RuntimeApprox.NumericalCertificate.maxPoolContract : GraphRangeContract

Max pooling without padding selects existing values and therefore preserves the input hull.

def Proofs.RuntimeApprox.NumericalCertificate.maxPoolPadContract : GraphRangeContract

Padded max pooling may additionally select the padding value zero.

def Proofs.RuntimeApprox.NumericalCertificate.averagePoolContract (padded : Bool) : GraphRangeContract

Shared average-pooling contract constructor.

def Proofs.RuntimeApprox.NumericalCertificate.inverseContract : GraphRangeContract

Reciprocal contract with an explicit nonzero-domain check.

def Proofs.RuntimeApprox.NumericalCertificate.sumContract : GraphRangeContract

Whole-tensor fixed-left sum contract.

def Proofs.RuntimeApprox.NumericalCertificate.axisReductionContract (mean : Bool) : GraphRangeContract

Axis reduction contract shared by sum and mean.

def Proofs.RuntimeApprox.NumericalCertificate.matmulContract : GraphRangeContract

Matrix multiplication contract using the selected fixed-left accumulation schedule.

def Proofs.RuntimeApprox.NumericalCertificate.mseContract : GraphRangeContract

Mean-squared-error contract with nonnegativity restored after dependent squaring.

def Proofs.RuntimeApprox.NumericalCertificate.layerNormContract : GraphRangeContract

Pure LayerNorm contract over an arbitrary normalized suffix.

def Proofs.RuntimeApprox.NumericalCertificate.softmaxContract : GraphRangeContract

Softmax contract: exact-real outputs lie in the unit interval on every nonempty axis.

def Proofs.RuntimeApprox.NumericalCertificate.reluContract : GraphRangeContract

ReLU interval contract.

def Proofs.RuntimeApprox.NumericalCertificate.absContract : GraphRangeContract

Absolute-value interval contract.

def Proofs.RuntimeApprox.NumericalCertificate.sqrtContract : GraphRangeContract

Square-root contract with a checked nonnegative domain.

def Proofs.RuntimeApprox.NumericalCertificate.boundedUnaryContract (op : NN.Backend.BackendOp) (rule : ℕ → RangeRule) (enclosure : TorchLean.Floats.IEEE754.IEEE32Exec.Interval32) : GraphRangeContract

Constructor for bounded transcendental contracts.

def Proofs.RuntimeApprox.NumericalCertificate.defaultContracts : List GraphRangeContract

Built-in numerical contracts. Grouping is by operation semantics, never by architecture.

def Proofs.RuntimeApprox.NumericalCertificate.defaultRegistry : Except String GraphRangeRegistry

TorchLean's built-in numerical registry. Construction is checked once at use sites so a future duplicate produces an explicit configuration failure.

def Proofs.RuntimeApprox.NumericalCertificate.deriveNodeRangeWith (registry : GraphRangeRegistry) (sources : Array CheckedSourceRange) (plan : NN.Backend.AcceptedGraphPlan) (ranges : Array CheckedNodeRange) (node : NN.IR.Node) : Except String RangeTransferResult

Compute one node range using an explicit numerical contract registry.

def Proofs.RuntimeApprox.NumericalCertificate.deriveNodeRange (sources : Array CheckedSourceRange) (plan : NN.Backend.AcceptedGraphPlan) (ranges : Array CheckedNodeRange) (node : NN.IR.Node) : Except String RangeTransferResult

Compute one node range using TorchLean's built-in registry.

def Proofs.RuntimeApprox.NumericalCertificate.buildRangeTraceWith (registry : GraphRangeRegistry) (graph : NN.IR.Graph) (sources : Array CheckedSourceRange) (plan : NN.Backend.AcceptedGraphPlan) : Except String (Array CheckedNodeRange)

Construct and validate the canonical range trace using an explicit contract registry.

def Proofs.RuntimeApprox.NumericalCertificate.buildRangeTrace (graph : NN.IR.Graph) (sources : Array CheckedSourceRange) (plan : NN.Backend.AcceptedGraphPlan) : Except String (Array CheckedNodeRange)

Construct and validate the canonical range trace using TorchLean's built-in contracts.

def Proofs.RuntimeApprox.NumericalCertificate.eraseRangeTrace (ranges : Array CheckedNodeRange) : Array NodeRange

Erase validity proofs from a checked trace.

def Proofs.RuntimeApprox.NumericalCertificate.sameRangeTrace (checked : Array CheckedNodeRange) (raw : Array NodeRange) : Bool

Compare a canonical checked trace with untrusted raw rows.

Backend-linked graph certificates

structure Proofs.RuntimeApprox.NumericalCertificate.GraphNumericalCertificate : Type

Untrusted certificate data.

The audit field records the data selected by backend planning. The checker replans the graph under profileName and compares the complete audit, so an artifact cannot choose its own provider, trust level, or evidence classification.

• profileName : String
• registryName : String
• sources : Array SourceRange
• ranges : Array NodeRange
• audit : NN.Backend.ExecutionAudit

@[implicit_reducible]

instance Proofs.RuntimeApprox.NumericalCertificate.instReprGraphNumericalCertificate : Repr GraphNumericalCertificate

structure Proofs.RuntimeApprox.NumericalCertificate.CheckedCertificate : Type

Proof-carrying result returned by check. Raw endpoint data has been replaced by the canonical trace reconstructed from the graph, and backendPlan contains the acceptance-gate proof.

• graph : NN.IR.Graph

  The exact graph whose ranges and backend plan were reconstructed by the checker.

• raw : GraphNumericalCertificate

  The untrusted artifact supplied to the checker, retained for inspection and serialization.

• sources : Array CheckedSourceRange

  Source assumptions whose interval endpoints have been proved finite and ordered.

• ranges : Array CheckedNodeRange

  The canonical node-by-node range trace reconstructed from the graph.

• backendPlan : NN.Backend.AcceptedGraphPlan

  The backend plan accepted when the checker replanned graph.

• rangesMatch : sameRangeTrace self.ranges self.raw.ranges = true

  Proof that the reconstructed trace matches every range row claimed by raw.

• auditMatch : self.backendPlan.audit = self.raw.audit

  Proof that the accepted plan's audit is the one stored in raw.

@[implicit_reducible]

instance Proofs.RuntimeApprox.NumericalCertificate.instReprCheckedCertificate : Repr CheckedCertificate

structure Proofs.RuntimeApprox.NumericalCertificate.CheckedExecution : Type

Result of executing the canonical IR with bit-level binary32 semantics and replaying every intermediate value against a checked numerical certificate.

• certificate : CheckedCertificate
• values : Array (NN.IR.DVal TorchLean.Floats.IEEE754.IEEE32Exec)
• withinRanges : executionWithinRanges self.certificate.ranges self.values = true

def Proofs.RuntimeApprox.NumericalCertificate.toRaw (profile : NN.Backend.BackendProfile) (registry : GraphRangeRegistry) (sources : Array SourceRange) (ranges : Array CheckedNodeRange) (plan : NN.Backend.AcceptedGraphPlan) : GraphNumericalCertificate

Convert an accepted backend plan and checked range trace into raw certificate data.

def Proofs.RuntimeApprox.NumericalCertificate.acceptedPlan (profile : NN.Backend.BackendProfile) (graph : NN.IR.Graph) : Except String NN.Backend.AcceptedGraphPlan

Obtain an accepted backend plan or report the acceptance-gate failures.

def Proofs.RuntimeApprox.NumericalCertificate.generateWith (registry : GraphRangeRegistry) (profile : NN.Backend.BackendProfile) (graph : NN.IR.Graph) (sources : Array SourceRange) : Except String GraphNumericalCertificate

Generate a canonical certificate using an explicit numerical operation registry.

def Proofs.RuntimeApprox.NumericalCertificate.generate (profile : NN.Backend.BackendProfile) (graph : NN.IR.Graph) (sources : Array SourceRange) : Except String GraphNumericalCertificate

Generate a canonical certificate using TorchLean's built-in numerical contracts.

def Proofs.RuntimeApprox.NumericalCertificate.checkWith (registry : GraphRangeRegistry) (profile : NN.Backend.BackendProfile) (graph : NN.IR.Graph) (raw : GraphNumericalCertificate) : Except String CheckedCertificate

Check an untrusted certificate with an explicit numerical operation registry.

def Proofs.RuntimeApprox.NumericalCertificate.check (profile : NN.Backend.BackendProfile) (graph : NN.IR.Graph) (raw : GraphNumericalCertificate) : Except String CheckedCertificate

Check an untrusted certificate using TorchLean's built-in numerical contracts.

def Proofs.RuntimeApprox.NumericalCertificate.generateChecked (profile : NN.Backend.BackendProfile) (graph : NN.IR.Graph) (sources : Array SourceRange) : Except String CheckedCertificate

Generate and immediately check a certificate. This is convenient for in-process callers and ensures examples exercise exactly the same checker used for imported artifacts.

def Proofs.RuntimeApprox.NumericalCertificate.generateCheckedWith (registry : GraphRangeRegistry) (profile : NN.Backend.BackendProfile) (graph : NN.IR.Graph) (sources : Array SourceRange) : Except String CheckedCertificate

Generate and immediately check with one explicit registry.

def Proofs.RuntimeApprox.NumericalCertificate.executeIEEE32 (payload : NN.IR.Payload TorchLean.Floats.IEEE754.IEEE32Exec) (input : NN.IR.DVal TorchLean.Floats.IEEE754.IEEE32Exec) (certificate : CheckedCertificate) : Except String CheckedExecution

Execute a graph under IEEE32Exec and check all intermediate tensors against the certificate.

This reference replay path gives imported runtime artifacts a bit-level oracle. The backend audit records the capsules and numerical policies selected when the graph is replanned. The audit is not runtime provenance and does not prove that those kernels produced the imported values.

structure Proofs.RuntimeApprox.NumericalCertificate.CheckedRealExecution (certificate : CheckedCertificate) : Type

Exact-real execution evidence for the graph stored in a checked certificate.

The numerical checker reconstructs interval transfers, while a semantic proof establishes that the real graph trace lies in those intervals. Keeping this proof separate prevents successful endpoint replay from being mistaken for a theorem about an unsupported real operation.

• payload : NN.IR.Payload ℝ

  Real-valued constants and external tensors used by the graph execution.

• input : NN.IR.DVal ℝ

  Real-valued graph input.

• values : Array (NN.IR.DVal ℝ)

  Complete real-valued node trace, in graph order.

• denotation : certificate.graph.denoteAll self.payload self.input = Except.ok self.values

  Evidence that values is exactly the graph's denotational execution trace.

• enclosed : List.Forall₂ RealDValEnclosed certificate.ranges.toList self.values.toList

  Pointwise evidence that every real node value lies in its checked interval.

theorem Proofs.RuntimeApprox.NumericalCertificate.CheckedExecution.errorTrace (execution : CheckedExecution) (exact : CheckedRealExecution execution.certificate) : ExecutionErrorTrace execution.certificate.ranges.toList exact.values.toList execution.values.toList

Pair a checked IEEE replay with a proved real enclosure trace to obtain a graph-wide, pointwise error trace. Each node's error budget is the width of its checked outward interval.