# 數值近似與誤差：以 0.33 近似 1/3 的絕對誤差、相對誤差與容許範圍

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-numerical-approximation-error/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

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



## 目標與範圍

以精確有理數計算：近似值 a=33/100 相對參照值 x=1/3 的絕對誤差與相對誤差；判定 a 是否在容許誤差 τ₁=1/250、τ₂=1/400、τ₃=1/300 之內（τ₃ 為端點情形）；證明 |a−x|≤τ ⇔ x−τ≤a≤x+τ；比較放大 1000 倍後的誤差；說明參照值為 0 時相對誤差沒有定義，以及誤差數值本身不能說明誤差來源。

全部使用精確有理數（MKO 假設 a1），十進位寫法 0.33 讀作有理數 33/100，不涉及二進位浮點表示。相對誤差只在參照值非零時計算（假設 a2）。不處理條件數、穩定性或收斂階；不改動 canonical MKO 或英文 edition。





## 已知條件與符號


- frac_rules
- abs_rules
- order_basics
- mul_inverse_nonzero
- case_analysis


- G1 — 近似值 a=33/100（十進位 0.33 讀作精確有理數），參照值 x=1/3。
- G2 — 容許誤差 τ₁=1/250、τ₂=1/400、τ₃=1/300，皆 ≥0。
- G3 — 放大的一對：a′=330，x′=1000/3。
- G4 — 參照值為零的一對：a₀=1/1000，x₀=0。
- G5 — 兩位小數的產生方式：四捨五入取最接近的 k/100；截斷取不超過原數（正數）的最大 k/100（k 為整數）。


- a,\ x — 近似值與參照值
- |a-x| — 絕對誤差
- \frac{|a-x|}{|x|} — 相對誤差（x≠0）
- \tau — 容許誤差，τ≥0
- [x-\tau,\ x+\tau] — 容許區間（含端點）





## 規則與來源


- frac_rules · prerequisite — 分數運算（分母皆非零）：a/c+b/c=(a+b)/c；(a/b)(c/d)=(ac)/(bd)；(a/b)/(c/d)=(ad)/(bc)（另需 c≠0）；a/b=(ak)/(bk)（k≠0）。
- abs_rules · prerequisite — 絕對值（實數）：|u|=u（u≥0）、|u|=−u（u<0）；|u|≥0；|uv|=|u||v|；三角不等式 |u+v|≤|u|+|v|；|u|<r ⇔ −r<u<r。
- order_basics · prerequisite — 實數的序：任兩數恰有 u<v、u=v、u>v 之一；u<v 且 v<w 推出 u<w；u<v 推出 u+w<v+w；u<v 且 w>0 推出 uw<vw；u<v 且 w<0 推出 uw>vw。
- mul_inverse_nonzero · prerequisite — 非零數的倒數：在 ℚ、ℝ、ℂ 中，若 u≠0，存在 1/u 使 u·(1/u)=1；對 u≠0 定義 v/u 為 v·(1/u)。u=0 時沒有倒數，v/0 不定義。
- case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
- def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
- numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
- neg_mul · prerequisite — 負號與乘法：(−u)v=−(uv)，(−u)(−v)=uv。
- eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
- and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
- mko_error_def · cited — 給近似值 a 與參照值 x，絕對誤差為 |a−x|。若 x≠0，相對誤差為 |a−x|/|x|。容許誤差 τ≥0 時，|a−x|≤τ 才稱在該容許範圍內。 · mko-numerical-approximation-error
- mko_error_sources · cited — 誤差數值本身不說明來源。要區分離散化、截斷、捨入、量測與模型誤差，必須另有產生過程資料。 · mko-numerical-approximation-error
- frac_compare · prerequisite — 正分母的分數比較：若 b>0、d>0，則 a/b≤c/d ⇔ ad≤cb（兩邊同乘正數 bd）。
- L_tol_interval · lemma — 對實數 a、x 與 τ≥0：|a−x|≤τ ⇔ x−τ≤a≤x+τ。





## 逐步主鏈

S01 · definition操作前

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

條件：\tau\ge 0

規則：mko_error_def · 依賴：G1, G2

葉節點依據：mko_error_def + def_intro

依 MKO 寫出三個定義。絕對誤差保留原量的尺度；相對誤差只在 x≠0 時定義，把誤差和參照量比較；「在容許範圍內」用的是 ≤，所以等號成立時也算在內。



S02 · equivalent操作前

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

操作後

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

條件：100\neq 0,\ 3\neq 0

規則：frac_rules · 依賴：G1

