自然數質數：證明 97 是質數、91 是合數，並排除 0 與 1

目標與範圍

依 MKO 定義（p 為質數 ⇔ 2≤p 且 p 的每個自然數因數 d 都滿足 d=1 或 d=p）：(1) 說明 0 與 1 不是質數；(2) 證明 2 是質數；(3) 以見證 7 證明 91 是合數，並說明只測 2、3、5 會誤判；(4) 證明「若 n=dk 且 d、k≥2，則 min(d,k)²≤n」，據此只需檢查 2 到 9，證明 97 是質數；(5) 證明 2 是唯一的偶質數。

只在包含 0 的自然數中工作，使用自然數整除與精確的整數比較（MKO 假設 a1、a2），不用浮點平方根。平方根界由本稿證明的引理給出。不處理質因數分解的唯一性、質數無窮多或大整數的質數證書；不改動 canonical MKO 或英文 edition。

已知條件與符號

• order_basics
• division_algorithm
• mul_zero
• numeric_evaluation

• G1 — p、d 是包含 0 的自然數；整除依 MKO 自然數整除，見證必須是自然數（MKO 假設 a1）。
• G2 — 因數判定用自然數整除與精確整數比較，不用近似平方根或浮點除法（MKO 假設 a2）。
• G3 — 候選：0、1、2、91、97，以及大於 2 的偶數。

• p — 候選的自然數
• d\mid p — d 整除 p
• m=\min(d,k) — 因數對中較小者
• n\bmod m — n 除以 m 的餘數

規則與來源

• 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。
• division_algorithm · prerequisite — 帶餘除法：對整數 a 與正整數 b，存在唯一的整數 q、r 使 a=bq+r 且 0≤r<b。
• mul_zero · prerequisite — 乘以零：u·0=0。理由：u·0=u·(0+0)=u·0+u·0，兩邊同減 u·0 得 0=u·0。
• numeric_evaluation · prerequisite — 明確整數或有理數算式的精確求值；可以獨立重算。
• def_unfold · prerequisite — 展開定義：把一個已定義的詞換成它的定義內容（或反向收回），命題的真假不變。
• exists_elim · prerequisite — ∃消去：由 ∃x∈D, P(x)，可取一個新名字 a 表示某個滿足 P(a) 的元素；只要最後結論不含 a，就可用 a 推理。
• contradiction · prerequisite — 反證法：若假設 ¬P 推出矛盾（某命題與其否定同時成立），則 P 成立。
• mul_one · prerequisite — 乘法單位元：1·u=u。
• case_analysis · prerequisite — 分情況論證：若 P∨Q 成立，且 P⇒R、Q⇒R 都已證，則 R 成立。所有情況必須涵蓋全部可能。
• exists_intro · prerequisite — ∃引入：若找到 a∈D 使 P(a) 成立，則 ∃x∈D, P(x)。
• mul_comm · prerequisite — 乘法交換律：uv=vu（在交換的數系中，例如 ℤ、ℚ、ℝ、ℂ）。
• quantifier_negation · prerequisite — 量詞否定：¬(∀x, P(x)) 等價於 ∃x, ¬P(x)；¬(∃x, P(x)) 等價於 ∀x, ¬P(x)。
• forall_intro · prerequisite — ∀引入（全稱推廣）：若某命題對一個「任意的」元素 x 證成，而證明沒有對 x 加任何額外假設，則它對論域中所有 x 成立。
• mko_prime_def · cited — 自然數 p 為質數，當且僅當 2≤p，且每個自然數 d 若 d∣p，則 d=1 或 d=p。0 與 1 都不是質數。 · mko-prime-number
• mko_dvd_def · cited — 對自然數 a、b，a∣b 當且僅當存在自然數 k 使 b=a·k。 · mko-natural-divisibility
• rem_test · prerequisite — 對自然數 n 與正自然數 m：m∣n ⇔ n 除以 m 的餘數為 0（由帶餘除法的唯一性得到）。
• L_div_bound · lemma — 若 d∣n、n>0，且 n=dk，則 d≥1、k≥1 且 d≤n。
• L_small_factor · lemma — 若 n=d·k，且 d≥2、k≥2，則 m=min(d,k) 滿足 2≤m、m∣n 且 m²≤n。

逐步主鏈

p\ \text{prime}

2\le p\ \land\ \forall d\in\mathbb{N}\,(d\mid p\Rightarrow d=1\lor d=p)

d\mid n,\ n>0

1\le d\le n

p=0,\ p=1

0,\ 1\ \text{not prime}

p=2

2\ \text{prime}

91=7\cdot 13

7\mid 91,\ 7\notin\{1,91\};\ 91\ \text{not prime}

91\bmod 2=91\bmod 3=91\bmod 5=1

2,3,5\nmid 91,\ \text{yet}\ 91\ \text{is composite}

d\mid 97,\ d\neq 1,\ d\neq 97

97=dk,\ 2\le d\le 96,\ k\ge 2

97=dk,\ d\ge 2,\ k\ge 2

m=\min(d,k):\ 2\le m,\ m\mid 97,\ m^2\le 97

m^2\le 97

2\le m\le 9

m\in\{2,3,4,5,6,7,8,9\}

97\bmod m\in\{1,1,1,2,1,6,1,7\}\neq 0,\ \text{so}\ m\nmid 97

\text{assumption of S07 leads to a contradiction}

\forall d\,(d\mid 97\Rightarrow d=1\lor d=97);\ 97\ \text{prime}

