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

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\cdots\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\cdots\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\cdots\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 · next 3 levels

Direct dependencies and their dependencies through the next three levels: 18 results over 11 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

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