# Complete factorization and mu(30)

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

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-function-01 · ocme-new142-reader-adoption-20261021



## Goal and scope

mu(30)=-1, mu(12)=0, mu(1)=1; the sum over every divisor of 30 is zero.

Complete positive-integer factorization and divisor cross-checks; incomplete factors give no classification.





## Givens and symbols


- calc


- G1 — Main n=30, with 12 and 1; mu is zero for a repeated prime factor and (-1)^k for a squarefree integer with k distinct primes.


- \mu — Mobius function
- D(n) — all positive divisors





## Rules and sources

Some rule statements have reader clarifications in this revision: they are paraphrases, not verbatim quotations. Referenced original source bytes and hashes are unchanged.


- calc · prerequisite — Assume exact integer arithmetic, division with remainder, and definitions of divisibility and gcd; every congruence has an explicit modulus.
- mko_definition · cited — A complete unique-prime-factorization certificate supplies multiplicities and the distinct-prime count, independently of factor order. The exact divisor-sum cross-check is sum over d dividing n of mu(d)=1 for n=1 and 0 otherwise. Zero and negative integers are outside the domain. Incomplete trial division does not justify classification. · mko-mobius-function





## Main derivation

S01 · impliesBefore

30=2\cdot15=2\cdot3\cdot5

After

30=2^1 3^1 5^1

Conditions: none

Rule: calc · Uses: G1

Leaf basis: calc

Complete trial extraction removes 2 then 3, leaving prime 5 after testing 2; the product returns 30.



S02 · impliesBefore

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

After

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

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

Every prime multiplicity is 1, so the square-factor branch does not apply and the distinct-prime count is 3.



S03 · impliesBefore

k=3

After

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

Conditions: none

Rule: mko_definition · Uses: G1, S02

Leaf basis: mko_definition

The squarefree branch gives sign -1.



S04 · impliesBefore

30=2^1 3^1 5^1

After

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

Conditions: none

Rule: calc · Uses: G1, S01

Leaf basis: calc

Each exponent is 0 or 1, and all 2^3=8 choices give the listed positive divisors.



S05 · impliesBefore

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

After

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

Conditions: none

Rule: calc · Uses: G1, S03, S04

Leaf basis: calc

Each divisor inherits complete multiplicities; the empty product for 1 gives 1.



S06 · impliesBefore

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

After

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

Conditions: none

Rule: calc · Uses: G1, S05

Leaf basis: calc

The complete eight-term sum gives the exact n>1 cross-check.



S07 · impliesBefore

12=2^2\cdot3

After

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

Conditions: none

Rule: calc · Uses: G1, S02

Leaf basis: calc

The repeated factor 2 forces the square-factor branch, not (-1)^2.



S08 · impliesBefore

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

After

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

Conditions: none

Rule: mko_definition · Uses: G1, S05, S07

Leaf basis: mko_definition

Retain the empty prime product and divisor sum 1 at n=1; zero and negatives are outside this definition.







## Substeps and lemmas

No substeps in this guide.





## Reverse audits


- S08 · premise_audit · G1, S05, S07 — mu(0) is not assigned zero; it is outside the classification domain.
- S07 · premise_audit · G1, S02 — Complete multiplicities are 2,1; distinct count 2 alone is insufficient.
- S06 · premise_audit · G1, S05 — This finite check certifies 30, not the general divisor-sum theorem.
- S05 · premise_audit · G1, S03, S04 — 6 has two primes giving +1 and 30 three giving -1; numerical parity is irrelevant.
- S04 · premise_audit · G1, S01 — The list includes both 1 and 30, not just prime or proper divisors.
- S03 · premise_audit · G1, S02 — Reordering factors changes neither the count nor multiplicities.
- S02 · premise_audit · G1, S01 — Check multiplicities before counting types; three distinct primes alone would not ensure squarefreeness.
- S01 · premise_audit · G1 — No remaining factor is unclassified, so multiplicities can be read.





## Error controls and negative controls

Multiplicity firstAny prime multiplicity at least 2 forces zero; distinct count then does not determine a sign.

Complete factorizationDo not label a remainder prime before trial division reaches its square-root bound.


- mu(12)=1 because there are two prime types. → reject — 2^2 divides 12, forcing zero.
- mu(1)=-1. → reject — The empty prime product has k=0, so (-1)^0=1.
- mu(0)=0 under this definition. → reject — The domain is positive integers; zero is unclassified.





## Result and limitations

mu(30)=-1, mu(12)=0, mu(1)=1; the sum over every divisor of 30 is zero.







## Verification and source binding

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


- source commit: b1b2f1dcf8c50d67a93fe52d95f8eef7b3abba9f
- adopted source SHA-256: 3505226a6366d7f0fe4ff0cdea84d0829765aebda7ef89862b6364d7922604cd
- original source SHA-256: 59850a6096a974b7810ab0b6adb6274aa72c4c80f42e39bd8ed038c2ccad9727
- 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-function-01.json)