91,\ 9^2\le 91<10^2

\text{the complete search}\ 2\le m\le 9\ \text{finds}\ 7

p=2j,\ p\ge 2,\ p\neq 2

2\mid p,\ 2\notin\{1,p\};\ p\ \text{not prime}

局部子步與引理

n=dk,\ n>0

d\ge 1,\ k\ge 1

k\ge 1,\ d\ge 0

n=dk\ge d\cdot 1=d

n=dk

d\mid n,\ k\mid n,\ \text{so}\ m\mid n

m\le d,\ m\le k,\ m\ge 0

m^2=m\cdot m\le d\cdot m\le d\cdot k=n

逐步反向審查

• S13 · premise_audit · S01, S04, mko_dvd_def — 一般論證對每個偶數 p≠2 成立；有限核對 N21 不是證明的一部分。
• S12 · premise_audit · S05, L_small_factor — 引理保證合數在界內有因數；這裡只是說明完整搜尋與部分搜尋的差別。
• S11 · sufficient_goal_reduction · S07, S10, contradiction, mko_prime_def — 目標 G：97 是質數。足夠條件 H：97≥2 且沒有非平凡因數；H⇒G 由定義。H 由反證法證成，沒有把 G 當作前提；N15 只是交叉核對，不是證明的一部分。
• S10 · premise_audit · S09, rem_test, case_analysis — 八種情況窮盡 2≤m≤9 的所有 m；這是完整檢查，不是抽樣。
• S09 · premise_audit · S08, order_basics, G2 — 上界必須涵蓋所有 m²≤97 的 m；取 9 不多也不少。
• S08.2 · premise_audit · order_basics — 乘以非負數保持 ≤；沒有使用引理本身。
• S08.1 · premise_audit · mko_dvd_def, mul_comm, exists_intro — 只用交換律與見證；沒有使用引理本身。
• S08 · premise_audit · S07, L_small_factor — 引理需要 d、k 都至少為 2，由 S07 提供。
• S07 · premise_audit · S02, exists_elim — 這是反證法的假設與它的直接推論；結論要到 S11 才釋放假設。
• S06 · premise_audit · S05, rem_test — 這一步只顯示部分檢查的不足，不改變 S05 的結論。
• S05 · premise_audit · S01, mko_dvd_def, numeric_evaluation — 否定只需一個非平凡因數。
• S04 · premise_audit · S01, S02, case_analysis — 因數範圍 1 到 2 已窮盡；沒有遺漏的候選。
• S03 · premise_audit · S01, S02, mul_zero — 否定只需一個條件失敗；這裡同時說明哪個條件對 1 是決定性的。
• S02.2 · premise_audit · order_basics, mul_one — 乘以非負數保持 ≤；沒有使用引理本身。
• S02.1 · premise_audit · mul_zero, contradiction — 只用乘以零；沒有使用引理本身。
• S02 · premise_audit · L_div_bound — 需要 n>0；n=0 時每個 d 都整除 0，沒有上界（S03）。
• S01 · premise_audit · G1, mko_prime_def — 此步只展開定義，不推出新事實。

錯誤控制與反例

1 不是質數

MKO 指出的誤解：把 1 列為質數。1 的因數確實只有 1，但定義另要求 2≤p，所以 1 不是質數（S03）。0 則連因數條件也失敗，因為 2∣0。

只測少數小因數不夠

MKO 指出的另一個誤解：只測少數小因數就宣稱是質數。91 不被 2、3、5 整除，卻等於 7·13（S06）。肯定質數必須排除所有可能的非平凡因數；引理 L_small_factor 把範圍縮到 m²≤n，但範圍內的每個 m 都要檢查（S10、S12）。

平方根界要用精確整數比較

MKO 假設 a2 不允許用近似平方根。本稿以 m²≤97 與 10²=100>97 精確決定上界 9；若用四捨五入的浮點 √n 決定上界，在 n 是完全平方數附近可能少檢查一個候選。

• 1 是質數，因為它的因數只有 1 與它自己 → reject — 定義要求 2≤p，1 不滿足。
• 91 不被 2、3、5 整除，所以 91 是質數 → reject — 91=7·13；部分檢查不是證明。
• 要證 97 是質數，必須試除 2 到 96 的每一個數 → reject — 引理 L_small_factor 證明若有非平凡因數，必有一個 m 滿足 2≤m≤9，所以檢查 2 到 9 已足夠。
• 0 是質數，因為 0 沒有因數 → reject — 每個自然數都整除 0（例如 0=2·0），而且 2≤0 不成立。
• 所有質數都是奇數 → reject — 2 是質數（S04）且是偶數。

結論與限制

0 與 1 不是質數（2≤p 失敗；1 雖只有因數 1，仍被排除）；2 是質數，也是唯一的偶質數；91=7·13 是合數，只測 2、3、5 會漏掉 7；由 min(d,k)²≤n 只需檢查 2 到 9，而 97 除以 2 到 9 的餘數都不為 0，所以 97 是質數。

• rem_test 作為前置規則使用，其證明見自然數整除的教學稿。
• 只試除 2 到 9 中的質數（2、3、5、7）其實也足夠，但需要「最小的非平凡因數必為質數」這個額外事實，本稿沒有使用也沒有證明。
• N15、N16、N22 使用核對器內建的質數判定，只作獨立交叉核對；N21 是有限範圍核對。

驗證及來源綁定

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

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

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