實數：在 Cauchy 完備化中證明「循環的 9」與有理數 1 是同一個實數

目標與範圍

在以有理數 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}<ε。

逐步主鏈

\mathbb{R}

\{[(a_n)]\mid (a_n)\ \text{Cauchy in}\ \mathbb{Q}\},\ \iota(q)=[(q)_{n\ge1}]

[(a_n)]=[(b_n)]

(a_n)\sim(b_n)

a_n=1-10^{-n}\ \ (n\ge1)

a_1=\tfrac{9}{10},\ a_2=\tfrac{99}{100},\ a_3=\tfrac{999}{1000}

a_n-1

-10^{-n},\quad |a_n-1|=10^{-n}

n\ge 1\ \text{an integer}

10^n>n

\varepsilon\in\mathbb{Q},\ \varepsilon>0

\exists N\ \forall n\ge N:\ 10^{-n}<\varepsilon

(a_n)_{n\ge1}

(a_n)\ \text{is Cauchy}

(a_n),\ (1)_{n\ge1}

(a_n)\sim(1)_{n\ge1}

(a_n)\sim(1)_{n\ge1}

[(a_n)]=\iota(1)

p\neq q\ \text{in}\ \mathbb{Q}

\iota(p)\neq\iota(q)

\tfrac{999}{1000}\neq 1

\iota(\tfrac{999}{1000})\neq\iota(1)

0.375

\tfrac{375}{1000}=\tfrac{3}{8},\quad \iota(\tfrac{3}{8})\in\mathbb{R}

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

局部子步與引理

n=1

10^1=10>1

10^n>n\ \ (n\ge1)

10^{n+1}>n+1

\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

N:=s,\ n\ge N

10^{-n}<\tfrac{1}{n}\le\tfrac{1}{s}\le\tfrac{r}{s}=\varepsilon

逐步反向審查

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