NF Scalar Primitive Bounds #
Scalar bridge lemmas and forward-error bounds for rounded NF primitives. These are the facts
that later tensor proofs lift pointwise across shapes.
Interpret a runtime NF scalar as a spec scalar (ℝ) by forgetting rounding metadata.
Instances For
max on NF is a pure selection, so forgetting the format commutes with maximum exactly.
Constructing an NF value from a real incurs at most one half ULP.
This is the canonical bridge for rounded constants and casts. Keeping it next to toSpec avoids
repeating the implementation-level NF.ofReal unfolding in attention scales, optimizer
hyperparameters, and quantization parameters.
Casting an exact rational constant rounds its real value once.
This supplies the epsilon-constant hypothesis for normalization without first rounding a potentially unrepresentable natural denominator. Positivity still needs a separate argument.
Bridge lemmas from NF to $\mathbb R$ #
Most approximation statements in this file are phrased over the spec scalar ℝ, but the runtime
backend is NF β fexp rnd. The following lemmas are small bridge facts that let us rewrite
runtime expressions into:
- an exact real expression in terms of
toSpec, plus - an explicit rounding operator
roundRapplied at the outermost step.
Keeping these as named lemmas (instead of repeating huge simp [...] lists) makes the later
forward-approx proofs much easier to read.
toSpec of runtime 0 is the spec scalar 0.
toSpec respects runtime exp, up to an explicit rounding step.
Forward approximation bound for sqrt (max · 0) under a positive lower bound.
This is a clamped sqrt bound: we work with sqrt (max x 0) to avoid the sqrt domain issue, but
still require a strict lower bound η > 0 on max x 0 to control conditioning via
|√a - √b| ≤ |a-b| / √η.
Forward approximation bound for addition in NF.
In words: if xR approximates x within epsx and yR approximates y within epsy,
then xR + yR approximates x + y within epsx + epsy + ulp(toSpec xR + toSpec yR)/2.
Forward approximation bound for subtraction in NF.
This is proved by reducing subtraction to addition with a negation and applying approx_add_nf.
Forward approximation bound for negation in NF (rounding error on -toSpec xR).
Forward approximation bound for absolute value in NF (abs is pure + a final rounding).
Forward-error budget for one rounded exponential.
The first term propagates an input error eps through exp; the second pays for the final
rounding. In particular, exact input contributes no propagation error. This definition is shared
by scalar activations, tensor lifting, and stable axis softmax so that all three use the same
numerical contract.
Instances For
Forward approximation bound for exp in NF.
Uses the mean value theorem for Real.exp to bound the propagation of input error, then adds one
rounding-ULP term for the final NF rounding.
Forward approximation bound for tanh in NF (coarse but unconditional).
Because tanh is bounded in [-1, 1], we always have |tanh(toSpec xR) - tanh(x)| ≤ 2, and then
we add one rounding-ULP term for the final NF rounding step.
Clamped log on spec scalars: log (max x ε).
This is used to obtain unconditional forward bounds for log by avoiding the singularity at 0.
Instances For
Clamped log on runtime NF scalars (implemented as NF.ofReal (safeLog (toSpec xR))).
This definition keeps the semantic spec function explicit (so proofs can reason about it) while still producing an executable runtime scalar.
Instances For
Forward approximation bound for safeLog in NF.
On the clamped domain u,v ≥ ε > 0, log is (1/ε)-Lipschitz. We use that to propagate the input
error and then add one rounding-ULP term for the final NF rounding.
Forward approximation bound for ordinary square root on a certified positive domain.
The extra runtime hypothesis is not cosmetic: the executable NF.sqrt receives the rounded input,
so a real lower bound alone does not rule out an invalid rounded argument. Once both exact and
runtime inputs are nonnegative, the clamped theorem above reduces definitionally to ordinary
square root.
Square-root approximation when the input error budget itself certifies runtime positivity.
From η ≤ x, |x̂-x| ≤ eps, and eps < η, the rounded input satisfies 0 < x̂; callers do not
need a separate runtime-domain hypothesis. This is the form used by normalization certificates.
Forward approximation bound for multiplication in NF.
This has the standard "first-order" shape:
terms proportional to |toSpec xR| * epsy and |toSpec yR| * epsx, plus an ulp term for the
final
rounding. (For classical background, see Higham, Accuracy and Stability of Numerical Algorithms.)
Forward approximation bound for scaling (elementwise multiply by a runtime constant c).