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.

Every finite Boolean lattice has a symmetric chain decomposition

Statement

For every finite set $A$ , the Boolean lattice $B (A)$ can be partitioned into saturated chains whose least and greatest ranks sum to $∣ A ∣$ .

Facts & Assumptions

Given: A finite set $A$ .

[L1]

A symmetric chain decomposition of $B (X)$ lifts to one of $B (X \cup {x})$ whenever $x \notin X$ (A symmetric chain decomposition of one Boolean lattice lifts to the next Boolean lattice).

[L2]

The principle of induction on $N$ (The principle of mathematical induction).

Proof

technique · induction

1.1

For $∣ A ∣ = 0$ , the Boolean lattice consists only of $\emptyset$ ; the one-term chain has endpoint ranks $0$ and $0$ , so it is symmetric.

base

1.2

Assume every Boolean lattice on an $n$ -element set has a symmetric chain decomposition, and let $A$ have $n + 1$ elements. Choose $x \in A$ and put $X = A ∖ {x}$ , so $∣ X ∣ = n$ .

ihL2choose

2.1

The induction hypothesis gives a symmetric chain decomposition of $B (X)$ , and [L1] lifts it to a symmetric chain decomposition of $B (X \cup {x}) = B (A)$ .

step 1.2L1

3.1

The base case and induction step prove the assertion for every finite cardinality, hence for every finite set $A$ .

step 1.1step 2.1discharge-induction∎

Depends on

Used by

Dependency tree · two levels

6 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

Symmetric chain decomposition background, Electronic Journal of Combinatorics (standard reference, not scraped)