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.

On a finite chain, the Möbius function is $1$ on the diagonal, $-1$ on covers and $0$ on longer intervals

Statement

Let $C$ be a finite totally ordered poset, and let $x\le y$ in $C$ . Then

$\mu_C(x,y)=\begin{cases}1,&x=y,\\-1,&y\text{ covers }x,\\0,&\text{there is }z\text{ with }x<z<y.\end{cases}$

Facts & Assumptions

Given: A finite chain $C$ (Chain in a poset) and comparable elements $x\le y$ .

[L1]

$\mu(x,x)=1$ and $\mu(x,y)=-\sum_{x\le z<y}\mu(x,z)$ for $x<y$ (The Möbius recurrence: $\mu_P(x,x)=1$ and both interval sums of $\mu_P$ vanish when $x<y$ ).

[L2]

Strong induction on finite interval cardinality (Strong (complete) induction, The cardinality $\lvert A\rvert$ of a finite set).

[L3]

A proper subset of a finite set has smaller cardinality (A subset of a finite set is finite, with $\lvert B\rvert \le \lvert A\rvert$ , and equality holds if and only if $B = A$ ).

Proof

technique · induction

1.1

The diagonal value is $1$ by [L1].

baseL1

1.2

If $y$ covers $x$ , then the recurrence has only the term $z=x$ , so $\mu(x,y)=-\mu(x,x)=-1$ .

1.3

Fix an interval cardinality and assume the formula holds on every strictly smaller interval.

1.4

Suppose there is an element strictly between $x$ and $y$ . The finite nonempty chain $(x,y]$ has a least element $c$ : starting with any element, successively retain the smaller one while traversing a finite enumeration. Then $c$ covers $x$ and $c<y$ .

givenconstruct

2.1

For every $z$ with $c<z<y$ , the interval $[x,z]$ is a proper subset of $[x,y]$ and contains the intermediate element $c$ , so the inductive hypothesis and [L3] give $\mu(x,z)=0$ .

step 1.3step 1.4L3

3.1

The recurrence now gives $\mu(x,y)=-\sum_{x\le z<y}\mu(x,z)=-(\mu(x,x)+\mu(x,c))=-(1-1)=0$ .

step 1.1step 1.2step 2.1L1

4.1

The diagonal and cover cases are steps 1.1 and 1.2; step 3.1 proves the longer-interval case from all smaller intervals, so strong induction completes the formula.

step 1.1step 1.2step 1.3step 3.1L2discharge-induction∎

Depends on

Used by

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 52 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

R. Stanley, Enumerative Combinatorics, Volume 1, §§3.6–3.8 (standard reference, not scraped)

On a finite chain, the Möbius function is 111 on the diagonal, −1-1−1 on covers and 000 on longer intervals