# 仿射函數在divisor poset的反演

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

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

derivation-mko-mobius-inversion-finite-divisors-01 · ocme-new142-reader-adoption-20261021



## 目標與範圍

f(k)=2k+1、n=6時，F(6)=28且反演得到f(6)=13；n=1亦roundtrip。

正整數6的全部divisors與exact仿射題族；只核這個有限反演證書。





## 已知條件與符號


- calc


- G1 — f(k)=2k+1，F(m)=Σ_{d|m}f(d)；n=6，使用μ(d)F(6/d)索引。


- F — divisor forward transform
- f — 仿射原函數2k+1





## 規則與來源


- calc · prerequisite — 假設精確整數算術、帶餘除法、整除與gcd的定義；同餘等式始終綁定明示模數。
- mko_definition · cited — positive integer n上，若F(n)=sum_{d|n}f(d)，則f(n)=sum_{d|n}mu(d)F(n/d)。等價index形式可用mu(n/d)F(d)，但不得混合。必須枚舉全部positive divisors並由完整UPF取得mu；n=1與mu(1)=1保留。這是divisor-poset convolution，不是d≤n。 · mko-mobius-inversion-finite-divisors





## 逐步主鏈

S01 · implies操作前

6=2\cdot3

操作後

D(6)=\{1,2,3,6\}

條件：無

規則：calc · 依賴：G1

葉節點依據：calc

完整prime分解兩指數0或1產生全部四divisors。



S02 · implies操作前

d=1,2,3,6

操作後

f(d)=3,5,7,13\text{ respectively}

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

依同一仿射公式逐個精確代入。



S03 · implies操作前

D(1)=\{1\},\ D(2)=\{1,2\},\ D(3)=\{1,3\}

操作後

F(1)=3,\quad F(2)=3+5=8,\quad F(3)=3+7=10

條件：無

規則：calc · 依賴：G1, S01, S02

葉節點依據：calc

為反演所需每個quotient建立完整forward sums。



S04 · implies操作前

D(6)=\{1,2,3,6\}

操作後

F(6)=3+5+7+13=28

條件：無

規則：calc · 依賴：G1, S01, S02

葉節點依據：calc

完整forward transform包含1與n自身。



S05 · implies操作前

d=1,2,3,6

操作後

\mu(d)=1,-1,-1,1;\quad6/d=6,3,2,1

條件：無

規則：calc · 依賴：G1, S01

葉節點依據：calc

完整UPF給四個μ值，同時列出配對quotients避免索引混合。



S06 · implies操作前

\sum_{d\mid6}\mu(d)F(6/d)

操作後

28-10-8+3=13=f(6)

條件：無

規則：mko_definition · 依賴：G1, S03, S04, S05

葉節點依據：mko_definition

四項精確逆變換重建原值13。



S07 · implies操作前

F(6)-F(3)-F(2)+F(1)

操作後

f(1)(1-1-1+1)+f(2)(1-1)+f(3)(1-1)+f(6)=f(6)

條件：無

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

葉節點依據：calc

展開所有forward sums，直接看低divisor項係數消去，解釋本例反演機制。



S08 · implies操作前

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

操作後

F(1)=f(1)=3,\quad\mu(1)F(1)=3

條件：無

規則：calc · 依賴：G1, S03, S05, S07

葉節點依據：calc

最小domain點保留μ(1)=1，roundtrip完整。







## 局部子步與引理

本稿無局部子步。





## 逐步反向審查


- S08 · premise_audit · G1, S03, S05, S07 — 0、負數或不完整divisors不在此證書域。
- S07 · premise_audit · G1, S03, S04, S06 — 每個f只依divisibility出現，不是一般d≤n前綴和。
- S06 · premise_audit · G1, S03, S04, S05 — 若改用μ(6/d)F(d)整體換索引亦可，但不能只換半邊。
- S05 · premise_audit · G1, S01 — d=6對F(1)，不是對F(6)。
- S04 · premise_audit · G1, S01, S02 — 只加proper divisors會得15而非28，破壞roundtrip。
- S03 · premise_audit · G1, S01, S02 — F(3)不含f(2)，因2不整除3。
- S02 · premise_audit · G1, S01 — 只需這四個f值，不是把1至6全加總。
- S01 · premise_audit · G1 — 4、5雖小於6卻不整除6，不能混入。





## 錯誤控制與反例

索引配對同一項是μ(d)F(n/d)，或完整同步改為μ(n/d)F(d)。

完整divisors包括1與n，不以prime或proper列表替代。


- F(6)要加f(4)、f(5)。 → reject — 4與5不是6的divisors。
- 反演可把每項都配F(d)但保留μ(d)。 → reject — 3−8−10+28=13在本例巧合成立，但n=2時3−8=−5≠5；正確需同步換μ為μ(n/d)。
- 只列prime divisors就能反演。 → reject — 漏1與6會只得−10−8=−18，不是13。





## 結論與限制

f(k)=2k+1、n=6時，F(6)=28且反演得到f(6)=13；n=1亦roundtrip。







## 驗證及來源綁定

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: a3d906c53553c720d08fa4763944293d886bfad9ea166a77f4ae2c1399c65f18
- original source SHA-256: a3d906c53553c720d08fa4763944293d886bfad9ea166a77f4ae2c1399c65f18
- 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-inversion-finite-divisors-01.json)