存在、Euclid引理與唯一質因數

目標與範圍

正整數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

逐步主鏈

n>1,\quad d=\min\{m>1:m\mid n\}

d\text{ prime}

n=dq,\quad d\text{ prime},\quad1\le q<n

q=1\Rightarrow n=d;\quad q>1\Rightarrow q\text{ has prime factors by induction}

p\text{ prime},\quad p\mid ab,\quad p\nmid a

\gcd(p,a)=1\Rightarrow\exists u,v:\ up+va=1

up+va=1,\quad p\mid ab

b=upb+vab\Rightarrow p\mid b

\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

p_1=q_j\ne0

\text{cancel }p_1\text{ and induct on }r+s\Rightarrow\{p_i\}_{\rm multiset}=\{q_j\}_{\rm multiset}

360

360=2\cdot180=2^2\cdot90=2^3\cdot45=2^3\cdot3\cdot15=2^3\cdot3^2\cdot5

2^3\cdot3^2\cdot5=360

360\text{ has multiset }\{2,2,2,3,3,5\}\text{ uniquely}

-360,\quad1,\quad-1,\quad0

-360=-(2^3 3^2 5),\quad\pm1\text{ use empty prime product};\quad0\text{ excluded}

局部子步與引理

本稿無局部子步。

逐步反向審查

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