# Divisor-poset inversion of an affine function

[← Guide index](https://ocme.evemisslab.com/en/derivations/) · [Original MKO](https://ocme.evemisslab.com/en/mko/mko-mobius-inversion-finite-divisors/)

This is an owner-adopted natural-language teaching guide. Finite/arithmetic checks are not universal proofs; no Lean was run, and review scope is recorded per revision. Original source status labels are retained as historical data. Formulas retain exact TeX; no new semantic AST is invented.

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



## Goal and scope

For f(k)=2k+1 at n=6, F(6)=28 and inversion returns f(6)=13; n=1 roundtrips too.

Every divisor of positive integer 6 and an exact affine family; only this finite inversion certificate is claimed.





## Givens and symbols


- calc


- G1 — f(k)=2k+1, F(m)=sum of f(d) over d dividing m; n=6, with indexing mu(d)*F(6/d).


- F — divisor forward transform
- f — affine function 2k+1





## Rules and sources


- calc · prerequisite — Assume exact integer arithmetic, division with remainder, and definitions of divisibility and gcd; every congruence has an explicit modulus.
- mko_definition · cited — For positive integer n, F(n)=sum over d|n of f(d) implies f(n)=sum over d|n of mu(d)*F(n/d). The equivalent indexing mu(n/d)*F(d) is valid but must not be mixed with the first convention. Enumerate every positive divisor and derive mu from complete prime multiplicities. Retain n=1 and mu(1)=1. This is convolution on the divisor poset, not a sum over all d≤n. · mko-mobius-inversion-finite-divisors





## Main derivation

S01 · impliesBefore

6=2\cdot3

After

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

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

The complete factorization and exponents zero or one give all four divisors.



S02 · impliesBefore

d=1,2,3,6

After

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

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

Evaluate the same affine formula exactly at every divisor.



S03 · impliesBefore

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

After

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

Conditions: none

Rule: calc · Uses: G1, S01, S02

Leaf basis: calc

Build complete forward sums for each quotient needed by inversion.



S04 · impliesBefore

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

After

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

Conditions: none

Rule: calc · Uses: G1, S01, S02

Leaf basis: calc

The full forward transform includes 1 and n itself.



S05 · impliesBefore

d=1,2,3,6

After

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

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

Complete factorization gives all four mu values, with paired quotients to prevent index mixing.



S06 · impliesBefore

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

After

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

Conditions: none

Rule: mko_definition · Uses: G1, S03, S04, S05

Leaf basis: mko_definition

The exact four-term inverse transform reconstructs 13.



S07 · impliesBefore

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

After

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

Conditions: none

Rule: calc · Uses: G1, S03, S04, S06

Leaf basis: calc

Expand all forward sums to see lower-divisor coefficients cancel, explaining inversion in this instance.



S08 · impliesBefore

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

After

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

Conditions: none

Rule: calc · Uses: G1, S03, S05, S07

Leaf basis: calc

The smallest domain point retains mu(1)=1 and roundtrips exactly.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S03, S05, S07 — Zero, negatives and incomplete divisor lists are outside this certificate.
- S07 · premise_audit · G1, S03, S04, S06 — Terms appear according to divisibility, not an ordinary d≤n prefix sum.
- S06 · premise_audit · G1, S03, S04, S05 — The fully reindexed mu(6/d)F(d) is also valid; changing only one side is not.
- S05 · premise_audit · G1, S01 — d=6 pairs with F(1), not F(6).
- S04 · premise_audit · G1, S01, S02 — Using only proper divisors gives 15, not 28, breaking the roundtrip.
- S03 · premise_audit · G1, S01, S02 — F(3) excludes f(2) because 2 does not divide 3.
- S02 · premise_audit · G1, S01 — Only these four f-values are used, not all integers 1 through 6.
- S01 · premise_audit · G1 — 4 and 5 are below 6 but do not divide it.





## Error controls and negative controls

Index pairingEach term is mu(d)F(n/d), or a fully reindexed mu(n/d)F(d).

All divisorsInclude 1 and n, not just prime or proper divisors.


- F(6) includes f(4),f(5). → reject — 4 and 5 are not divisors of 6.
- Use F(d) with unchanged mu(d) in every inverse term. → reject — Here 3-8-10+28 happens to be 13, but at n=2,3-8=-5 differs from 5; correct reindexing changes mu to mu(n/d).
- Prime divisors alone suffice for inversion. → reject — Omitting 1 and 6 leaves -10-8=-18, not 13.





## Result and limitations

For f(k)=2k+1 at n=6, F(6)=28 and inversion returns f(6)=13; n=1 roundtrips too.







## Verification and source binding

2 declared checks for this guide; only the listed expressions are covered.


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: a3d906c53553c720d08fa4763944293d886bfad9ea166a77f4ae2c1399c65f18
- original source SHA-256: a3d906c53553c720d08fa4763944293d886bfad9ea166a77f4ae2c1399c65f18
- Lean: NOT_RUN · independent AI: SCOPED_LEAD_AND_BILINGUAL_CONTEXT_REVIEW

[Same-source full JSON (formulas, ASTs, controls and revision log)](https://ocme.evemisslab.com/data/derivations/coverage-20261021/guides/derivation-mko-mobius-inversion-finite-divisors-01.json)