Alphabeta Math
LemmaStatement: 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 Möbius recurrence: μP(x,x)=1 and both interval sums of μP vanish when x<y

Statement

For a locally finite poset P and x≤y,

μP(x,x)=1,

and, when x<y,

∑x≤z≤yμP(x,z)=0,∑x≤z≤yμP(z,y)=0.

Equivalently, off the diagonal,

μP(x,y)=−∑x≤z<yμP(x,z)=−∑x<z≤yμP(z,y).

Either recurrence together with the diagonal values uniquely determines μP interval by interval.

Facts & Assumptions

Given: A locally finite poset P and comparable elements x≤y.

[F1]

μP∗ζ=δ=ζ∗μP (The integer-valued Möbius function μP of a locally finite poset).

Proof

technique · direct
1.1F1F2

Evaluating either inverse equation at (x,x) gives μP(x,x)=1.

1.2F1F2

Evaluating μP∗ζ=δ at x<y gives ∑x≤z≤yμP(x,z)=0.

1.3F1F2

Evaluating ζ∗μP=δ at x<y gives ∑x≤z≤yμP(z,y)=0.

2.1step 1.2step 1.3algebra

Isolating the term z=y in step 1.2 and the term z=x in step 1.3 yields the two displayed recursive formulas.

3.1step 1.1step 2.1

Each right-hand side uses only proper subintervals, so induction on the finite cardinality of [x,y] shows that either recurrence and the diagonal clause determine at most one function.

4.1step 1.1step 1.2step 1.3step 2.1step 3.1∎

Steps 1.1 through 3.1 prove both sums, both recurrences and uniqueness.

Depends on

Used by

Dependency tree · two levels

16 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