Alphabeta Math
TheoremStatement: 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.

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

Statement

Let RR be a commutative ring and interpret an integer mm in a coefficient as the repeated-addition element m1Rm1_R (Integer multiples in a ring: (m+n)a=ma+na(m + n)a = ma + na, m(a+b)=ma+mbm(a + b) = ma + mb, (ma)b=m(ab)=a(mb)(ma)b = m(ab) = a(mb) and (ma)(nb)=(mn)(ab)(ma)(nb) = (mn)(ab) for all m,n∈Zm, n \in \mathbb{Z} and a,b∈Ra, b \in R).

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

  1. g(y)=∑x≤yf(x)g(y)=\sum_{x\le y}f(x) for every y∈Py\in P;
  2. f(y)=∑x≤yμP(x,y)g(x)f(y)=\sum_{x\le y}\mu_P(x,y)g(x) for every y∈Py\in P.

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

  1. g(x)=∑x≤yf(y)g(x)=\sum_{x\le y}f(y) for every x∈Px\in P;
  2. f(x)=∑x≤yμP(x,y)g(y)f(x)=\sum_{x\le y}\mu_P(x,y)g(y) for every x∈Px\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 RR, functions f,g:P→Rf,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]

∑u≤z≤yμP(z,y)=δu,y\sum_{u\le z\le y}\mu_P(z,y)=\delta_{u,y} and ∑u≤z≤yμP(u,z)=δu,y\sum_{u\le z\le y}\mu_P(u,z)=\delta_{u,y} (The Möbius recurrence: μP(x,x)=1\mu_P(x,x)=1 and both interval sums of μP\mu_P vanish when x<yx<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=ma+na(m + n)a = ma + na, m(a+b)=ma+mbm(a + b) = ma + mb, (ma)b=m(ab)=a(mb)(ma)b = m(ab) = a(mb) and (ma)(nb)=(mn)(ab)(ma)(nb) = (mn)(ab) for all m,n∈Zm, n \in \mathbb{Z} and a,b∈Ra, b \in R, Commutative ring).

Proof

technique · direct
1.1

Assume PP is lower-finite and g(y)=∑u≤yf(u)g(y)=\sum_{u\le y}f(u) for every y∈Py\in P. Fix y∈Py\in P. Every index set below is contained in the finite principal ideal of yy by [F1]. Substitution and finite Fubini give ∑x≤yμP(x,y)g(x)=∑u≤x≤yμP(x,y)f(u)=∑u≤yf(u)(∑u≤x≤yμP(x,y))=f(y)\sum_{x\le y}\mu_P(x,y)g(x)=\sum_{u\le x\le y}\mu_P(x,y)f(u)=\sum_{u\le y}f(u)\left(\sum_{u\le x\le y}\mu_P(x,y)\right)=f(y) by [L1].

F1L1L2L3
1.2

Conversely, assume f(x)=∑u≤xμP(u,x)g(u)f(x)=\sum_{u\le x}\mu_P(u,x)g(u) for every x∈Px\in P, and fix y∈Py\in P. Then ∑x≤yf(x)=∑u≤x≤yμP(u,x)g(u)=∑u≤yg(u)(∑u≤x≤yμP(u,x))=g(y)\sum_{x\le y}f(x)=\sum_{u\le x\le y}\mu_P(u,x)g(u)=\sum_{u\le y}g(u)\left(\sum_{u\le x\le y}\mu_P(u,x)\right)=g(y) by [L1].

F1L1L2L3
1.3

Now assume PP is upper-finite and g(x)=∑y≥xf(y)g(x)=\sum_{y\ge x}f(y) for every x∈Px\in P. Fix x∈Px\in P. Every index set lies in the finite principal filter of xx. Substitution and finite Fubini give ∑y≥xμP(x,y)g(y)=∑x≤y≤zμP(x,y)f(z)=∑z≥xf(z)(∑x≤y≤zμP(x,y))=f(x)\sum_{y\ge x}\mu_P(x,y)g(y)=\sum_{x\le y\le z}\mu_P(x,y)f(z)=\sum_{z\ge x}f(z)\left(\sum_{x\le y\le z}\mu_P(x,y)\right)=f(x) by [L1].

F1L1L2L3
1.4

Conversely, assume f(y)=∑z≥yμP(y,z)g(z)f(y)=\sum_{z\ge y}\mu_P(y,z)g(z) for every y∈Py\in P, and fix x∈Px\in P. Then ∑y≥xf(y)=∑x≤y≤zμP(y,z)g(z)=∑z≥xg(z)(∑x≤y≤zμP(y,z))=g(x)\sum_{y\ge x}f(y)=\sum_{x\le y\le z}\mu_P(y,z)g(z)=\sum_{z\ge x}g(z)\left(\sum_{x\le y\le z}\mu_P(y,z)\right)=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

Dependency tree · next 3 levels

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