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.

For $A\subseteq B$ in a finite Boolean lattice, $\mu(A,B)=(-1)^{\lvert B\setminus A\rvert}$

Statement

Let $X$ be finite and order its Boolean lattice $B(X)=\mathcal P(X)$ by inclusion (The Boolean lattice of subsets of a finite set and its rank levels). For $A\subseteq B\subseteq X$ ,

$\mu_{B(X)}(A,B)=(-1)^{|B\setminus A|}.$

Facts & Assumptions

Given: A finite set $X$ and subsets $A\subseteq B\subseteq X$ .

[F1]

The interval $[A,B]$ consists of the sets $A\cup E$ with $E\subseteq B\setminus A$ , and $|(A\cup E)\setminus A|=|E|$ (The Boolean lattice of subsets of a finite set and its rank levels, The cardinality $\lvert A\rvert$ of a finite set).

[F2]

Natural powers of $-1$ are defined in the multiplicative monoid of $\mathbb Z$ , and $\mathbb Z$ is a commutative ring (Powers $g^{n}$ : natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$ , The integers form a commutative ring).

[L1]

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

[L2]

The Möbius function is the unique function with diagonal value $1$ and vanishing interval sums off the diagonal (The Möbius recurrence: $\mu_P(x,x)=1$ and both interval sums of $\mu_P$ vanish when $x<y$ ).

[L3]

The alternating binomial row sum vanishes in positive degree ( $\sum_{k<n+1}\binom{n}{k} = 2^{n}$ , and $\sum_{k<n+1}(-1)^{k}\iota\!\binom{n}{k} = 0$ for $n \ge 1$ , Integer powers $a^m$ ).

[L4]

Möbius functions multiply on product posets (The Möbius function of a product poset is the product of the Möbius functions).

Proof

technique · direct

1.1

Define $\nu(A,B):=(-1)^{|B\setminus A|}$ in $\mathbb Z$ . On the diagonal, $B\setminus A=\varnothing$ , so $\nu(A,A)=(-1)^0=1$ .

F1F2

1.2

Suppose $A<B$ and choose $b\in B\setminus A$ . The subsets $E\subseteq B\setminus A$ split into disjoint pairs $E$ and $E\cup\{b\}$ with $b\notin E$ ; their contributions satisfy $(-1)^{|E|}+(-1)^{|E|+1}=0$ in $\mathbb Z$ . Finite splitting and reindexing therefore give $\sum_{A\subseteq C\subseteq B}\nu(A,C)=\sum_{E\subseteq B\setminus A}(-1)^{|E|}=0$ .

F1F2L1choose

2.1

Thus $\nu$ satisfies the diagonal and vanishing-sum recurrence, so uniqueness gives $\nu=\mu_{B(X)}$ .

step 1.1step 1.2L2

2.2

Equivalently, grouping the sum in step 1.2 by $|E|$ gives the alternating binomial sum in [L3]. Identifying the interval with a finite product of two-element chains gives the same formula by [L4], since the defining recurrence and its uniqueness in [L2] transport through a poset isomorphism.

step 1.2L2L3L4

3.1

Step 2.1 is the asserted formula, with step 2.2 recording its binomial and product-poset readings.

step 2.1step 2.2∎

Depends on

Used by

Dependency tree · next 3 levels

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

For A⊆BA\subseteq BA⊆B in a finite Boolean lattice, μ(A,B)=(−1)∣B∖A∣\mu(A,B)=(-1)^{\lvert B\setminus A\rvert}μ(A,B)=(−1)∣B∖A∣