NF Scalar Primitive Bounds #
Scalar bridge lemmas and forward-error bounds for rounded NF primitives, lifted pointwise
by the tensor proofs. This is a noncomputable rounded-real model, not a native-kernel proof.
An NF value need not be representable in its format, so even negation and absolute value
include a rounding term.
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$ #
The bridge lemmas express each NF operation as a real calculation followed by rounding.
toSpec of runtime 0 is the spec scalar 0: every valid rounder fixes the integer 0.
toSpec respects runtime exp, up to an explicit rounding step.
The clamped square-root error is bounded even at zero, without a positive input margin.
The sqrt eps term uses the square root's Hölder bound; rounding adds one half-ULP.
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.
The argument is the one behind scalarApprox_roundedAdd: the exact difference of the runtime
operands is within epsx + epsy of x - y, and the runtime result is one rounding away from that
exact difference.
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 in the rounded-real NF model: evaluate safeLog and round once.
This definition is noncomputable; it does not implement a native logarithm.
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.
Nonnegativity of the represented input lets the clamped bound reduce to ordinary square root.
The underlying Real.sqrt is total, returning zero for negative arguments; this hypothesis
describes the theorem's domain, not an IEEE invalid-operation check.
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.
Includes both input perturbations, their cross terms, and one half-ULP rounding term.
Forward approximation bound for scaling (elementwise multiply by a runtime constant c).