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

Möbius inversion on a lower-finite poset, with the dual upper-finite form

Statement

Let $R$ be a commutative ring and interpret an integer $m$ in a coefficient as the repeated-addition element $m 1_{R}$ (Integer multiples in a ring: $(m + n) a = m a + n a$ , $m (a + b) = m a + m b$ , $(m a) b = m (a b) = a (m b)$ and $(m a) (n b) = (m n) (a b)$ for all $m, n \in Z$ and $a, b \in R$ ).

Lower-finite form. If $P$ is lower-finite and $f, g : P \to R$ , then the following are equivalent:

$g (y) = \sum_{x \leq y} f (x)$ for every $y \in P$ ;
$f (y) = \sum_{x \leq y} μ_{P} (x, y) g (x)$ for every $y \in P$ .

Upper-finite form. If $P$ is upper-finite and $f, g : P \to R$ , then the following are equivalent:

$g (x) = \sum_{x \leq y} f (y)$ for every $x \in P$ ;
$f (x) = \sum_{x \leq y} μ_{P} (x, y) g (y)$ for every $x \in P$ .

The two assertions have separate finiteness hypotheses. Local finiteness alone makes each interval recurrence finite but does not make either displayed global sum finite.

Facts & Assumptions

Given: A commutative ring $R$ , functions $f, g : P \to R$ , and either the lower-finite or the upper-finite hypotheses in the Statement.

[F1]

In a lower-finite poset each principal ideal is finite; in an upper-finite poset each principal filter is finite; either condition implies local finiteness (Intervals in a poset; locally finite, lower-finite and upper-finite posets).

[L1]

$\sum_{u \leq z \leq y} μ_{P} (z, y) = δ_{u, y}$ and $\sum_{u \leq z \leq y} μ_{P} (u, z) = δ_{u, y}$ (The Möbius recurrence: $μ_{P} (x, x) = 1$ and both interval sums of $μ_{P}$ vanish when $x < y$ ).

[L2]

Finite sums may be split, reindexed and interchanged by finite Fubini (Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule).

[L3]

Integer multiples distribute through ring sums and products (Integer multiples in a ring: $(m + n) a = m a + n a$ , $m (a + b) = m a + m b$ , $(m a) b = m (a b) = a (m b)$ and $(m a) (n b) = (m n) (a b)$ for all $m, n \in Z$ and $a, b \in R$ , Commutative ring).

Proof

technique · direct

1.1

Assume $P$ is lower-finite and $g (y) = \sum_{u \leq y} f (u)$ for every $y \in P$ . Fix $y \in P$ . Every index set below is contained in the finite principal ideal of $y$ by [F1]. Substitution and finite Fubini give $\sum_{x \leq y} μ_{P} (x, y) g (x) = \sum_{u \leq x \leq y} μ_{P} (x, y) f (u) = \sum_{u \leq y} f (u) (\sum_{u \leq x \leq y} μ_{P} (x, y)) = f (y)$ by [L1].

F1L1L2L3

1.2

Conversely, assume $f (x) = \sum_{u \leq x} μ_{P} (u, x) g (u)$ for every $x \in P$ , and fix $y \in P$ . Then $\sum_{x \leq y} f (x) = \sum_{u \leq x \leq y} μ_{P} (u, x) g (u) = \sum_{u \leq y} g (u) (\sum_{u \leq x \leq y} μ_{P} (u, x)) = g (y)$ by [L1].

F1L1L2L3

1.3

Now assume $P$ is upper-finite and $g (x) = \sum_{y \geq x} f (y)$ for every $x \in P$ . Fix $x \in P$ . Every index set lies in the finite principal filter of $x$ . Substitution and finite Fubini give $\sum_{y \geq x} μ_{P} (x, y) g (y) = \sum_{x \leq y \leq z} μ_{P} (x, y) f (z) = \sum_{z \geq x} f (z) (\sum_{x \leq y \leq z} μ_{P} (x, y)) = f (x)$ by [L1].

F1L1L2L3

1.4

Conversely, assume $f (y) = \sum_{z \geq y} μ_{P} (y, z) g (z)$ for every $y \in P$ , and fix $x \in P$ . Then $\sum_{y \geq x} f (y) = \sum_{x \leq y \leq z} μ_{P} (y, z) g (z) = \sum_{z \geq x} g (z) (\sum_{x \leq y \leq z} μ_{P} (y, z)) = g (x)$ by [L1].

F1L1L2L3

2.1

Steps 1.1 and 1.2 prove the lower-finite equivalence, while steps 1.3 and 1.4 separately prove its upper-finite order dual.

step 1.1step 1.2step 1.3step 1.4∎

Depends on

Used by

Both forms of Möbius inversion hold on every finite poset Corollary
Classical Möbius inversion over positive divisors Corollary

Dependency tree · two levels

31 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

F. Gotti, Incidence Algebras, MIT 18.211 notes (standard reference, not scraped)
R. Stanley, Enumerative Combinatorics, Volume 1, §§3.6–3.8 (standard reference, not scraped)