階乘：遞迴定義的唯一性、乘積形式與 5! 的計算

目標與範圍

只用 F(0)=1 與 F(n+1)=(n+1)F(n)（n∈ℕ，ℕ 含 0）：(1) 證明滿足這兩條的函數 ℕ→ℕ 只有一個；(2) 證明對所有 n 有 F(n)=∏_{k=1}^{n} k（空乘積為 1），所以 n>0 時 n! 是從 1 到 n 所有整數的乘積；(3) 證明每個 F(n)≥1，特別是 0!=1≠0；(4) 由遞迴逐步算出 5!=120。

在 MKO 的範圍內：自然數含 0（假設 a1），以遞迴定義的函數 F。F 的存在取自 MKO 的陳述（遞迴定理不在本稿證明）；本稿證明唯一性、乘積形式與正性。不證明「n! 計數 n 元集合的排列」（MKO 指出那是另需證明的定理）；不改動 canonical MKO 或英文 edition。

已知條件與符號

• nat_induction
• function_def
• eq_replace
• mul_comm
• order_basics
• numeric_evaluation

• G1 — ℕ 包含 0；n 是自然數（MKO 假設 a1）。
• G2 — F:ℕ→ℕ 滿足 F(0)=1，且對每個 n∈ℕ 有 F(n+1)=(n+1)F(n)；記 n!=F(n)。這樣的 F 存在，取自 MKO 的陳述。

• F,\ n! — 階乘函數及其記號 n!=F(n)
• G — 任一滿足同樣兩條等式的函數
• \mathbb{N} — 含 0 的自然數
• \prod_{k=1}^{n} k — 1 到 n 的整數乘積，n=0 時為 1
• P(n) — 乘積 ∏_{k=1}^{n} k 作為 n 的函數

規則與來源

• nat_induction · prerequisite — 數學歸納原理：對從 n₀ 起的命題族 P(n)，若 P(n₀) 成立，且對每個 n≥n₀ 都有 P(n)⇒P(n+1)，則所有 n≥n₀ 都有 P(n)。
• function_def · prerequisite — 函數：f:A→B 對每個 a∈A 指定恰好一個 f(a)∈B。兩函數相等 ⇔ 定義域、對應域相同且對每個 a 都有相同值。
• eq_replace · prerequisite — 等值代換：命題中的一個式子可換成與它相等的式子，命題的真假不變。
• mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
• 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。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• def_intro · prerequisite — 引入定義：可為一個命題、式子或物件取名；之後名稱與被定義者可互相替換。
• eq_refl_symm_trans · prerequisite — 等號的性質：u=u；若 u=v 則 v=u；若 u=v 且 v=w 則 u=w。
• forall_elim · prerequisite — ∀消去（代入特例）：若 ∀x∈D, P(x) 成立且 a∈D，則 P(a) 成立。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• mul_one · prerequisite — 乘法單位元：1·u=u。
• and_intro_elim · prerequisite — 合取：由 P 與 Q 得 P∧Q；由 P∧Q 可分別得 P 與 Q。
• mko_factorial_def · cited — 函數 F:ℕ→ℕ 由 F(0)=1 與 F(n+1)=(n+1)F(n) 唯一遞迴決定；慣用記號為 n!。 · mko-factorial
• prod_def · prerequisite — 有限乘積：∏_{k=1}^{0} a_k=1（空乘積），且 ∏_{k=1}^{n+1} a_k=(∏_{k=1}^{n} a_k)·a_{n+1}。
• nat_closure · prerequisite — 自然數的和與積仍是自然數；對每個 n∈ℕ 有 n+1≥1>0。
• L_pos · lemma — 對每個 n∈ℕ，F(n)≥1。

逐步主鏈

n!

F(0)=1,\ \ F(n+1)=(n+1)F(n)\ \ (n\in\mathbb{N})

G:\mathbb{N}\to\mathbb{N},\ G(0)=1,\ G(n+1)=(n+1)G(n)

Q(n):\ G(n)=F(n)

G(0),\ F(0)

G(0)=1=F(0)

G(n)=F(n)

G(n+1)=F(n+1)

Q(0),\ \ Q(n)\Rightarrow Q(n+1)

G=F\ \text{for every such}\ G

P(n)=\prod_{k=1}^{n} k

P:\mathbb{N}\to\mathbb{N}

P(0)=\prod_{k=1}^{0} k

P(0)=1

P(n+1)=P(n)\cdot(n+1)

P(n+1)=(n+1)P(n)

P(0)=1,\ \ P(n+1)=(n+1)P(n)

F(n)=\prod_{k=1}^{n} k\ \text{for every}\ n\in\mathbb{N}

F(n)

F(n)\geq 1\ \text{for every}\ n\in\mathbb{N};\ \text{in particular}\ 0!=1\neq 0

F(0)=1

F(1)=1,\ F(2)=2,\ F(3)=6

F(3)=6

F(4)=24,\ F(5)=120

\prod_{k=1}^{5} k

1\cdot 2\cdot 3\cdot 4\cdot 5=120=F(5)

S05,\ S09,\ S10,\ S12

\text{goals (1) to (4) established}

局部子步與引理

F(0)=1

F(0)\geq 1

F(n)\geq 1

F(n+1)=(n+1)F(n)\geq 1

逐步反向審查

