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

目標與範圍

以精確有理數計算：近似值 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+τ。

逐步主鏈

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

局部子步與引理

\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

逐步反向審查

• 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、反控制與修訂記錄）