葉節點依據：frac_rules + numeric_evaluation

通分到公分母 300 後相減，細節在 S02.1、S02.2。結果為負，表示近似值比參照值小。



S03 · equivalent操作前

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

操作後

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

條件：-\tfrac{1}{300}<0

規則：abs_rules · 依賴：S02

葉節點依據：abs_rules + neg_mul

因 −1/300<0，依絕對值定義 |u|=−u，得 1/300。這就是絕對誤差，單位與 x 相同。



S04 · implies操作前

x=\tfrac{1}{3}

操作後

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

條件：\tfrac{1}{3}>0

規則：abs_rules · 依賴：G1

葉節點依據：abs_rules + order_basics

1/3>0，所以 x≠0，且 |x|=x=1/3。這是 MKO 計算相對誤差的前提。



S05 · equivalent操作前

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

操作後

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

條件：\tfrac{1}{3}\neq 0

規則：frac_rules · 依賴：S03, S04

葉節點依據：frac_rules + mul_inverse_nonzero

依 (a/b)/(c/d)=(ad)/(bc)（c≠0）：(1·3)/(300·1)=3/300=1/100。相對誤差是無因次的比，也就是 1%。



S06 · equivalent操作前

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

操作後

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

條件：300>0,\ 250>0

規則：frac_compare · 依賴：S03, G2

葉節點依據：frac_compare + order_basics

依分數比較，兩邊同乘正數 300·250：1/300≤1/250 ⇔ 1·250≤1·300，後者成立。所以 |a−x|≤τ₁，a 在容許誤差 τ₁ 之內。



S07 · equivalent操作前

|a-x|\le\tau

操作後

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

條件：\tau\ge 0

規則：L_tol_interval · 依賴：L_tol_interval

葉節點依據：abs_rules + order_basics + case_analysis

依引理 L_tol_interval（在 S07.1 到 S07.3 分情況證明），誤差界等價於 a 位於含端點的區間 [x−τ, x+τ]，這是 MKO 第二段的說法。庫中的 abs_rules 只給嚴格版 |u|<r，所以非嚴格版需要自己證明。



S08 · implies操作前

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

操作後

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

條件：\tau_1\ge 0

規則：L_tol_interval · 依賴：S07, G1, G2, S06

葉節點依據：L_tol_interval + frac_compare + numeric_evaluation

第二條路線核對 S06：1/3−1/250=250/750−3/750=247/750，1/3+1/250=253/750。交叉相乘：33·750=24750≥247·100=24700，且 24750≤253·100=25300，所以 247/750≤33/100≤253/750。依 L_tol_interval，這與 |a−x|≤τ₁ 等價，與 S06 一致。



S09 · equivalent操作前

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

操作後

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

條件：300>0,\ 400>0

規則：frac_compare · 依賴：S03, G2

葉節點依據：frac_compare + order_basics

依分數比較，1/300≤1/400 ⇔ 400≤300，後者不成立，所以 |a−x|>τ₂，a 不在容許誤差 τ₂ 之內。分子同為 1 時，分母較大的分數較小。



S10 · implies操作前

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

操作後

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

條件：\tau_3\ge 0

規則：mko_error_def · 依賴：S03, S07, G2

葉節點依據：mko_error_def + eq_refl_symm_trans + order_basics

τ₃=1/300 時 |a−x|=τ₃，而定義用 ≤，所以 a 在容許範圍內。事實上 x−τ₃=1/3−1/300=99/300=33/100=a，a 正好在左端點；MKO 說明端點包含在容許範圍。



S11 · implies操作前

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

操作後

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

條件：x'\neq 0

規則：mko_error_def · 依賴：G3, mko_error_def

葉節點依據：mko_error_def + frac_rules + abs_rules

330=990/3，所以 a′−x′=−10/3，絕對誤差 10/3；x′=1000/3≠0，相對誤差 (10/3)/(1000/3)=1/100。兩個量都放大 1000 倍後，絕對誤差也放大 1000 倍（10/3=1000·1/300），相對誤差不變。兩種誤差回答不同的問題。



S12 · implies操作前

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

操作後

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

條件：x_0=0

規則：mul_inverse_nonzero · 依賴：G4, mko_error_def

葉節點依據：mul_inverse_nonzero + abs_rules

絕對誤差照常計算：|1/1000−0|=1/1000。相對誤差要除以 |x₀|=0，而 0 沒有倒數，v/0 不定義，所以依 MKO 假設 a2 不計算相對誤差；不能把它寫成無限大或改用其他分母而不加說明。



S13 · implies操作前

\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}

