TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-07-31

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The number-theoretic Möbius function is the poset Möbius function of divisibility: $μ (n) = μ_{∣} (1, n)$

Statement

For every positive integer $n$ ,

$μ (n) = μ_{∣} (1, n),$

where the left side is The number-theoretic Möbius function $μ (n)$ from prime factorisation and the right side is the poset Möbius function of positive-integer divisibility (The integer-valued Möbius function $μ_{P}$ of a locally finite poset). More generally, if $d ∣ n$ , then

$μ_{∣} (d, n) = μ (n / d) .$

Facts & Assumptions

Given: A positive integer $n$ and, for the general clause, a positive divisor $d$ of $n$ .

[L1]

A divisor interval for quotient $q$ is order-isomorphic to a finite product of exponent chains ${0, \dots, v_{p_{i}} (q)}$ (The divisibility poset is lower-finite, and each divisor interval factorises as a product of finite chains of prime exponents).

[L2]

The Möbius function of a product poset is the product of the factor Möbius functions (The Möbius function of a product poset is the product of the Möbius functions).

[L3]

The endpoint Möbius value of a finite chain is $1$ for a one-point chain, $- 1$ for a two-point chain, and $0$ for a longer chain (On a finite chain, the Möbius function is $1$ on the diagonal, $- 1$ on covers and $0$ on longer intervals).

[L4]

The diagonal and interval-sum recurrence uniquely determine the Möbius function, so a poset isomorphism transports its values (The Möbius recurrence: $μ_{P} (x, x) = 1$ and both interval sums of $μ_{P}$ vanish when $x < y$ ).

[F1]

The prime-factor definition gives $0$ when some exponent is at least $2$ , and otherwise gives $(- 1)^{r}$ for the $r$ exponents equal to $1$ (The number-theoretic Möbius function $μ (n)$ from prime factorisation).

Proof

technique · direct

1.1

Apply [L1] to $[1, n]$ . Transporting through its order isomorphism by [L4] and iterating [L2], its endpoint Möbius value is the product over the prime exponents $e_{i} = v_{p_{i}} (n)$ of the endpoint values of the chains ${0, \dots, e_{i}}$ .

L1L2L4

2.1

If some $e_{i} \geq 2$ , [L3] makes one factor $0$ , so the product is $0$ . If every $e_{i} = 1$ , every factor is $- 1$ , so the product is $(- 1)^{r}$ . For $n = 1$ the product is empty and equals $1$ .

step 1.1L3

3.1

The cases in step 2.1 are exactly those of [F1], proving $μ_{∣} (1, n) = μ (n)$ .

step 2.1F1

3.2

For $d ∣ n$ , [L1] identifies $[d, n]$ with the divisor interval $[1, n / d]$ and hence with the same exponent-chain product; transporting through these isomorphisms by [L4] and repeating steps 1.1 and 2.1 gives $μ_{∣} (d, n) = μ (n / d)$ .

step 1.1step 2.1L1L2L3L4

4.1

Steps 3.1 and 3.2 prove the stated agreement and its interval form.

step 3.1step 3.2∎

Depends on

Used by

Dependency tree · two levels

28 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

R. Stanley, Enumerative Combinatorics, Volume 1, §§3.8.4–3.8.5 (standard reference, not scraped)

The number-theoretic Möbius function is the poset Möbius function of divisibility: μ(n)=μ∣(1,n)μ(n)=μ∣​(1,n)