# 完整因數分解與μ(30)

[← 導讀目錄](https://ocme.evemisslab.com/zh-Hant/derivations/) · [原始 MKO](https://ocme.evemisslab.com/zh-Hant/mko/mko-mobius-function/)

這是使用者已採用的自然語言教學導讀。有限／算術檢查不等於普遍證明；本輪未跑 Lean，各稿審查範圍見其修訂記錄。來源原有的狀態標籤保留為歷史資料。公式保留精確 TeX，不另造語意 AST。

derivation-mko-mobius-function-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

μ(30)=−1，μ(12)=0，μ(1)=1；30的全部divisor值加總為0。

正整數完整UPF與完整divisor cross-check，未完成分解不分類。





## 已知條件與符號


- calc


- G1 — 主例n=30，另核12與1；μ對平方因數為0、對k個distinct prime的squarefree整數為(−1)^k。


- \mu — Mobius函數
- D(n) — 全部positive divisors





## 規則與來源

本稿部分規則文字經本輪讀者釐清，屬於改述而非逐字引文；被引用的原始來源內容及雜湊沒有改動。


- calc · prerequisite — 假設精確整數算術、帶餘除法、整除與gcd的定義；同餘等式始終綁定明示模數。
- mko_definition · cited — 完整UPF certificate提供multiplicities與distinct-prime count。factor order不影響。sum_{d|n}mu(d)=1 if n=1 else0作精確cross-check。0與negative integers不在domain；incomplete trial division不得分類。 · mko-mobius-function





## 逐步主鏈

S01 · implies操作前

30=2\cdot15=2\cdot3\cdot5

操作後

30=2^1 3^1 5^1

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

完整trial extraction先取2再3，餘5只需試2；2、3、5均prime，乘積回到30。



S02 · implies操作前

(e_2,e_3,e_5)=(1,1,1)

操作後

30\text{ squarefree},\quad k=3

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

全部prime重數皆1，平方因數分支不觸發，distinct-prime count為3。



S03 · implies操作前

k=3

操作後

\mu(30)=(-1)^3=-1

條件：無

規則：mko_definition · 依賴：G1, S02

葉節點依據：mko_definition

按squarefree分支給符號−1。



S04 · implies操作前

30=2^1 3^1 5^1

操作後

D(30)=\{1,2,3,5,6,10,15,30\}

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

三個指數各只能取0或1，2³=8種選擇全部列出positive divisors。



S05 · implies操作前

d=1,2,3,5,6,10,15,30

操作後

\mu(d)=1,-1,-1,-1,1,1,1,-1\text{ respectively}

條件：無

規則：calc · 依賴：G1, S03, S04

葉節點依據：calc

每個divisor皆由同一完整分解繼承重數；empty product對1給1。



S06 · implies操作前

\sum_{d\mid30}\mu(d)

操作後

1-1-1-1+1+1+1-1=0

條件：無

規則：calc · 依賴：G1, S05

葉節點依據：calc

完整八項加總給n>1的精確cross-check。



S07 · implies操作前

12=2^2\cdot3

操作後

2^2\mid12\Rightarrow\mu(12)=0

條件：無

規則：calc · 依賴：G1, S02

葉節點依據：calc

2重複出現，故必先進平方因數分支，不能取(−1)²。



S08 · implies操作前

D(1)=\{1\},\quad\mu(1)=1

操作後

\sum_{d\mid1}\mu(d)=1;\quad n\le0\text{ outside domain}

條件：無

規則：mko_definition · 依賴：G1, S05, S07

葉節點依據：mko_definition

n=1另保留empty prime product與sum1；0、負整數不擴張定義。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S05, S07 — 本稿不定義 μ(0)，因此不能依本定義賦值為 0；0 不在此稿的分類定義域內。
- S07 · premise_audit · G1, S02 — 完整分解含重數2、1，distinct count2不足以分類。
- S06 · premise_audit · G1, S05 — 這次有限核對只認證30，不取代一般divisor-sum定理。
- S05 · premise_audit · G1, S03, S04 — 例如6有兩個prime給+1，30有三個給−1，不能用大小奇偶。
- S04 · premise_audit · G1, S01 — 列表同時含1與30，並非只列prime或proper divisors。
- S03 · premise_audit · G1, S02 — 因數排序不改3個prime的個數或重數。
- S02 · premise_audit · G1, S01 — 先核重數再數種類，不能只數三種就略平方條件。
- S01 · premise_audit · G1 — 沒有未分類的剩餘因子，才能讀multiplicities。





## 錯誤控制與反例

重數先行任何prime重數≥2就給0，distinct count不再決定符號。

完整分解未試到sqrt(remaining)前不可把剩餘數直接當prime。


- μ(12)=1因有兩種prime。 → reject — 2²整除12，故值0。
- μ(1)=−1。 → reject — 空prime product的k=0，(−1)^0=1。
- μ(0)=0依本定義。 → reject — domain是positive integers，0不分類。





## 結論與限制

μ(30)=−1，μ(12)=0，μ(1)=1；30的全部divisor值加總為0。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 3505226a6366d7f0fe4ff0cdea84d0829765aebda7ef89862b6364d7922604cd
- original source SHA-256: 59850a6096a974b7810ab0b6adb6274aa72c4c80f42e39bd8ed038c2ccad9727
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[同源完整 JSON（含公式、AST、反控制與修訂記錄）](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-mobius-function-01.json)