條件：無

規則：mko_error_sources · 依賴：G1, G5, mko_error_sources

葉節點依據：mko_error_sources + frac_compare + numeric_evaluation

33/100≤1/3<34/100，且 1/3 到 33/100 的距離 1/300 小於到 34/100 的距離 2/300，所以四捨五入與截斷都給出 33/100，誤差同為 1/300。同一個誤差值可能來自兩種不同程序，所以誤差值本身不能告訴我們來源。對 2/3 兩者就不同：四捨五入得 67/100（誤差 1/300），截斷得 66/100（誤差 1/150）。



S14 · implies操作前

\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

條件：無

規則：and_intro_elim · 依賴：S03, S05, S06, S09, S10, S12, S13

葉節點依據：and_intro_elim

合併結論：絕對誤差 1/300，相對誤差 1/100；在 τ₁ 與 τ₃（端點）之內，不在 τ₂ 之內；參照值為 0 時相對誤差沒有定義；誤差值不決定來源。







## 局部子步與引理

S02.1 · equivalent操作前

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

操作後

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

條件：3\neq 0,\ 100\neq 0

規則：frac_rules · 依賴：G1

葉節點依據：frac_rules

依 a/b=(ak)/(bk)（k≠0）：33/100 分子分母同乘 3 得 99/300；1/3 同乘 100 得 100/300。



S02.2 · equivalent操作前

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

操作後

-\tfrac{1}{300}

條件：無

規則：frac_rules · 依賴：S02.1

葉節點依據：frac_rules + numeric_evaluation

同分母相減：(99−100)/300=−1/300。



S07.1 · equivalent操作前

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

操作後

-\tau\le u\le\tau

條件：u\ge 0; \tau\ge 0

規則：abs_rules · 依賴：abs_rules

葉節點依據：abs_rules + order_basics

設 u=a−x 且 u≥0。此時 |u|=u，所以 |u|≤τ ⇔ u≤τ。而 −τ≤0≤u 自動成立（因 τ≥0），所以 u≤τ ⇔ −τ≤u≤τ。



S07.2 · equivalent操作前

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

操作後

-\tau\le u\le\tau

條件：u<0; \tau\ge 0

規則：abs_rules · 依賴：abs_rules

葉節點依據：abs_rules + order_basics + neg_mul

設 u<0。此時 |u|=−u，−u≤τ ⇔ −τ≤u（兩邊乘 −1 反轉不等號）。而 u<0≤τ 使 u≤τ 自動成立，所以 −u≤τ ⇔ −τ≤u≤τ。



S07.3 · equivalent操作前

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

操作後

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

條件：\tau\ge 0

規則：case_analysis · 依賴：S07.1, S07.2

葉節點依據：case_analysis + order_basics

u≥0 與 u<0 涵蓋所有實數（三分律），兩種情形都得到同一個等價，依分情況論證它對每個 u=a−x 成立。最後三邊同加 x 得 x−τ≤a≤x+τ。S07.1 到 S07.3 合起來證得引理 L_tol_interval。







## 逐步反向審查


