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.
• For Lean Float, such lemmas would require a formal semantics of IEEE-754 operations; we do not prove those here, so Float execution is treated as trusted.
• The intended proof-relevant path is to use rounding-model backends (NeuralFloat / NF) where rounding error bounds are explicit and can be composed.

PyTorch correspondence / citations

Conceptually, approxWith / approxTTol 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} {s : Spec.Shape} (toSpec : α → Spec.SpecScalar) (t : Spec.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} {s : Spec.Shape} (toSpec : α → Spec.SpecScalar) (norm : {s : Spec.Shape} → Spec.SpecTensor s → Spec.SpecScalar) (spec : Spec.SpecTensor s) (runtime : Spec.Tensor α s) (eps : Spec.SpecScalar) : Prop

Approximation predicate with an explicit error bound.

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

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

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

Default abs+rel tensor approximation (uses linf_norm).

theorem Proofs.RuntimeApprox.approx_with_to_approx_with_tol_absOnly {α : Type} {s : Spec.Shape} {toSpec : α → Spec.SpecScalar} {norm : {s : Spec.Shape} → Spec.SpecTensor s → Spec.SpecScalar} {spec : Spec.SpecTensor s} {runtime : Spec.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)

theorem Proofs.RuntimeApprox.approxT_to_approxTTol_absOnly {α : Type} {s : Spec.Shape} {toSpec : α → Spec.SpecScalar} {spec : Spec.SpecTensor s} {runtime : Spec.Tensor α s} (eps : ℝ) (h : approxWith toSpec (fun {s : Spec.Shape} => linfNorm) spec runtime eps) : approxTTol toSpec spec runtime (ApproxTol.absOnly eps)

theorem Proofs.RuntimeApprox.approx_with_tol_to_approx_with {α : Type} {s : Spec.Shape} {toSpec : α → Spec.SpecScalar} {norm : {s : Spec.Shape} → Spec.SpecTensor s → Spec.SpecScalar} {spec : Spec.SpecTensor s} {runtime : Spec.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)))

theorem Proofs.RuntimeApprox.approx_with_tol_mono {α : Type} {s : Spec.Shape} {toSpec : α → Spec.SpecScalar} {norm : {s : Spec.Shape} → Spec.SpecTensor s → Spec.SpecScalar} {spec : Spec.SpecTensor s} {runtime : Spec.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₂

theorem Proofs.RuntimeApprox.approx_with_tol_absOnly_iff {α : Type} {s : Spec.Shape} {toSpec : α → Spec.SpecScalar} {norm : {s : Spec.Shape} → Spec.SpecTensor s → Spec.SpecScalar} {spec : Spec.SpecTensor s} {runtime : Spec.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

Notation

Use open scoped ApproxTol to enable:

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

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

structure Proofs.RuntimeApprox.Witness (α : Type) (s : Spec.Shape) : Type

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

• toSpec : α → Spec.SpecScalar

  to Spec.

• spec : Spec.SpecTensor s

  spec.

• runtime : Spec.Tensor α s

  runtime.

• eps : Spec.SpecScalar

  eps.

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

  bound.

noncomputable def Proofs.RuntimeApprox.neuralTensorToReal {β : TorchLean.Floats.NeuralRadix} {s : Spec.Shape} (t : Spec.Tensor (TorchLean.Floats.NeuralFloat β) s) : Spec.SpecTensor s

Map NeuralFloat tensors to spec scalars.

noncomputable def Proofs.RuntimeApprox.neuralTensorErrorBound {β : TorchLean.Floats.NeuralRadix} {s : Spec.Shape} (t : Spec.Tensor (TorchLean.Floats.NeuralFloat β) s) : Spec.SpecScalar

Linf bound over NeuralFloat error markers.

def Proofs.RuntimeApprox.neuralRuntimeApprox {β : TorchLean.Floats.NeuralRadix} {s : Spec.Shape} (spec : Spec.SpecTensor s) (runtime : Spec.Tensor (TorchLean.Floats.NeuralFloat β) s) : Prop

NeuralFloat runtime approximation to the spec with explicit epsilon bound.