• S14 · sufficient_goal_reduction · S05, S09, S10, S12, and_intro_elim — 目標 G：(1) 到 (4) 同時成立。足夠條件 H：S05、S09、S10、S12 各自成立；H⇒G 由合取引入。H 由定義與歸納正向證成，沒有把 G 當作前提。
• S13 · premise_audit · S09, S12, prod_def — 這只是 n=5 的一致性核對；S09 的一般結論來自唯一性，不來自這個例子。
• S12 · premise_audit · S11, forall_elim, numeric_evaluation — 精確整數乘法（N4、N5），沒有使用浮點近似。
• S11 · premise_audit · S01, forall_elim, numeric_evaluation — 每個值都依賴前一個值，必須按順序計算；乘法可獨立重算（N1 到 N3）。
• S10.2 · premise_audit · nat_closure, order_basics, nat_induction — 乘以 n+1 保持不等號方向需要 n+1>0；若乘的是可能為 0 的數（例如錯誤遞迴 n·F(n) 在 n=0），結論就會失敗。
• S10.1 · premise_audit · S01, order_basics — 只用到定義的起始值。
• S10 · premise_audit · L_pos — 結論只宣稱 F(n)≥1，不宣稱更強的下界。
• S09 · premise_audit · S05, S06, S07, S08, forall_elim — 套用唯一性需要 P 滿足同樣的起始值與同樣的遞迴，兩者分別由 S07、S08 提供。不是靠核對幾個 n 得到的。
• S08 · inverse_equivalence · mul_comm — 交換律是恆等式，兩種寫法表示同一個數，雙向成立。
• S07 · inverse_equivalence · prod_def — 兩邊依定義是同一個數，等式雙向成立。
• S06 · premise_audit · prod_def, nat_closure, nat_induction — 要套用 S05，P 必須是 ℕ→ℕ 的函數；這一步確認了對應域。
• S05 · premise_audit · S03, S04, nat_induction, function_def, forall_intro — 需要基礎 S03 與歸納步 S04 兩者；只檢查前幾個 n 不能代替歸納步。此步只證唯一性，存在性來自 MKO。
• S04 · premise_audit · S01, S02, eq_replace — 只用到同一個 n 的歸納假設與兩條遞迴；n 是任意的，沒有加條件。不宣稱反向（由 Q(n+1) 推回 Q(n)）。
• S03 · premise_audit · S01, S02, eq_refl_symm_trans — 需要兩個函數的起始值相同；若 G(0)=0，基礎就不成立（見錯誤控制一）。
• S02 · premise_audit · S01, def_intro — 對 G 不加任何其他假設，這是 S05 能對所有這樣的 G 下結論（全稱推廣）的前提。
• S01 · premise_audit · G1, G2, mko_factorial_def — 此步只寫出定義，不推出新事實。F 的存在是 MKO 提供的前提；唯一性在 S02 到 S05 證明。

錯誤控制與反例

0! 是 1，不是 0

MKO 指出常見誤解是把 0! 當成 0。F(0)=1 是定義的一部分。若把起點改成 H(0)=0 而保留 H(n+1)=(n+1)H(n)，則依歸納每個 H(n) 都是 0（H(n+1)=(n+1)·0=0），整個函數塌成 0，5! 會變成 0 而不是 120。空乘積為 1 的慣例（S07）也與 F(0)=1 一致。

n! 不是「n 倍」

MKO 指出另一個誤解是把 n! 當成 n 倍。遞迴每一步都乘上新的因數 n+1，所以 n! 累積了從 1 到 n 的所有因數：3!=6 不是 3，5!=120 不是 5，也不是 5·5=25。另一個常見的差一錯誤是寫成 H(n+1)=n·H(n)：此時 H(1)=0·H(0)=0，之後全為 0。

用精確整數，不用浮點近似

MKO 提醒不可用超出安全範圍的浮點值冒充精確結果。23!=25852016738884976640000=2¹⁹·49308808782358125，其奇數部分大於 2⁵³=9007199254740992。IEEE 754 binary64 的有效數具有 53 位元精度，一個正整數（在指數範圍內）可精確表示當且僅當它的奇數部分小於 2⁵³，所以 binary64 無法精確表示 23!。本稿的計算全部用精確整數乘法。

• 0!=0 → reject — 定義給出 F(0)=1；且 S10 證明每個 F(n)≥1。
• 把遞迴寫成 H(n+1)=n·H(n)、H(0)=1，定義的是同一個階乘 → reject — H(1)=0·1=0，但 F(1)=1。
• 對 n=0 到 5 核對 F(n)=∏_{k=1}^{n} k 成立，就證明了所有 n 都成立 → reject — 有限檢查只涵蓋那些 n；一般結論來自 S05 的唯一性（歸納法）。
• 以 binary64 浮點計算得到的 23! 就是精確值 → reject — 23! 的奇數部分大於 2⁵³，binary64 無法精確表示。

結論與限制

由 F(0)=1 與 F(n+1)=(n+1)F(n) 決定的函數只有一個；它等於乘積 ∏_{k=1}^{n} k（n=0 時為空乘積 1），每個值都至少為 1，所以 0!=1 而不是 0；逐步代入得 1!=1、2!=2、3!=6、4!=24、5!=120。

• F 的存在（遞迴定理）取自 MKO 的陳述，本稿未證明；本稿證明的是唯一性與由此推出的性質。
• N8、N9 是以 Python 標準函式 factorial 對 n=0 到 30 的有限核對，只支持這些 n，論證不依賴它們。
• 錯誤控制三關於 binary64 的敘述依據 IEEE 754 binary64 格式有 53 位元有效數精度這一事實，本稿未核對標準原文。

驗證及來源綁定

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

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: 20f46251e6543f0cb88df555a6522f263111c7e35fd4a025a2b6b776eb0bc6c5
• original source SHA-256: 20f46251e6543f0cb88df555a6522f263111c7e35fd4a025a2b6b776eb0bc6c5
• Lean: NOT_RUN · independent AI: NOT_MEASURED

同源完整 JSON（含公式、AST、反控制與修訂記錄）