Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 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.

A cancellation-prone formula can be replaced by a stable reformulation

Example

Evaluate f(z)=1−1−z at z=10−8 under the standard relative model with unit roundoff u (The standard relative floating-point model and unit roundoff). The direct formula 1−1−z subtracts the nearby numbers 1 and 1−z≈1−5⋅10−9 and loses about eight decimal digits; the algebraically equivalent form

f(z)=z1+1−z

subtracts nothing and evaluates to full accuracy. Cancellation is a property of the formula, and a stable reformulation removes it without changing the mathematical function.

Facts & Assumptions

Given: The parameter z=10−8, the value w=1−z>0, the unit roundoff u with 0<u<1/2, and the two formulas g(z)=1−1−z and h(z)=z/(1+1−z).

[L1]

The relative model: each operation obeys fl⁡(t)=t(1+δ) with ∣δ∣≤u when t lies in the normal range (The standard relative floating-point model and unit roundoff).

[L2]

Relative forward error of a computed value y^ for the exact answer f(z) is ∣y^−f(z)∣/∣f(z)∣ (Absolute and relative forward error for an approximate value of a problem map).

Verification

technique · direct
1.1algebra

The two formulas agree exactly: z/(1+w)=(1−w)(1+w)/(1+w)=1−w, because z=1−w2 and 1+w>0.

1.2algebra

For z=10−8, the exact value is f(z)=1−w≈5⋅10−9: indeed (1−5⋅10−9)2=1−10−8+25⋅10−18>1−z, so w<1−5⋅10−9, while (1−6⋅10−9)2=1−12⋅10−9+36⋅10−18<1−z, so w>1−6⋅10−9; hence 1−w∈(5⋅10−9, 6⋅10−9).

1.3L1algebra

The direct formula. By [L1] the computed values are fl⁡(w)=w(1+δ1) and fl⁡(1−fl⁡(w))=(1−w(1+δ1))(1+δ2) with ∣δ1∣,∣δ2∣≤u; subtracting the exact value 1−w leaves an error of absolute value ∣δ2(1−w)−δ1w(1+δ2)∣≤u(1−w)+uw(1+u).

1.4L1algebra

The reformulated formula. By [L1], the computed values are fl⁡(1+w)=(1+w)(1+δ3) for the denominator and fl⁡(z/fl⁡(1+w))=z(1+w)(1+δ3)(1+δ4) for the quotient, with ∣δ3∣,∣δ4∣≤u.

2.1L2step 1.3algebra

By [L2], the relative error of the direct formula is at most u+u w(1+u)/(1−w); with w≈1 and 1−w≈5⋅10−9 this is about u(1+2⋅108), roughly 2⋅108 u: with u=2−53 the relative forward error can reach about 2⋅10−8, losing about eight of the roughly sixteen decimal digits of relative precision available in binary64.

2.2L2step 1.4algebra

By [L2], the relative error of the reformulated value is ∣(1+δ4)/(1+δ3)−1∣=∣δ4−δ3∣/∣1+δ3∣≤2u/(1−u), which is of order u, not of order 108u: no subtraction of nearby quantities occurs, and the reformulation evaluates f to full relative accuracy.

3.1step 2.1step 2.2∎

Steps 2.1 and 2.2 compare the same function evaluated two ways: the direct formula amplifies roundoff by the cancellation factor 1/(1−w)≈2⋅108, while the rationalized formula keeps the error at order u.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

4 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