TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck 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: $\mu(n)=\mu_{\mid}(1,n)$

Statement

For every positive integer $n$ ,

$\mu(n)=\mu_{\mid}(1,n),$

where the left side is The number-theoretic Möbius function $\mu(n)$ from prime factorisation and the right side is the poset Möbius function of positive-integer divisibility (The integer-valued Möbius function $\mu_P$ of a locally finite poset). More generally, if $d\mid n$ , then

$\mu_{\mid}(d,n)=\mu(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,\ldots,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: $\mu_P(x,x)=1$ and both interval sums of $\mu_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 $\mu(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,\ldots,e_i\}$ .

L1L2L4

2.1

If some $e_i\ge2$ , [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 $\mu_{\mid}(1,n)=\mu(n)$ .

step 2.1F1

3.2

For $d\mid 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 $\mu_{\mid}(d,n)=\mu(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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 89 results over 21 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click 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)\mu(n)=\mu_{\mid}(1,n)μ(n)=μ∣​(1,n)