ScaleApprox

Scale-aware approximation helpers.

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

An absolute budget eps and a reference magnitude B give an abs-plus-rel tolerance whose relative coefficient is eps / B (zero when B = 0). The full absolute budget is retained, so this conversion weakens the tolerance; it does not establish a relative-only error bound. Its soundness does not require a magnitude proof. Actual magnitude propagation uses the separate scaleTensor and scaleCtx predicates.

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

Scale vectors aligned with contexts

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

Transporting along rfl is the identity.

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)

unsnoc undoes snoc.

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).

Scale predicates (single tensor and contexts)

def Proofs.RuntimeApprox.scaleWith {α : 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) (B : NNReal) : Prop

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

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

Default scale predicate on tensors (uses linfNorm).

def Proofs.RuntimeApprox.scaleCtx {α : Type} [TorchLean.Storage α] (toSpec : α → Spec.SpecScalar) {ss : List Spec.Shape} : TorchLean.TensorPack Spec.SpecScalar ss → TorchLean.TensorPack α ss → BList ss → Prop

Context-level scale predicate aligned with a BList.

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

The context scale predicate survives transporting all three arguments along the same equality.

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

Appending a tensor with a known scale bound extends the context predicate.

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

Conversely, a predicate on an extended context splits into the prefix part and the last entry.

theorem Proofs.RuntimeApprox.scaleCtx_get {α : Type} [TorchLean.Storage α] {toSpec : α → Spec.SpecScalar} {Γ : List Spec.Shape} {xS : TorchLean.TensorPack Spec.SpecScalar Γ} {xR : TorchLean.TensorPack α Γ} {bs : BList Γ} (h : scaleCtx toSpec xS xR bs) (i : Fin Γ.length) : scaleTensor toSpec (xS.get i) (xR.get i) (bs.get i)

Every entry of a context satisfying scaleCtx satisfies its own scale bound.

Derive abs+rel tolerances from (eps, scale)

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

tolFromEpsScale is at least as permissive as the absolute-only tolerance in every field.

theorem Proofs.RuntimeApprox.approxTensorWithTol_from_scale {α : Type} [TorchLean.Storage α] {s : Spec.Shape} {toSpec : α → Spec.SpecScalar} {spec : Spec.SpecTensor s} {runtime : TorchLean.Tensor α s} (eps : ℝ) (B : NNReal) (h : approxTensor toSpec spec runtime eps) : approxTensorWithTol toSpec spec runtime (tolFromEpsScale eps B)

An absolute tensor bound upgrades to the abs-plus-rel tolerance derived from a scale bound.

theorem Proofs.RuntimeApprox.approxCtx_get_tolFromEpsScale {α : Type} [TorchLean.Storage α] {toSpec : α → Spec.SpecScalar} {Γ : List Spec.Shape} {xS : TorchLean.TensorPack Spec.SpecScalar Γ} {xR : TorchLean.TensorPack α Γ} {eps : EList Γ} (bs : BList Γ) (hε : approxCtx toSpec xS xR eps) (i : Fin Γ.length) : approxTensorWithTol toSpec (xS.get i) (xR.get i) (tolFromEpsScale (eps.get i) (bs.get i))

Per-entry form of the upgrade: each context slot gets the tolerance derived from its own eps and its own scale bound.

As in approxTensorWithTol_from_scale, no scale hypothesis is needed: the derived tolerance is reached purely by weakening the absolute bound. A magnitude proof can justify the chosen reference scale, but an upper magnitude bound does not imply a relative-only error guarantee.