Diamond sealing a maximal antichain in L

Since $\delta$ is countable, the family of earlier countable levels is a countable family. F4 and A1 make $T_{<\delta }$ countable. It is nonempty by its root, so the empty antichain is not maximal: the root could be adjoined. F2 applies to the given normal tree and nonempty maximal antichain $A$, yielding countably many distinct covering branches and a top $t_b$ for each. Its predecessor set is exactly $b$, and some $a_b\in A$ belongs to $b$, hence $a_b{<}_T{t}_b$. No family of chosen $a_b$ is needed for this existential assertion.

For the concrete instance, height $n$ consists of the $2^n$ binary strings of length $n$. The code $s\mapsto 2^{\mathrm{\mid }s\mathrm{\mid }}+{\sum }_{i<\mathrm{\mid }s\mathrm{\mid }}s(i)2^i$ injects all finite strings into the positive integers, so the partial tree is countable without Choice. Its root is the empty string, every string extends to every larger finite height by appending zeros, and every string has its two immediate successors. The two strings in $A$ are incomparable; every nonempty string extends exactly one of them and the root precedes both. Thus $A$ is maximal. There is no positive limit height below $\omega$ requiring a further predecessor-uniqueness check.

For every finite binary string $s$ put and view this infinite sequence as the branch of all its finite initial segments. It is cofinal, contains $s$, and meets $A$ in exactly its length-one initial segment. The distinct $b_s$ are precisely the eventually-zero binary sequences. They form a countable set by taking, for each sequence, the least numerical code of a string producing it; this is an injection into $\omega$. They form an infinite set because the sequences with a unique $1$ at position $n$ are distinct for distinct $n$. Adjoin a separate top for each distinct sequence. Its predecessors have order type $\omega$; distinct tops have distinct predecessor sets. Every old string lies below a top, and the countable new level preserves normality and all old splitting. This computes the branch family directly, including $s$ empty, which gives $0^{\omega }$.

In either construction, a node $u$ at a later height has a unique predecessor $t$ at height $\delta$ by F3. Since $t$ is one of the added tops, there is $a\in A$ with $a<t\le u$, so $a<u$. A node at height $\delta$ already has this property. If a global antichain $B$ restricts below $\delta$ to $A$ and contained such a $u$, it would contain the distinct comparable members $a,u$, which is impossible. Thus $B$ has no members at or above $\delta$. This is the failed-antichain-extension conclusion that sealing enforces.

The singleton root antichain is the degenerate maximal guess handled by the same argument: every cofinal branch contains the root. Heights zero and successor heights are excluded from this limit-stage operation. Choice entered only when obtaining countability of the unspecified family of earlier levels; the binary calculation and F2's least-index branch construction use no Choice. Inside $L$, F5 supplies the A1 hypothesis. The example assumes the particular correct stage guess, so it does not require an existence proof for a diamond sequence from $V=L$; F1 is the separate global theorem that combines such guesses with the stage construction. [F1, F2, F5, A1, step 1.1, step 3.1] QED.