SpecApprox

Spec/runtime approximation bridge with explicit error bounds.

This is a spec-level statement: runtime values are mapped into Real and compared against the spec using a chosen norm.

Trust boundary:

• This file is purely about stating approximation predicates. Turning it into an end-to-end theorem requires per-op approximation lemmas and a composition argument.
• Lean supplies a logical model for Float, but this file does not yet provide per-operation approximation lemmas for that model. Native execution also requires a separate provider agreement. Neither connection is assumed here.
• The intended proof-relevant path is to use rounding-model backends (FloatLib NF) where rounding error bounds are explicit and can be composed.

PyTorch correspondence / citations

Conceptually, approxWith / approxTensorWithTol are theorem-level versions of “runtime tensor is close to spec tensor under a chosen norm”, similar to how PyTorch uses norms and rtol/atol style checks in testing/validation. https://pytorch.org/docs/stable/generated/torch.linalg.vector_norm.html https://pytorch.org/docs/stable/generated/torch.allclose.html

def Proofs.RuntimeApprox.tensorToSpec {α : Type} [TorchLean.Storage α] {s : Spec.Shape} (toSpec : α → Spec.SpecScalar) (t : TorchLean.Tensor α s) : Spec.SpecTensor s

Convert a runtime tensor into the spec scalar by mapping a scalar function.

noncomputable def Proofs.RuntimeApprox.linfNorm {s : Spec.Shape} : Spec.SpecTensor s → Spec.SpecScalar

Linf norm on spec tensors.

def Proofs.RuntimeApprox.approxWith {α : Type} [TorchLean.Storage α] {s : Spec.Shape} (toSpec : α → Spec.SpecScalar) (norm : {s : Spec.Shape} → Spec.SpecTensor s → Spec.SpecScalar) (spec : Spec.SpecTensor s) (runtime : TorchLean.Tensor α s) (eps : Spec.SpecScalar) : Prop

Approximation predicate with an explicit error bound.

def Proofs.RuntimeApprox.approxWithTol {α : Type} [TorchLean.Storage α] {s : Spec.Shape} (toSpec : α → Spec.SpecScalar) (norm : {s : Spec.Shape} → Spec.SpecTensor s → Spec.SpecScalar) (spec : Spec.SpecTensor s) (runtime : TorchLean.Tensor α s) (tol : ApproxTol) : Prop

Abs+rel approximation predicate with a ApproxTol budget (scaled by max ‖spec‖ ‖runtime‖).

def Proofs.RuntimeApprox.approxTensorWithTol {α : Type} [TorchLean.Storage α] {s : Spec.Shape} (toSpec : α → Spec.SpecScalar) (spec : Spec.SpecTensor s) (runtime : TorchLean.Tensor α s) (tol : ApproxTol) : Prop

Default abs+rel tensor approximation (uses linfNorm).

theorem Proofs.RuntimeApprox.approx_with_to_approx_with_tol_absOnly {α : Type} [TorchLean.Storage α] {s : Spec.Shape} {toSpec : α → Spec.SpecScalar} {norm : {s : Spec.Shape} → Spec.SpecTensor s → Spec.SpecScalar} {spec : Spec.SpecTensor s} {runtime : TorchLean.Tensor α s} (eps : ℝ) (h : approxWith toSpec (fun {s : Spec.Shape} => norm) spec runtime eps) : approxWithTol toSpec (fun {s : Spec.Shape} => norm) spec runtime (ApproxTol.absOnly eps)

A plain eps bound is an abs-only tolerance bound.

The clamping in Real.toNNReal only ever weakens the claim, so no sign hypothesis on eps is needed in this direction; the converse approx_with_tol_absOnly_iff does need one.

theorem Proofs.RuntimeApprox.approxTensor_to_approxTensorWithTol_absOnly {α : Type} [TorchLean.Storage α] {s : Spec.Shape} {toSpec : α → Spec.SpecScalar} {spec : Spec.SpecTensor s} {runtime : TorchLean.Tensor α s} (eps : ℝ) (h : approxWith toSpec (fun {s : Spec.Shape} => linfNorm) spec runtime eps) : approxTensorWithTol toSpec spec runtime (ApproxTol.absOnly eps)

The same lift specialized to the default linfNorm tensor relation.

theorem Proofs.RuntimeApprox.approx_with_tol_to_approx_with {α : Type} [TorchLean.Storage α] {s : Spec.Shape} {toSpec : α → Spec.SpecScalar} {norm : {s : Spec.Shape} → Spec.SpecTensor s → Spec.SpecScalar} {spec : Spec.SpecTensor s} {runtime : TorchLean.Tensor α s} {tol : ApproxTol} (h : approxWithTol toSpec (fun {s : Spec.Shape} => norm) spec runtime tol) : approxWith toSpec (fun {s : Spec.Shape} => norm) spec runtime (approxBound tol (norm spec) (norm (tensorToSpec toSpec runtime)))

Conversely, a tolerance bound is a plain bound at the tolerance's own evaluated budget.

theorem Proofs.RuntimeApprox.approx_with_tol_mono {α : Type} [TorchLean.Storage α] {s : Spec.Shape} {toSpec : α → Spec.SpecScalar} {norm : {s : Spec.Shape} → Spec.SpecTensor s → Spec.SpecScalar} {spec : Spec.SpecTensor s} {runtime : TorchLean.Tensor α s} {tol₁ tol₂ : ApproxTol} (habs : tol₁.abs ≤ tol₂.abs) (hrel : tol₁.rel ≤ tol₂.rel) (hslack : tol₁.slack ≤ tol₂.slack) (h : approxWithTol toSpec (fun {s : Spec.Shape} => norm) spec runtime tol₁) : approxWithTol toSpec (fun {s : Spec.Shape} => norm) spec runtime tol₂

Tensor approximation is preserved when the tolerance is weakened in any field.

theorem Proofs.RuntimeApprox.approx_with_tol_absOnly_iff {α : Type} [TorchLean.Storage α] {s : Spec.Shape} {toSpec : α → Spec.SpecScalar} {norm : {s : Spec.Shape} → Spec.SpecTensor s → Spec.SpecScalar} {spec : Spec.SpecTensor s} {runtime : TorchLean.Tensor α s} {eps : ℝ} (heps : 0 ≤ eps) : approxWithTol toSpec (fun {s : Spec.Shape} => norm) spec runtime (ApproxTol.absOnly eps) ↔ approxWith toSpec (fun {s : Spec.Shape} => norm) spec runtime eps

For nonnegative eps the two formulations coincide, so nothing is lost by working with whichever is convenient at each step.

Notation

Use open scoped ApproxTol to enable:

spec ≈ᵀ[toSpec, tol] runtime meaning: approxTensorWithTol toSpec spec runtime tol.

def ApproxTol.«term_≈ᵀ[_,_]_» : Lean.TrailingParserDescr

structure Proofs.RuntimeApprox.Witness (α : Type) [TorchLean.Storage α] (s : Spec.Shape) : Type

Packaged approximation witness (defaults to Linf on spec tensors).

• toSpec : α → Spec.SpecScalar

  Map a runtime scalar into the specification scalar domain.

• spec : Spec.SpecTensor s

  Specification tensor.

• runtime : TorchLean.Tensor α s

  Runtime tensor being compared with the specification tensor.

• eps : Spec.SpecScalar

  Absolute error budget for the Linf comparison.

• bound : approxWith self.toSpec (fun {s : Spec.Shape} => linfNorm) self.spec self.runtime self.eps

  Checked approximation statement connecting spec and runtime.