# 存在、Euclid引理與唯一質因數 [← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-unique-prime-factorization/) 這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。 derivation-mko-unique-prime-factorization-01 · ocme-new142-reader-adoption-20261021 ## 目標與範圍 正整數n>1存在唯一質因數多重集合；360=2³·3²·5，負號與units另列。 以強歸納與明示Bezout前提證存在唯一性，再完整trial division核360。 ## 已知條件與符號 - calc - G1 — 主定理n∈Z,n>1；實例n=360；分解忽略因數順序但保留重數。 - p_i,q_j — 含重數的prime因子 - r,s — 有限因數個數 ## 規則與來源 - calc · prerequisite — 假設精確整數算術、帶餘除法、整除與gcd的定義；同餘等式始終綁定明示模數。另假設正整數良基／強歸納原理，以及互質整數的Bezout恆等式。 - mko_definition · cited — existence以well-founded/induction與完整trial division小切片驗證；uniqueness保留Euclid lemma witness p|ab implies p|a or p|b，而非只比較少數答案。整數版分離negative sign，±1為units與empty product，0沒有此prime factorization。 · mko-unique-prime-factorization ## 逐步主鏈 S01 · implies操作前 n>1,\quad d=\min\{m>1:m\mid n\} 操作後 d\text{ prime} 條件：無 規則：calc · 依賴：G1 葉節點依據：calc 若d=uv且11\Rightarrow q\text{ has prime factors by induction} 條件：無 規則：calc · 依賴：G1, S01 葉節點依據：calc 商比n小，強歸納提供q分解，乘回d證存在；n=2的基礎亦落q=1分支。 S03 · implies操作前 p\text{ prime},\quad p\mid ab,\quad p\nmid a 操作後 \gcd(p,a)=1\Rightarrow\exists u,v:\ up+va=1 條件：無 規則：calc · 依賴：G1 葉節點依據：calc p因數只有1、p，且p不整除a，故互質，可用明示Bezout前提。 S04 · implies操作前 up+va=1,\quad p\mid ab 操作後 b=upb+vab\Rightarrow p\mid b 條件：無 規則：calc · 依賴：G1, S03 葉節點依據：calc 乘b後兩項皆被p整除，證p|ab則p|a或p|b。 S05 · implies操作前 \prod_{i=1}^{r}p_i=\prod_{j=1}^{s}q_j,\quad p_i,q_j\text{ prime} 操作後 p_1\mid\prod_{j=1}^{s}q_j\Rightarrow\exists j:\ p_1\mid q_j\Rightarrow p_1=q_j 條件：無 規則：calc · 依賴：G1, S04 葉節點依據：calc 反覆對有限乘積使用Euclid引理，p₁必等於右側某個prime。 S06 · implies操作前 p_1=q_j\ne0 操作後 \text{cancel }p_1\text{ and induct on }r+s\Rightarrow\{p_i\}_{\rm multiset}=\{q_j\}_{\rm multiset} 條件：無 規則：calc · 依賴：G1, S02, S05 葉節點依據：calc 消去非零整數prime使總因數數下降，直到空乘積1；非空prime乘積≥2，不能等1。 S07 · implies操作前 360 操作後 360=2\cdot180=2^2\cdot90=2^3\cdot45=2^3\cdot3\cdot15=2^3\cdot3^2\cdot5 條件：無 規則：calc · 依賴：G1, S01, S02 葉節點依據：calc 完整抽取2三次與3兩次，餘5；2、3皆prime，餘5只需試2因3²>5，故5prime。 S08 · implies操作前 2^3\cdot3^2\cdot5=360 操作後 360\text{ has multiset }\{2,2,2,3,3,5\}\text{ uniquely} 條件：無 規則：mko_definition · 依賴：G1, S06, S07 葉節點依據：mko_definition 乘積精確重驗，並由一般唯一性證其他prime列表只有排列不同。 S09 · implies操作前 -360,\quad1,\quad-1,\quad0 操作後 -360=-(2^3 3^2 5),\quad\pm1\text{ use empty prime product};\quad0\text{ excluded} 條件：無 規則：calc · 依賴：G1, S06, S08 葉節點依據：calc 負號是單位因子；±1無prime因數而用空乘積1；0不屬n>1分解域。 ## 局部子步與引理 本稿無局部子步。 ## 逐步反向審查 - S09 · premise_audit · G1, S06, S08 — 0可被任意prime整除，不能給有限唯一prime多重集合。 - S08 · premise_audit · G1, S06, S07 — 不能只寫360=p^k，因這個例子有三種互異prime。 - S07 · premise_audit · G1, S01, S02 — 剩餘5不是未處理的合數；已完整核到平方根界。 - S06 · premise_audit · G1, S02, S05 — 唯一性保留重數，只忽略次序，空與非空終點亦已區分。 - S05 · premise_audit · G1, S04 — 不是只比兩個已算答案；對任意兩個有限prime分解適用。 - S04 · premise_audit · G1, S03 — 若p|a則直接在另一分支；合數p不保證前一步互質。 - S03 · premise_audit · G1 — 這一步標示實際用到的Bezout，不把Euclid引理當自證。 - S02 · premise_audit · G1, S01 — 歸納只用更小正整數，不用待證同一n。 - S01 · premise_audit · G1 — 集合非空因n自身是因數，最小值由良基前提保證。 ## 錯誤控制與反例 存在與唯一強歸納給存在，Euclid引理加消去給唯一，兩責任分開。 重數比較prime多重集合，不只distinct prime集合。 - 360=2³·3·5。 → reject — 右側120，漏掉一個3。 - Euclid引理對合數4也成立。 → reject — 4|2·2但4不整除任一2。 - 0的prime factorization是空乘積。 → reject — 空乘積是1，不是0。 ## 結論與限制 正整數n>1存在唯一質因數多重集合；360=2³·3²·5，負號與units另列。 ## 驗證及來源綁定 1 個本稿宣告算術檢查；只支持所列算式。 - source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f - adopted source SHA-256: 648c53ebc102df797ce25af2afb0b128976c45a091ff54b1a47d03de1a9d1ad6 - original source SHA-256: 648c53ebc102df797ce25af2afb0b128976c45a091ff54b1a47d03de1a9d1ad6 - Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW [同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-unique-prime-factorization-01.json)