LemmaStatement: 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.

A symmetric chain decomposition of one Boolean lattice lifts to the next Boolean lattice

Statement

A saturated chain in $B (A)$ is symmetric if its least and greatest ranks sum to $∣ A ∣$ . If $B (A)$ has a partition into symmetric saturated chains and $x \notin A$ , then $B (A \cup {x})$ also has such a partition.

Facts & Assumptions

Given: A finite set $A$ with $∣ A ∣ = n$ , an element $x \notin A$ , and a symmetric chain decomposition of $B (A)$ .

[F1]

The rank of a subset in $B (A)$ is its cardinality, and adjoining $x$ raises rank by one (The Boolean lattice of subsets of a finite set and its rank levels).

Proof

technique · constructive

1.1

Take one chain $C : S_{r} \subset S_{r + 1} \subset \dots \subset S_{n - r}$ of the given decomposition, where the subscripts are ranks and $r + (n - r) = n$ .

givenF1

2.1

Construct the chain $C_{0} : S_{r} \subset S_{r + 1} \subset \dots \subset S_{n - r} \subset S_{n - r} \cup {x}$ in $B (A \cup {x})$ . Its endpoint ranks are $r$ and $n - r + 1$ , whose sum is $n + 1$ .

step 1.1F1construct

2.2

If $r < n - r$ , also construct $C_{1} : S_{r} \cup {x} \subset S_{r + 1} \cup {x} \subset \dots \subset S_{n - r - 1} \cup {x}$ . Its endpoint ranks are $r + 1$ and $n - r$ , whose sum is $n + 1$ ; when $r = n - r$ , this second chain is empty and is omitted.

step 1.1F1construct

3.1

The chains $C_{0}$ and $C_{1}$ partition the two copies ${T : T \in C}$ and ${T \cup {x} : T \in C}$ : the top set with $x$ goes to $C_{0}$ , and every other set with $x$ goes to $C_{1}$ .

step 2.1step 2.2

4.1

Applying this construction independently to every chain of the original partition covers each subset of $A \cup {x}$ exactly once and produces only symmetric chains. Hence it is a symmetric chain decomposition of $B (A \cup {x})$ .

step 3.1F1discharge-construct∎

Depends on

The Boolean lattice of subsets of a finite set and its rank levels

Used by

Every finite Boolean lattice has a symmetric chain decomposition Theorem

Dependency tree · two levels

4 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)