CorollaryStatement: AI-adaptedProof: 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.

Classical Möbius inversion over positive divisors

Statement

Let $R$ be a commutative ring and let $f,g:\mathbb Z_{>0}\to R$ . Then

$g(n)=\sum_{d\mid n}f(d)\quad\text{for every }n\ge1$

if and only if

$f(n)=\sum_{d\mid n}\mu(n/d)g(d)=\sum_{d\mid n}\mu(d)g(n/d)\quad\text{for every }n\ge1.$

All divisors in the sums are positive.

Facts & Assumptions

Given: A commutative ring $R$ and functions $f,g$ on the positive integers.

[L1]

Lower-finite poset inversion says $g(n)=\sum_{d\mid n}f(d)$ exactly when $f(n)=\sum_{d\mid n}\mu_{\mid}(d,n)g(d)$ (Möbius inversion on a lower-finite poset, with the dual upper-finite form).

[L2]

For $d\mid n$ , $\mu_{\mid}(d,n)=\mu(n/d)$ (The number-theoretic Möbius function is the poset Möbius function of divisibility: $\mu(n)=\mu_{\mid}(1,n)$ ).

[L3]

The divisibility poset of positive integers is lower-finite (The divisibility poset is lower-finite, and each divisor interval factorises as a product of finite chains of prime exponents).

[L4]

A finite sum is invariant under bijective reindexing (Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule).

Proof

technique · direct

1.1

Apply [L1] to the lower-finite divisibility poset from [L3] and substitute [L2]. This gives $f(n)=\sum_{d\mid n}\mu(n/d)g(d)$ .

L1L2L3

2.1

The map $d\mapsto n/d$ is a bijection of the positive divisors of $n$ with itself and is its own inverse. Reindexing the sum in step 1.1 by [L4] gives $f(n)=\sum_{d\mid n}\mu(d)g(n/d)$ .

step 1.1L4

3.1

Since [L1] is an equivalence, steps 1.1 and 2.1 prove both directions and both standard indexings.

step 1.1step 2.1L1∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 85 results over 18 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

P. J. Cameron, Notes on Number Theory, Theorem 7.9 (standard reference, not scraped)
Stanford Pairing-Based Cryptography notes, Möbius inversion (standard reference, not scraped)