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

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-numerical-approximation-error/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

derivation-mko-numerical-approximation-error-01 · production-20261019-adopted-96



## 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

S01 · definitionBefore

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

After

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

Conditions: \tau\ge 0

Rule: mko_error_def · Uses: G1, G2

Leaf basis: mko_error_def + def_intro

State the three definitions from the MKO. Absolute error keeps the scale of the quantity; relative error is defined only for x≠0 and compares the error with the reference; 'within tolerance' uses ≤, so equality counts as within.



S02 · equivalentBefore

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

After

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

Conditions: 100\neq 0,\ 3\neq 0

Rule: frac_rules · Uses: G1

Leaf basis: frac_rules + numeric_evaluation

Bring both to the common denominator 300 and subtract; details in S02.1 and S02.2. The result is negative, so the approximation is below the reference.



S03 · equivalentBefore

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

After

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

Conditions: -\tfrac{1}{300}<0

Rule: abs_rules · Uses: S02

Leaf basis: abs_rules + neg_mul

Since −1/300<0, the definition |u|=−u gives 1/300. This is the absolute error, in the same units as x.



S04 · impliesBefore

x=\tfrac{1}{3}

After

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

Conditions: \tfrac{1}{3}>0

Rule: abs_rules · Uses: G1

Leaf basis: abs_rules + order_basics

1/3>0, so x≠0 and |x|=x=1/3. This is the MKO's precondition for computing the relative error.



S05 · equivalentBefore

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

After

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

Conditions: \tfrac{1}{3}\neq 0

Rule: frac_rules · Uses: S03, S04

Leaf basis: frac_rules + mul_inverse_nonzero

By (a/b)/(c/d)=(ad)/(bc) with c≠0: (1·3)/(300·1)=3/300=1/100. The relative error is a dimensionless ratio, that is 1%.



S06 · equivalentBefore

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

After

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

Conditions: 300>0,\ 250>0

Rule: frac_compare · Uses: S03, G2

Leaf basis: frac_compare + order_basics

By comparison of fractions, multiplying both sides by the positive number 300·250: 1/300≤1/250 ⇔ 1·250≤1·300, which is true. So |a−x|≤τ₁ and a is within tolerance τ₁.



S07 · equivalentBefore

|a-x|\le\tau

After

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

Conditions: \tau\ge 0

Rule: L_tol_interval · Uses: L_tol_interval

Leaf basis: abs_rules + order_basics + case_analysis

By Lemma L_tol_interval (proved by cases in S07.1 to S07.3), the error bound is equivalent to a lying in the closed interval [x−τ, x+τ], as the MKO's second paragraph says. The library rule abs_rules gives only the strict version |u|<r, so the non-strict version is proved here.



S08 · impliesBefore

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

After

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

Conditions: \tau_1\ge 0

Rule: L_tol_interval · Uses: S07, G1, G2, S06

Leaf basis: L_tol_interval + frac_compare + numeric_evaluation

A second route to S06: 1/3−1/250=250/750−3/750=247/750 and 1/3+1/250=253/750. Cross-multiplying: 33·750=24750≥247·100=24700 and 24750≤253·100=25300, so 247/750≤33/100≤253/750. By L_tol_interval this is equivalent to |a−x|≤τ₁, agreeing with S06.



S09 · equivalentBefore

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

After

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

Conditions: 300>0,\ 400>0

Rule: frac_compare · Uses: S03, G2

Leaf basis: frac_compare + order_basics

By comparison of fractions, 1/300≤1/400 ⇔ 400≤300, which is false, so |a−x|>τ₂ and a is not within tolerance τ₂. With equal numerators 1, the fraction with the larger denominator is smaller.



S10 · impliesBefore

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

After

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

Conditions: \tau_3\ge 0

Rule: mko_error_def · Uses: S03, S07, G2

Leaf basis: mko_error_def + eq_refl_symm_trans + order_basics

With τ₃=1/300 we have |a−x|=τ₃, and the definition uses ≤, so a is within tolerance. In fact x−τ₃=1/3−1/300=99/300=33/100=a, so a sits exactly at the left endpoint; the MKO says endpoints are included.



