Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generatedaudited 2026-08-29
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The standard relative floating-point model and unit roundoff

Definition

A floating-point system. A floating-point system consists of a nonempty finite set F⊆R of representable numbers with 0∈F and −F=F, a positive real Nmax⁡∈F (the largest normal magnitude), a positive real Nmin⁡∈F (the smallest normal magnitude), with Nmin⁡≤Nmax⁡, and a rounding map fl⁡ defined on 0 and on the real numbers t with Nmin⁡≤∣t∣≤Nmax⁡, taking values in F and satisfying fl⁡(0)=0.

Unit roundoff. A real u>0 is a unit roundoff for the system when every real t with Nmin⁡≤∣t∣≤Nmax⁡ satisfies

fl⁡(t)=t(1+δ)for some δ with ∣δ∣≤u,

with ∣⋅∣ the absolute value (Absolute value in an ordered field). The model quantifies all subsequent error analysis through the single constant u and says nothing about the internal bit representation beyond the bound ∣δ∣≤u.

The standard relative model. For each operation ∘∈{+,−,×,÷} and all x,y∈F such that x∘y is zero or is a real number in the normal range (Nmin⁡≤∣x∘y∣≤Nmax⁡; for ÷ this includes y≠0), the computed result is

fl⁡(x∘y)=(x∘y)(1+δ)for some δ with ∣δ∣≤u.

When x∘y=0, this identity is the exact-zero rule fl⁡(0)=0 and one may take δ=0.

The exclusions are part of the model, and are stated explicitly.

  • Overflow is excluded: when ∣x∘y∣>Nmax⁡ the result is not a real number of the form (x∘y)(1+δ) with ∣δ∣≤u.
  • Underflow is excluded: when 0<∣x∘y∣<Nmin⁡ the result falls into the subnormal or lost range and need not satisfy the relative bound.
  • Invalid operations are excluded: when x∘y is not a real number (for example 0/0), there is no real δ for the displayed identity.

Every item on this page that uses the model therefore carries the hypotheses that the relevant operations lie in the normal range, and statements about overflow, underflow or invalid operations are made only where the exclusion is mentioned.

Remarks

  • The running example. In the IEEE-754 binary64 system the unit roundoff is u=2−53, the largest normal magnitude is Nmax⁡=(2−2−52) 21023≈1.798⋅10308, and the smallest normal magnitude is Nmin⁡=2−1022. The counterexample page uses these three numbers to exhibit the excluded events.

  • The exclusions are needed, not decorative. Each excluded event genuinely produces a value that is not of the form (x∘y)(1+δ) with ∣δ∣≤u: overflow at ((3/2)21023)⋅2 gives +∞, underflow at 2−1074/2 rounds to 0, and 0/0 gives NaN⁡.

  • The model is an assumption, not a theorem about hardware. Statements proved under this model are conditional on the displayed inequalities; they say "if every operation rounds this accurately, then the following error bound holds". That is exactly what makes the bounds of The computed floating-point dot product obeys componentwise and normwise error bounds transportable to any hardware conforming to the model.

Depends on

Used by

Dependency tree · two levels

2 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources