ScaleApprox

Scale-aware approximation helpers.

This module adds an optional layer that tracks a per-tensor "scale bound" (a nonnegative bound on linf_norm) alongside the existing eps error bounds.

It is designed to be used to derive readable abs+rel tolerances from existing eps-style proofs: given an error budget eps and a scale bound B, we can form an ApproxTol whose rel component is computed from (eps / B) (with safe handling of B = 0).

Nothing here changes existing forward/backward frameworks; it only provides new predicates and lemmas you can opt into.

PyTorch correspondence / citations

This is the proof-oriented analogue of reasoning with a magnitude/scale estimate (e.g. ‖x‖∞ ≤ B) to turn an absolute error budget into an rtol-style relative tolerance. https://pytorch.org/docs/stable/generated/torch.allclose.html

inductive Proofs.RuntimeApprox.BList : List Spec.Shape → Type

Nonnegative scale bounds aligned with a context shape list.

• nil : BList []
• cons {s : Spec.Shape} {ss : List Spec.Shape} : NNReal → BList ss → BList (s :: ss)

def Proofs.RuntimeApprox.BList.cast {ss₁ ss₂ : List Spec.Shape} (h : ss₁ = ss₂) (xs : BList ss₁) : BList ss₂

Transport a BList along an equality of the underlying shape lists.

@[simp]

theorem Proofs.RuntimeApprox.BList.cast_rfl {ss : List Spec.Shape} (xs : BList ss) : cast ⋯ xs = xs

def Proofs.RuntimeApprox.BList.snoc {τ : Spec.Shape} {ss : List Spec.Shape} : BList ss → NNReal → BList (ss ++ [τ])

Append one additional scale bound at the end of a BList.

def Proofs.RuntimeApprox.BList.unsnoc {τ : Spec.Shape} {ss : List Spec.Shape} : BList (ss ++ [τ]) → BList ss × NNReal

Split a BList (ss ++ [τ]) into its prefix and the last bound.

@[simp]

theorem Proofs.RuntimeApprox.BList.unsnoc_snoc {ss : List Spec.Shape} {τ : Spec.Shape} (xs : BList ss) (e : NNReal) : (xs.snoc e).unsnoc = (xs, e)

def Proofs.RuntimeApprox.BList.get {ss : List Spec.Shape} : BList ss → (i : Fin ss.length) → NNReal

Get the ith scale bound from a BList (using the Fin ss.length index).

def Proofs.RuntimeApprox.scaleWith {α : Type} {s : Spec.Shape} (toSpec : α → Spec.SpecScalar) (norm : {s : Spec.Shape} → Spec.SpecTensor s → Spec.SpecScalar) (spec : Spec.SpecTensor s) (runtime : Spec.Tensor α s) (B : NNReal) : Prop

A scale bound says both spec and runtime (mapped to spec) norms are bounded by B.

def Proofs.RuntimeApprox.scaleT {α : Type} {s : Spec.Shape} (toSpec : α → Spec.SpecScalar) (spec : Spec.SpecTensor s) (runtime : Spec.Tensor α s) (B : NNReal) : Prop

Default scale predicate on tensors (uses linf_norm).

def Proofs.RuntimeApprox.scaleCtx {α : Type} (toSpec : α → Spec.SpecScalar) {ss : List Spec.Shape} : TList Spec.SpecScalar ss → TList α ss → BList ss → Prop

Context-level scale predicate aligned with a BList.

theorem Proofs.RuntimeApprox.scaleCtx_cast {α : Type} {toSpec : α → Spec.SpecScalar} {ss₁ ss₂ : List Spec.Shape} (h : ss₁ = ss₂) {xS : TList Spec.SpecScalar ss₁} {xR : TList α ss₁} {bs : BList ss₁} : scaleCtx toSpec xS xR bs → scaleCtx toSpec (TList.cast h xS) (TList.cast h xR) (BList.cast h bs)

theorem Proofs.RuntimeApprox.scaleCtx_snoc {α : Type} {toSpec : α → Spec.SpecScalar} {ss : List Spec.Shape} {τ : Spec.Shape} {xS : TList Spec.SpecScalar ss} {xR : TList α ss} {bs : BList ss} (hx : scaleCtx toSpec xS xR bs) {yS : Spec.SpecTensor τ} {yR : Spec.Tensor α τ} {b : NNReal} (hy : scaleT toSpec yS yR b) : scaleCtx toSpec (TList.snoc xS yS) (TList.snoc xR yR) (bs.snoc b)

theorem Proofs.RuntimeApprox.scaleCtx_unsnoc {α : Type} {toSpec : α → Spec.SpecScalar} {ss : List Spec.Shape} {τ : Spec.Shape} {xS : TList Spec.SpecScalar (ss ++ [τ])} {xR : TList α (ss ++ [τ])} {bs : BList (ss ++ [τ])} : scaleCtx toSpec xS xR bs → scaleCtx toSpec (TList.unsnoc xS).1 (TList.unsnoc xR).1 bs.unsnoc.1 ∧ scaleT toSpec (TList.unsnoc xS).2 (TList.unsnoc xR).2 bs.unsnoc.2

theorem Proofs.RuntimeApprox.scaleCtx_get {α : Type} {toSpec : α → Spec.SpecScalar} {Γ : List Spec.Shape} {xS : TList Spec.SpecScalar Γ} {xR : TList α Γ} {bs : BList Γ} (h : scaleCtx toSpec xS xR bs) (i : Fin Γ.length) : scaleT toSpec (TList.get xS i) (TList.get xR i) (bs.get i)

noncomputable def Proofs.RuntimeApprox.tolFromEpsScale (eps : ℝ) (B : NNReal) : ApproxTol

A derived tolerance from an absolute error eps and a scale bound B.

We always keep the absolute component (abs = eps) for safety. The relative component is computed as eps / B (with a B = 0 guard) and then clamped to be nonnegative via toNNReal inside ApproxTol.ofReal.

theorem Proofs.RuntimeApprox.absOnly_le_tolFromEpsScale (eps : ℝ) (B : NNReal) : (ApproxTol.absOnly eps).abs ≤ (tolFromEpsScale eps B).abs ∧ (ApproxTol.absOnly eps).rel ≤ (tolFromEpsScale eps B).rel ∧ (ApproxTol.absOnly eps).slack ≤ (tolFromEpsScale eps B).slack

theorem Proofs.RuntimeApprox.approxTTol_from_scale {α : Type} {s : Spec.Shape} {toSpec : α → Spec.SpecScalar} {spec : Spec.SpecTensor s} {runtime : Spec.Tensor α s} (eps : ℝ) (B : NNReal) (h : approxT toSpec spec runtime eps) : approxTTol toSpec spec runtime (tolFromEpsScale eps B)

theorem Proofs.RuntimeApprox.approxCtx_get_tolFromEpsScale {α : Type} {toSpec : α → Spec.SpecScalar} {Γ : List Spec.Shape} {xS : TList Spec.SpecScalar Γ} {xR : TList α Γ} {eps : EList Γ} {bs : BList Γ} (hε : approxCtx toSpec xS xR eps) (_hB : scaleCtx toSpec xS xR bs) (i : Fin Γ.length) : approxTTol toSpec (TList.get xS i) (TList.get xR i) (tolFromEpsScale (eps.get i) (bs.get i))