Numerical approximation and error: absolute error, relative error and tolerance for 0.33 approximating 1/3

Goal and scope

Using exact rationals: compute the absolute and relative error of the approximation a=33/100 to the reference x=1/3; decide whether a is within the tolerances τ₁=1/250, τ₂=1/400 and τ₃=1/300 (τ₃ is the endpoint case); prove |a−x|≤τ ⇔ x−τ≤a≤x+τ; compare the errors after scaling by 1000; explain why relative error is undefined for a zero reference and why an error value alone does not reveal the source of the error.

Everything uses exact rationals (MKO assumption a1); the decimal 0.33 is read as the rational 33/100, and binary floating-point representation is not involved. Relative error is computed only for a nonzero reference (assumption a2). Condition numbers, stability and orders of convergence are not treated; the canonical MKO and its English edition are not changed.

Givens and symbols

• frac_rules
• abs_rules
• order_basics
• mul_inverse_nonzero
• case_analysis

• G1 — Approximation a=33/100 (the decimal 0.33 read as an exact rational), reference x=1/3.
• G2 — Tolerances τ₁=1/250, τ₂=1/400 and τ₃=1/300, all ≥0.
• G3 — A scaled pair: a′=330 and x′=1000/3.
• G4 — A pair with zero reference: a₀=1/1000 and x₀=0.
• G5 — Two ways of producing two decimals: rounding takes the nearest k/100; truncation takes the largest k/100 not exceeding the (positive) number, with k an integer.

• a,\ x — approximation and reference value
• |a-x| — absolute error
• \frac{|a-x|}{|x|} — relative error (x≠0)
• \tau — tolerance, τ≥0
• [x-\tau,\ x+\tau] — tolerance interval (endpoints included)

Rules and sources

• frac_rules · prerequisite — Fraction rules (all denominators nonzero): a/c+b/c=(a+b)/c; (a/b)(c/d)=(ac)/(bd); (a/b)/(c/d)=(ad)/(bc) (also needing c≠0); a/b=(ak)/(bk) for k≠0.
• abs_rules · prerequisite — Absolute value (reals): |u|=u if u≥0 and |u|=−u if u<0; |u|≥0; |uv|=|u||v|; triangle inequality |u+v|≤|u|+|v|; |u|<r ⇔ −r<u<r.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• mul_inverse_nonzero · prerequisite — Inverse of a nonzero number: in ℚ, ℝ or ℂ, if u≠0 there is 1/u with u·(1/u)=1, and v/u means v·(1/u). 0 has no inverse, so v/0 is undefined.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• neg_mul · prerequisite — Signs and multiplication: (−u)v=−(uv) and (−u)(−v)=uv.
• eq_refl_symm_trans · prerequisite — Properties of equality: u=u; if u=v then v=u; if u=v and v=w then u=w.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_error_def · cited — For approximation a and reference x, absolute error is |a−x|. If x≠0, relative error is |a−x|/|x|. For tolerance τ≥0, being within tolerance means |a−x|≤τ. · mko-numerical-approximation-error
• mko_error_sources · cited — An error value by itself does not indicate its source. Distinguishing discretization, truncation, rounding, measurement and model error requires separate data about how the value was produced. · mko-numerical-approximation-error
• frac_compare · prerequisite — Comparing fractions with positive denominators: if b>0 and d>0 then a/b≤c/d ⇔ ad≤cb (multiply both sides by the positive number bd).
• L_tol_interval · lemma — For reals a, x and τ≥0: |a−x|≤τ ⇔ x−τ≤a≤x+τ.

Main derivation

a=\tfrac{33}{100},\ x=\tfrac{1}{3}

e_{\mathrm{abs}}=|a-x|,\ e_{\mathrm{rel}}=\frac{|a-x|}{|x|}\ (x\neq 0),\ \text{within }\tau\iff |a-x|\le\tau

a-x=\tfrac{33}{100}-\tfrac{1}{3}

a-x=-\tfrac{1}{300}

|a-x|=\left|-\tfrac{1}{300}\right|

|a-x|=\tfrac{1}{300}

x=\tfrac{1}{3}

x\neq 0,\ |x|=\tfrac{1}{3}