S11 · impliesBefore

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

After

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

Conditions: x'\neq 0

Rule: mko_error_def · Uses: G3, mko_error_def

Leaf basis: mko_error_def + frac_rules + abs_rules

330=990/3, so a′−x′=−10/3 and the absolute error is 10/3; x′=1000/3≠0 and the relative error is (10/3)/(1000/3)=1/100. Scaling both quantities by 1000 scales the absolute error by 1000 (10/3=1000·1/300) and leaves the relative error unchanged. The two errors answer different questions.



S12 · impliesBefore

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

After

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

Conditions: x_0=0

Rule: mul_inverse_nonzero · Uses: G4, mko_error_def

Leaf basis: mul_inverse_nonzero + abs_rules

The absolute error is computed as usual: |1/1000−0|=1/1000. The relative error would divide by |x₀|=0, but 0 has no inverse and v/0 is undefined, so by MKO assumption a2 the relative error is not evaluated; it may not be written as infinity or silently replaced by another denominator.



S13 · impliesBefore

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

After

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

Conditions: none

Rule: mko_error_sources · Uses: G1, G5, mko_error_sources

Leaf basis: mko_error_sources + frac_compare + numeric_evaluation

33/100≤1/3<34/100, and the distance from 1/3 to 33/100, 1/300, is smaller than the distance to 34/100, 2/300, so both rounding and truncation give 33/100, with the same error 1/300. One error value can come from two different procedures, so the value itself cannot tell us the source. For 2/3 the two differ: rounding gives 67/100 (error 1/300) and truncation gives 66/100 (error 1/150).



S14 · impliesBefore

\text{computed and proved facts}

After

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

Conditions: none

Rule: and_intro_elim · Uses: S03, S05, S06, S09, S10, S12, S13

Leaf basis: and_intro_elim

Combine the conclusions: absolute error 1/300 and relative error 1/100; within τ₁ and τ₃ (endpoint), not within τ₂; for a zero reference the relative error is undefined; the error value does not determine its source.







## Substeps and lemmas

S02.1 · equivalentBefore

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

After

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

Conditions: 3\neq 0,\ 100\neq 0

Rule: frac_rules · Uses: G1

Leaf basis: frac_rules

By a/b=(ak)/(bk) with k≠0: multiplying numerator and denominator of 33/100 by 3 gives 99/300, and of 1/3 by 100 gives 100/300.



S02.2 · equivalentBefore

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

After

-\tfrac{1}{300}

Conditions: none

Rule: frac_rules · Uses: S02.1

Leaf basis: frac_rules + numeric_evaluation

Subtract over the common denominator: (99−100)/300=−1/300.



S07.1 · equivalentBefore

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

After

-\tau\le u\le\tau

Conditions: u\ge 0; \tau\ge 0

Rule: abs_rules · Uses: abs_rules

Leaf basis: abs_rules + order_basics

Let u=a−x with u≥0. Then |u|=u, so |u|≤τ ⇔ u≤τ. And −τ≤0≤u holds automatically (since τ≥0), so u≤τ ⇔ −τ≤u≤τ.



S07.2 · equivalentBefore

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

After

-\tau\le u\le\tau

Conditions: u<0; \tau\ge 0

Rule: abs_rules · Uses: abs_rules

Leaf basis: abs_rules + order_basics + neg_mul

Let u<0. Then |u|=−u, and −u≤τ ⇔ −τ≤u (multiplying by −1 reverses the inequality). And u<0≤τ makes u≤τ automatic, so −u≤τ ⇔ −τ≤u≤τ.



S07.3 · equivalentBefore

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

After

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

Conditions: \tau\ge 0

Rule: case_analysis · Uses: S07.1, S07.2

Leaf basis: case_analysis + order_basics

u≥0 and u<0 cover every real number (trichotomy), and both cases give the same equivalence, so by cases it holds for every u=a−x. Finally adding x to all three parts gives x−τ≤a≤x+τ. S07.1 to S07.3 together prove Lemma L_tol_interval.







## 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 referenceOne 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 errorAnother 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 carefullyThe 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)](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-numerical-approximation-error-01.json)