# 實數：在 Cauchy 完備化中證明「循環的 9」與有理數 1 是同一個實數 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-real-number/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-real-number-01 · production-20261019-adopted-96 ## 目標與範圍 在以有理數 Cauchy 序列的等價類建構的實數中（有理數 q 嵌入為常數列的類 ι(q)），令 a_n=1−10^{−n}（n≥1），即有限小數 0.9、0.99、0.999 等。證明 (a_n) 是 Cauchy 序列，且與常數列 1 等價，所以 [(a_n)]=ι(1)；證明 ι 是單射，因此有限小數 0.999=999/1000 所表示的實數不等於 1；並說明有限小數 0.375=3/8 是有理數，在 ℝ 中就是 ι(3/8)。 在 MKO 假設 a1 的 Cauchy 完備化語境中工作，只用有理數的運算、序與絕對值（不使用正在建構的實數的性質，避免循環）。「∼ 是等價關係」以外部文獻引用（citation_verified）。不定義 ℝ 上的加法、乘法與序，不證明完備性，也不證明與 Dedekind 分割等其他建構的等價（MKO 指出這需要另外證明）；不改動 canonical MKO 或英文 edition。 ## 已知條件與符號 - nat_induction - frac_rules - power_laws - numeric_evaluation - G1 — ℚ 是有序域：有理數的加、乘、序與絕對值遵守有序域的規則（含三角不等式 |x+y|≤|x|+|y|）。本稿的 ε、δ 都是正有理數。 - G2 — Cauchy 序列：有理數列 (a_n)_{n≥1} 是 Cauchy 序列，若對每個有理數 ε>0，存在 N，使所有 m,n≥N 都有 |a_m−a_n|<ε。 - G3 — 等價與實數（MKO 假設 a1）：Cauchy 序列 (a_n)、(b_n) 等價，記作 (a_n)∼(b_n)，若對每個有理數 ε>0，存在 N，使所有 n≥N 都有 |a_n−b_n|<ε。ℝ 是 Cauchy 序列等價類 [(a_n)] 的集合；有理數 q 的嵌入是常數列的類 ι(q)=[(q)_{n≥1}]。 - G4 — 資料：a_n=1−10^{−n}（n≥1）；有限小數 0.999 與 0.375。 - (a_n)_{n\ge1} — 有理數列 - (a_n)\sim(b_n) — 兩個 Cauchy 序列等價 - [(a_n)] — (a_n) 的等價類，即一個實數 - \iota(q) — 有理數 q 的嵌入：常數列 q 的類 - \varepsilon,\ \delta — 正有理數 ## 規則與來源 - nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。 - 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）。 - power_laws · prerequisite — 整數指數律（底數非零或指數為正整數）：a^m·a^n=a^{m+n}，(a^m)^n=a^{mn}，(ab)^n=a^n b^n，a^0=1。 - numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。 - def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。 - def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。 - add_inverse · prerequisite — 加法反元素：每個 u 都有 −u，使 u+(−u)=0；u−v 定義為 u+(−v)。 - exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。 - exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。 - forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。 - contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。 - forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。 - and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。 - mko_real_def · cited — 實數系 R 可由有理數的 Cauchy 完備化建構；每個有理數都可嵌入 R，而不同建構仍須證明彼此等價。 · mko-real-number - q_ordered_field · prerequisite — ℚ 是有序域：域的運算規則、序的規則（三一律、遞移、加同數保序、乘正數保序、正數取倒數使不等號反向）與絕對值規則（|x|≥0、|−x|=|x|、三角不等式）都在 ℚ 中成立。 - pos_int_ge_one · prerequisite — 每個正整數都 ≥1。 - cauchy_def · prerequisite — Cauchy 序列：對每個有理數 ε>0，存在 N，使所有 m,n≥N 都有 |a_m−a_n|<ε。 - equiv_def · prerequisite — (a_n)∼(b_n) 表示對每個有理數 ε>0，存在 N，使所有 n≥N 都有 |a_n−b_n|<ε；ℝ 是等價類的集合，ι(q)=[(q)_{n≥1}]。 - thm_equiv_relation · cited — 有理數 Cauchy 序列之間的等價 ∼ 是等價關係（自反、對稱、遞移）；因此等價類有定義，且 [(a_n)]=[(b_n)] ⇔ (a_n)∼(b_n)。 · Keith Conrad, Metric Spaces, Section 8 (completions), p. 39 - L_pow_ten · lemma — 對每個整數 n≥1：10^n>n。 - L_small · lemma — 對每個有理數 ε>0，存在正整數 N，使所有整數 n≥N 都有 10^{−n}<ε。 ## 逐步主鏈 S01 · definition操作前 \mathbb{R} 操作後 \{[(a_n)]\mid (a_n)\ \text{Cauchy in}\ \mathbb{Q}\},\ \iota(q)=[(q)_{n\ge1}] 條件：無 規則：equiv_def · 依賴：G2, G3, mko_real_def 葉節點依據：equiv_def + cauchy_def + mko_real_def 依 MKO 假設 a1，在 Cauchy 完備化的語境中工作：實數是有理數 Cauchy 序列的等價類，有理數 q 經 ι 嵌入為常數列（每一項都是 q）的類。常數列是 Cauchy 序列，因為 |q−q|=0<ε 對所有 m、n 成立。 S02 · equivalent操作前 [(a_n)]=[(b_n)] 操作後 (a_n)\sim(b_n) 條件：(a_n),(b_n)\ \text{Cauchy} 規則：thm_equiv_relation · 依賴：S01, thm_equiv_relation 葉節點依據：thm_equiv_relation + def_unfold ∼ 是等價關係（外部引用 thm_equiv_relation），所以等價類有定義，而且兩個類相等恰好當兩個代表序列等價。之後要證兩個實數相等，只需證兩個序列等價；要證不相等，只需證不等價。 S03 · definition操作前 a_n=1-10^{-n}\ \ (n\ge1) 操作後 a_1=\tfrac{9}{10},\ a_2=\tfrac{99}{100},\ a_3=\tfrac{999}{1000} 條件：無 規則：def_intro · 依賴：G4 葉節點依據：def_intro + q_ordered_field + numeric_evaluation 定義 a_n=1−10^{−n}。每一項都是有理數（10^{−n}=1/10^n，且 10^n≠0）。前三項是 9/10、99/100、999/1000（N1 到 N3），也就是有限小數 0.9、0.99、0.999；一般地，a_n 是小數點後有 n 個 9 的有限小數。 S04 · equivalent操作前 a_n-1 操作後 -10^{-n},\quad |a_n-1|=10^{-n} 條件：無 規則：q_ordered_field · 依賴：S03, q_ordered_field 葉節點依據：q_ordered_field + add_inverse + numeric_evaluation a_n−1=(1−10^{−n})−1=−10^{−n}。10^n>0，所以 10^{−n}=1/10^n>0，|−10^{−n}|=10^{−n}。例：a_3−1=999/1000−1=−1/1000（N4）。 S05 · implies操作前 n\ge 1\ \text{an integer} 操作後 10^n>n 條件：n\ge 1 規則：L_pow_ten · 依賴：L_pow_ten 葉節點依據：L_pow_ten 引理 L_pow_ten：對每個整數 n≥1，10^n>n。以數學歸納法在 S05.1、S05.2 證明。N8 檢查 n=1 到 40，只是有限檢查，不是證明；證明是歸納法。 S06 · implies操作前 \varepsilon\in\mathbb{Q},\ \varepsilon>0 操作後 \exists N\ \forall n\ge N:\ 10^{-n}<\varepsilon 條件：\varepsilon>0 規則：L_small · 依賴：L_small 葉節點依據：L_small 引理 L_small：每個正有理數 ε 都有 N，使 n≥N 時 10^{−n}<ε。在 S06.1、S06.2 證明。這裡只用有理數的運算與序，沒有用到正在建構的實數，避免循環。 S07 · implies操作前 (a_n)_{n\ge1} 操作後 (a_n)\ \text{is Cauchy} 條件：無 規則：cauchy_def · 依賴：S04, S06, G2 葉節點依據：cauchy_def + q_ordered_field + forall_intro + exists_intro 任取有理數 ε>0。對 ε/2（仍是正有理數）使用 L_small，得 N 使 n≥N 時 10^{−n}<ε/2。對 m,n≥N：|a_m−a_n|=|(a_m−1)+(1−a_n)|≤|a_m−1|+|a_n−1|=10^{−m}+10^{−n}<ε/2+ε/2=ε（三角不等式與 S04）。ε 是任意的，所以 (a_n) 是 Cauchy 序列。 S08 · implies操作前 (a_n),\ (1)_{n\ge1} 操作後 (a_n)\sim(1)_{n\ge1} 條件：無 規則：equiv_def · 依賴：S01, S04, S06, S07, G3 葉節點依據：equiv_def + forall_intro + exists_intro 兩個序列都是 Cauchy 序列（S07 與 S01）。任取有理數 ε>0，L_small 給出 N，使 n≥N 時 |a_n−1|=10^{−n}<ε（S04）。ε 是任意的，依 G3，(a_n) 與常數列 1 等價。 S09 · equivalent操作前 (a_n)\sim(1)_{n\ge1} 操作後 [(a_n)]=\iota(1) 條件：無 規則：thm_equiv_relation · 依賴：S02, S08 葉節點依據：thm_equiv_relation + def_unfold 依 S02，序列等價恰好表示類相等，所以 [(a_n)]=[(1)_{n≥1}]=ι(1)。也就是說，0.9、0.99、0.999 等截斷組成的整個序列所定的實數，正是有理數 1 的嵌入；常說的「0.9 循環等於 1」在這個建構中就是這個等式。 S10 · implies操作前 p\neq q\ \text{in}\ \mathbb{Q} 操作後 \iota(p)\neq\iota(q) 條件：無 規則：contradiction · 依賴：S02, G3, q_ordered_field 葉節點依據：contradiction + q_ordered_field + equiv_def 設 p≠q，令 δ=|p−q|>0（有理數）。若常數列 (p) 與 (q) 等價，取 ε=δ，存在 N 使 n≥N 時 |p−q|<δ，即 δ<δ，矛盾。所以兩個常數列不等價，依 S02，ι(p)≠ι(q)：ι 是單射，不同的有理數嵌入成不同的實數。 S11 · implies操作前 \tfrac{999}{1000}\neq 1 操作後 \iota(\tfrac{999}{1000})\neq\iota(1) 條件：無 規則：forall_elim · 依賴：S10, G4 葉節點依據：forall_elim + numeric_evaluation 999/1000≠1（兩者差 1/1000，N12、N13），依 S10，有限小數 0.999 所表示的實數 ι(999/1000) 不等於 1。等於 1 的是整個截斷序列的類（S09），不是任何一個有限截斷；有限截斷只是近似值。 S12 · implies操作前 0.375 操作後 \tfrac{375}{1000}=\tfrac{3}{8},\quad \iota(\tfrac{3}{8})\in\mathbb{R} 條件：無 規則：mko_real_def · 依賴：S01, G4 葉節點依據：mko_real_def + equiv_def + numeric_evaluation 有限小數 0.375=3/10+7/100+5/1000=375/1000=3/8（N14、N15），是有理數；它在 ℝ 中是 ι(3/8)，即常數列 3/8 的類。有限小數不是另一種獨立數系，更不是無理數。 S13 · implies操作前 \text{S07, S09, S10, S11, S12} 操作後 [(a_n)]=\iota(1);\ \iota\ \text{injective};\ \iota(\tfrac{999}{1000})\neq\iota(1);\ 0.375=\tfrac{3}{8} 條件：無 規則：and_intro_elim · 依賴：S07, S09, S10, S11, S12 葉節點依據：and_intro_elim 截斷序列 (a_n) 是 Cauchy 序列且與常數列 1 等價，所以它所定的實數就是 ι(1)；ι 是單射，所以單一的有限截斷 0.999 不等於 1；有限小數 0.375 是有理數 3/8 的嵌入。 ## 局部子步與引理 S05.1 · induction_base操作前 n=1 操作後 10^1=10>1 條件：無 規則：nat_induction · 依賴：q_ordered_field 葉節點依據：nat_induction + numeric_evaluation 基礎情形 n=1：10¹=10>1（N5）。 S05.2 · induction_step操作前 10^n>n\ \ (n\ge1) 操作後 10^{n+1}>n+1 條件：n\ge 1 規則：nat_induction · 依賴：S05.1, q_ordered_field 葉節點依據：nat_induction + power_laws + q_ordered_field 設 10^n>n（n≥1）。則 10^{n+1}=10·10^n>10n（乘以正數 10 保持不等號）。又 10n−(n+1)=9n−1（N6 是恆等式），n≥1 時 9n−1≥9·1−1=8>0（N7），所以 10n>n+1。合起來 10^{n+1}>n+1。依歸納原理（S05.1 與此步），對所有 n≥1 有 10^n>n，證得引理 L_pow_ten。 S06.1 · implies操作前 \varepsilon=\frac{p}{q}>0,\ p,q\in\mathbb{Z},\ q\neq0 操作後 \varepsilon=\frac{r}{s},\ r,s\in\mathbb{Z},\ r\ge1,\ s\ge1 條件：\varepsilon>0 規則：frac_rules · 依賴：q_ordered_field, pos_int_ge_one 葉節點依據：frac_rules + q_ordered_field + pos_int_ge_one + exists_elim ε 是有理數，可寫成 p/q（q≠0）。若 q<0，依分數規則 p/q=(−p)/(−q)，所以可設 q>0。此時 p=εq 是兩個正數的積，p>0。令 r=p、s=q，兩者都是正整數，所以 r≥1、s≥1。 S06.2 · implies操作前 N:=s,\ n\ge N 操作後 10^{-n}<\tfrac{1}{n}\le\tfrac{1}{s}\le\tfrac{r}{s}=\varepsilon 條件：n\ge s\ge 1; r\ge 1 規則：q_ordered_field · 依賴：S06.1, L_pow_ten 葉節點依據：q_ordered_field + L_pow_ten + exists_intro + forall_intro 取 N=s。對 n≥s：依 L_pow_ten，10^n>n>0，正數取倒數使不等號反向，10^{−n}=1/10^n<1/n；n≥s>0 推出 1/n≤1/s；r≥1 且 1/s>0 推出 1/s≤r/s=ε。串起來 10^{−n}<ε。例：ε=1/100 時 r=1、s=100，N=100 可用（N9）；引理只需要某個 N，不要求最小，例如 n=3 時已有 10^{−3}<1/100（N10）。S06.1 與 S06.2 合起來證得引理 L_small。 ## 逐步反向審查 - S13 · sufficient_goal_reduction · S07, S08, S09, S10, S11, S12 — 目標是 goal 所列各項。足夠條件 H：S07、S09、S10、S11、S12 各自成立；H 推出目標只用合取。普遍敘述由任意 ε 的論證與歸納法得到，沒有把目標當作前提；唯一外部依賴是 thm_equiv_relation。 - S12 · premise_audit · mko_real_def, equiv_def, numeric_evaluation — 只用到有限小數的意義與嵌入 ι。 - S11 · premise_audit · S10, forall_elim, numeric_evaluation — S09 與 S11 不矛盾：S09 比較的是整個序列，S11 比較的是單一個常數。 - S10 · premise_audit · S02, contradiction, q_ordered_field — 關鍵是常數列的差永遠是 δ，不會變小；ε 取 δ 就排除等價。 - S09 · inverse_equivalence · S02, thm_equiv_relation — S02 是雙條件，雙向成立。 - S08 · premise_audit · S04, S06, equiv_def, forall_intro — 等價要求對每個 ε 都找到 N；只看幾項（例如 a_3 與 1 差 1/1000）不夠。 - S07 · premise_audit · S04, S06, q_ordered_field, forall_intro, cauchy_def — 需要對 ε/2 使用引理，使兩項各小於 ε/2；N 可以依賴 ε，這是定義允許的。 - S06.2 · premise_audit · L_pow_ten, q_ordered_field, S06.1, exists_intro — 需要正數取倒數反轉不等號；若 n 可以為 0，1/n 沒有定義，所以 n≥s≥1 很重要。 - S06.1 · premise_audit · frac_rules, q_ordered_field, pos_int_ge_one — 需要 ε>0 才能得到 r>0；ε 是有理數才能寫成整數之比。 - S06 · premise_audit · L_small — 此步只引用引理；證明在子步。 - S05.2 · premise_audit · nat_induction, q_ordered_field, power_laws — 歸納步需要 n≥1 才有 9n−1>0；n=0 時 9·0−1<0，但那不在範圍內。 - S05.1 · premise_audit · nat_induction, numeric_evaluation — 歸納法需要基礎情形成立。 - S05 · premise_audit · L_pow_ten — 此步只引用引理；證明在子步。 - S04 · inverse_equivalence · q_ordered_field, add_inverse, numeric_evaluation — 代數恆等式與絕對值的定義，雙向成立。 - S03 · premise_audit · def_intro, q_ordered_field, numeric_evaluation — 此步只命名序列，並核對前三項。 - S02 · inverse_equivalence · thm_equiv_relation — 這是等價類的基本性質，需要 ∼ 是等價關係；本稿不重證，標記 citation_verified。 - S01 · premise_audit · G2, G3, equiv_def, mko_real_def — 此步只採用建構；不同建構（例如 Dedekind 分割）的等價不在此處理。 ## 錯誤控制與反例 有限小數是有理數MKO 指出的誤解之一是把有限小數視為無理數。0.375=375/1000=3/8（S12），任何有限小數都是「整數除以 10 的乘冪」，因此是有理數；它在 ℝ 中就是某個 ι(q)。 近似小數不是精確值MKO 的另一誤解是把近似小數當成精確值。0.999 與 1 只差 1/1000，但 ι(999/1000)≠ι(1)（S11）；等於 1 的是整個截斷序列的類（S09）。同理，有理數 1.4142 的平方是 1.99996164≠2（N16、N17），所以它不是 2 的平方根，只是近似。 「沒有空隙」不是完備性的證明MKO 提醒：只說實數線「沒有空隙」便宣稱完備性已證明，是誤解；『補入極限點』只是建構直覺。本稿建構了具體的實數並證明一個等式與 ι 的單射性，但沒有定義 ℝ 上的序與運算，也沒有證明完備性（例如每個有上界的非空集合有最小上界），更沒有證明與 Dedekind 分割等其他建構的等價。這些都需要另外的定義與證明。 - 0.375 是無理數，因為它是小數 → reject — 0.375=375/1000=3/8 是有理數（S12）。 - 有限小數 0.999（三個 9）等於 1 → reject — 999/1000≠1，而 ι 是單射，所以 ι(999/1000)≠ι(1)（S10、S11）。 - 截斷序列 0.9、0.99、0.999 等所定的實數比 1 小一點點 → reject — (a_n)∼(1)，所以 [(a_n)]=ι(1)，兩者是同一個實數（S08、S09）。 - 實數線沒有空隙，所以完備性已經證明 → reject — 「沒有空隙」是直覺，不是證明；本稿沒有證明完備性（MKO）。 ## 結論與限制 在 Cauchy 完備化中，a_n=1−10^{−n} 是 Cauchy 序列，且對每個 ε>0 都有 N 使 |a_n−1|=10^{−n}<ε，所以 (a_n)∼(1)，[(a_n)]=ι(1)。ι 是單射，所以有限截斷 0.999=999/1000 所表示的實數不是 1。有限小數 0.375=3/8 是有理數，在 ℝ 中是 ι(3/8)。 - ℝ 上的加法、乘法、序與完備性，以及與 Dedekind 分割等其他建構的等價，未在本稿處理（MKO 指出需另外證明）。 - 與 Mathlib Real 的 Cauchy completion、有理數嵌入、線性序與完備性聲明的對接（MKO formal next）未在此處理。 - N8 只是 n=1 到 40 的有限檢查；10^n>n 的證明是 S05.1、S05.2 的歸納法。 ## 驗證及來源綁定 18 個本稿宣告算術檢查；只支持所列算式。 - source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f - adopted source SHA-256: cf5c66c9854af5d95d9c38472102f8e076b1a986cf8bbfbef4f0f539680fda81 - original source SHA-256: cf5c66c9854af5d95d9c38472102f8e076b1a986cf8bbfbef4f0f539680fda81 - Lean: NOT_RUN · independent AI: NOT_MEASURED [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/production-20261019/guides/derivation-mko-real-number-01.json)