e_{\mathrm{rel}}=\frac{1/300}{1/3}

e_{\mathrm{rel}}=\tfrac{1}{100}

\tfrac{1}{300}\le\tfrac{1}{250}

250\le 300\ (\text{true}),\ \text{so }a\ \text{within }\tau_1

|a-x|\le\tau

x-\tau\le a\le x+\tau

[x-\tau_1,\ x+\tau_1]

\left[\tfrac{247}{750},\ \tfrac{253}{750}\right]\ni\tfrac{33}{100}

\tfrac{1}{300}\le\tfrac{1}{400}\ ?

400\le 300\ \text{false};\ \tfrac{1}{300}>\tfrac{1}{400};\ a\ \text{not within }\tau_2

|a-x|=\tfrac{1}{300}=\tau_3

|a-x|\le\tau_3,\ a=x-\tau_3\ \text{(left endpoint)}

a'=330,\ x'=\tfrac{1000}{3}

|a'-x'|=\tfrac{10}{3},\ \frac{|a'-x'|}{|x'|}=\tfrac{1}{100}

a_0=\tfrac{1}{1000},\ x_0=0

|a_0-x_0|=\tfrac{1}{1000},\ \frac{|a_0-x_0|}{|x_0|}\ \text{undefined}

\text{error }\tfrac{1}{300}\ \text{for }0.33

\text{rounding and truncation both give }\tfrac{33}{100};\ \text{source not determined by the value}

\text{computed and proved facts}

e_{\mathrm{abs}}=\tfrac{1}{300},\ e_{\mathrm{rel}}=\tfrac{1}{100};\ \text{within }\tau_1,\tau_3;\ \text{not within }\tau_2

Substeps and lemmas

\tfrac{33}{100},\ \tfrac{1}{3}

\tfrac{99}{300},\ \tfrac{100}{300}

\tfrac{99}{300}-\tfrac{100}{300}

-\tfrac{1}{300}

u\ge 0:\ |u|\le\tau

-\tau\le u\le\tau

u<0:\ |u|\le\tau

-\tau\le u\le\tau

|a-x|\le\tau\iff -\tau\le a-x\le\tau

|a-x|\le\tau\iff x-\tau\le a\le x+\tau

Reverse audits

• S14 · sufficient_goal_reduction · S03, S05, S06, S09, S10, S12, S13, and_intro_elim — Goal G: the determinations in the goal. Sufficient condition H: S03, S05, S06, S09, S10, S12 and S13 (H⇒G by conjunction introduction). H is derived forwards from the givens; G is never used as a premise.
• S13 · premise_audit · mko_error_sources, G5, frac_compare — It needs the definitions of the two procedures and exact comparisons; the conclusion is that the source cannot be determined from the value, not that the source is one particular procedure.
• S12 · premise_audit · mul_inverse_nonzero, mko_error_def — It needs only x₀=0; this is a limit of the definition, not a computational difficulty.
• S11 · premise_audit · mko_error_def, frac_rules, abs_rules — The relative error needs x′≠0, which holds. The example only shows the effect of scale; it does not claim relative error is invariant under every transformation.
• S10 · premise_audit · mko_error_def, S03, L_tol_interval — The conclusion depends on ≤ rather than <; with a strict inequality the endpoint would be excluded, so the MKO's definition must be followed.
• S09 · inverse_equivalence · frac_compare, order_basics — The same equivalence as in S06, valid both ways; here the conclusion is negative.
• S08 · premise_audit · L_tol_interval, frac_compare, numeric_evaluation — It needs the lemma and comparison of fractions with positive denominators; it is an independent check of the same conclusion, and S06 does not depend on it.
• S07.3 · inverse_equivalence · case_analysis, order_basics — Adding and subtracting x undo each other and keep inequalities, so both directions hold; the two cases are exhaustive.
• S07.2 · inverse_equivalence · abs_rules, order_basics — Multiplying by −1 twice returns to the original, and the right bound is always true in this case, so both directions hold.
• S07.1 · inverse_equivalence · abs_rules, order_basics — In this case the left bound −τ≤u is always true, so adding or removing it does not change truth, and both directions hold; this uses τ≥0.
• S07 · inverse_equivalence · L_tol_interval — The lemma is itself a biconditional, and both directions are proved in the sub-steps.
• S06 · inverse_equivalence · frac_compare, order_basics — Both denominators here, 300 and 250, are positive, so multiplication by their positive product preserves order and division by it reverses the move. These are sufficient hypotheses of the lemma used, not necessary sign conditions for every comparison: two negative denominators also have positive product. A negative product reverses order; a zero denominator makes the quotient undefined.
• S05 · inverse_equivalence · frac_rules, S04 — Dividing by 1/3 needs x≠0 from S04; backwards, multiplying by 1/3 gives 1/300.
• S04 · premise_audit · abs_rules, order_basics — It needs the sign of x; positive implies nonzero, and the converse is not claimed (a nonzero number may be negative).
• S03 · inverse_equivalence · abs_rules — Both expressions denote the same nonnegative number; the sign of u must be known first to choose the right branch of the absolute value.
• S02.2 · inverse_equivalence · frac_rules, numeric_evaluation — Exact integer computation 99−100=−1, valid both ways.
• S02.1 · inverse_equivalence · frac_rules — Cancelling the nonzero common factor 3 or 100 returns to the original, so the step holds both ways.
• S02 · inverse_equivalence · frac_rules, numeric_evaluation — Exact rational arithmetic, the same number both ways; backwards, 1/3+(−1/300)=99/300=33/100.
• S01 · premise_audit · G1, G2, mko_error_def — This step only states definitions and data and derives no new fact; the condition x≠0 must be checked in S04 before the relative error is used.

Error controls and negative controls

No relative error for a zero reference

One misconception named by the MKO is computing a relative error with a zero reference. In S12, |a₀−x₀|=1/1000 can be computed, but (1/1000)/0 is undefined. To describe quantities near 0, use the absolute error or state another nonzero scale explicitly, with a reason.

Not every error is a rounding error

Another misconception named by the MKO is calling every error a rounding error. S13 shows that 0.33 may come from rounding or from truncation, both with error 1/300; it might also come from measurement or modelling. The error value alone does not reveal the source; data about how the value was produced are needed.

Endpoints are included, and compare fractions carefully

The definition uses ≤, so the a in S10 that sits exactly at the endpoint counts as within tolerance. When comparing 1/300 with 1/400, do not carry the direction of the denominator comparison over to the fractions: fractions with positive denominators can be compared by cross-multiplying (S06, S09); with numerators 1, the larger denominator gives the smaller fraction.

• The relative error of a₀=1/1000 to x₀=0 is infinite → reject — Relative error is defined only for a nonzero reference; division by 0 is undefined (S12).
• a=33/100 is exactly on the boundary, so it is not within tolerance τ₃=1/300 → reject — The definition is |a−x|≤τ, which includes the endpoints (S10).
• |a−x|=1/300 proves that 0.33 was obtained by rounding → reject — Truncation also gives 33/100 with the same error (S13).
• Since 300<400, 1/300<1/400, so a is within τ₂ → reject — 1/300≤1/400 ⇔ 400≤300, which is false; in fact 1/300>1/400 (S09).
• a′=330 and x′=1000/3 have the same relative error 1/100, so the absolute error is also 1/300 → reject — Absolute error keeps the scale; it is 10/3 (S11).

Result and limitations

The approximation a=33/100 to x=1/3 has absolute error 1/300 and relative error 1/100. It is within τ₁=1/250, equivalently a∈[247/750, 253/750]; it is not within τ₂=1/400; it is within τ₃=1/300, exactly at the left endpoint. After scaling by 1000 the absolute error becomes 10/3 while the relative error stays 1/100. For a zero reference the relative error is undefined. The error value 1/300 can come from rounding or from truncation, so its source cannot be determined from the value.

• This guide reads the decimal 0.33 as the exact rational 33/100; the difference between a displayed binary floating-point value and its actual stored value is out of scope.

Verification and source binding

16 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 58bd7e5c1024dfee361ec4fcc28dfa4a57c63d8a4f604d1e27e3e41147838585
• original source SHA-256: b3644181d9d4bd6d19b2e0af1af975697928d76dee4dcb2c3153092b30403bce
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)