- S14 · sufficient_goal_reduction · S03, S05, S06, S09, S10, S12, S13, and_intro_elim — 目標 G：本稿目標的各項判定。足夠條件 H：S03、S05、S06、S09、S10、S12、S13（H⇒G 由合取引入）。H 由給定條件正向推出，沒有把 G 當作前提。
- S13 · premise_audit · mko_error_sources, G5, frac_compare — 需要兩種程序的定義與精確比較；結論是「不能由數值判定來源」，不是「來源是某一種」。
- S12 · premise_audit · mul_inverse_nonzero, mko_error_def — 只需要 x₀=0；這是定義的界限，而不是計算困難。
- S11 · premise_audit · mko_error_def, frac_rules, abs_rules — 相對誤差需要 x′≠0，這裡成立。此例只說明尺度效應，不宣稱相對誤差對任何變換都不變。
- S10 · premise_audit · mko_error_def, S03, L_tol_interval — 結論依賴「≤」而非「<」；若定義改用嚴格不等號，端點就會被排除，所以必須照 MKO 的定義。
- S09 · inverse_equivalence · frac_compare, order_basics — 與 S06 相同的等價變形，雙向成立；結論是否定的。
- S08 · premise_audit · L_tol_interval, frac_compare, numeric_evaluation — 需要引理與正分母的分數比較；這是對同一結論的獨立核對，S06 不依賴它。
- S07.3 · inverse_equivalence · case_analysis, order_basics — 加 x 與減 x 互為反運算且保持不等號，雙向成立；兩種情形完整涵蓋。
- S07.2 · inverse_equivalence · abs_rules, order_basics — 乘 −1 兩次回到原式，右界在此情形恆真，雙向成立。
- S07.1 · inverse_equivalence · abs_rules, order_basics — 左界 −τ≤u 在此情形下恆真，加入或去掉它都不改變真假，雙向成立；這裡用到 τ≥0。
- S07 · inverse_equivalence · L_tol_interval — 引理本身是雙條件，兩個方向都在子步證明。
- S06 · inverse_equivalence · frac_compare, order_basics — 本步的兩個分母 300、250 均為正，乘以其正乘積保持不等號方向，除回可還原。這是所用引理的充分前提，不表示每個分母都正是所有比較的必要條件：兩個負分母的乘積也為正；乘積為負才反向，分母為零則商未定義。
- S05 · inverse_equivalence · frac_rules, S04 — 除以 1/3 需要 S04 的 x≠0；反向是乘回 1/3 得 1/300。
- S04 · premise_audit · abs_rules, order_basics — 需要 x 的正負；正數推出非零，反向不宣稱（非零數也可能是負的）。
- S03 · inverse_equivalence · abs_rules — 兩式表示同一個非負數；先確定 u 的符號才能選對絕對值的分支。
- S02.2 · inverse_equivalence · frac_rules, numeric_evaluation — 整數 99−100=−1 的精確計算，雙向成立。
- S02.1 · inverse_equivalence · frac_rules — 約去非零公因數 3 或 100 即回到原式，雙向成立。
- S02 · inverse_equivalence · frac_rules, numeric_evaluation — 精確有理數運算，雙向是同一個數；反向可驗算 1/3+(−1/300)=99/300=33/100。
- S01 · premise_audit · G1, G2, mko_error_def — 此步只寫出定義與數據，不推出新事實；x≠0 的條件要在 S04 檢查後才能使用相對誤差。





## 錯誤控制與反例

參照值為零不能算相對誤差MKO 指出的誤解之一是參照值為零仍計算相對誤差。S12 中 |a₀−x₀|=1/1000 可以算，但 (1/1000)/0 沒有定義。若需要描述靠近 0 的量，應改用絕對誤差或明示另一個非零尺度，並說明理由。

不是所有誤差都是捨入誤差MKO 指出的另一個誤解是把所有誤差都叫捨入誤差。S13 顯示 0.33 可能由四捨五入或截斷得到，誤差都是 1/300；它也可能來自量測或模型。誤差數值本身不說明來源，必須有產生過程的資料。

端點包含在內，比較分數要注意方向定義用 ≤，所以 S10 中恰在端點的 a 算在容許範圍內。比較 1/300 與 1/400 時不能把分母的大小方向直接當成分數的大小方向：正分母的分數可用交叉相乘比較（S06、S09），分子同為 1 時分母越大分數越小。


- a₀=1/1000 相對 x₀=0 的相對誤差是無限大 → reject — 相對誤差只在參照值非零時定義；除以 0 沒有定義（S12）。
- a=33/100 剛好在邊界上，所以不在容許誤差 τ₃=1/300 之內 → reject — 定義是 |a−x|≤τ，端點包含在內（S10）。
- |a−x|=1/300 證明 0.33 是由四捨五入得到的 → reject — 截斷也得到 33/100 與同一個誤差（S13）。
- 因為 300<400，所以 1/300<1/400，a 在 τ₂ 之內 → reject — 1/300≤1/400 ⇔ 400≤300，不成立；實際上 1/300>1/400（S09）。
- a′=330 與 x′=1000/3 的相對誤差同為 1/100，所以絕對誤差也同為 1/300 → reject — 絕對誤差保留尺度，是 10/3（S11）。





## 結論與限制

a=33/100 近似 x=1/3 的絕對誤差是 1/300，相對誤差是 1/100。它在 τ₁=1/250 之內，等價地 a∈[247/750, 253/750]；不在 τ₂=1/400 之內；在 τ₃=1/300 之內且恰在左端點。放大 1000 倍後絕對誤差變為 10/3，相對誤差仍為 1/100。參照值為 0 時相對誤差沒有定義。誤差值 1/300 可由四捨五入或截斷產生，所以不能由數值判定來源。


- 本稿把十進位 0.33 讀作精確有理數 33/100；二進位浮點顯示值與其真正儲存值的差異不在範圍內。





## 驗證及來源綁定

16 個本稿宣告算術檢查；只支持所列算式。


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

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-numerical-approximation-error-01.json)