Streams never earn identity while apartness is earned by a finite witness and persists; the diagonal earns strict non-membership; one marked pair collapses the injectivity certificate; a nondegenerate mark does not equal itself; atom verdicts are the modal thresholds.

With the constants \(\top /\bot \) in the certified language, the lazy lfp of the nine-fact membership system computes to \([F,F,T,F,T,F,F,F,Z]\): eight facts grounded, quarantine exactly at \(R\in R\) — containment instead of explosion, by the kernel.

On mark-free lists a verified element certifies its membership and \(S \subseteq S\), \(S = S\) hold — the inheritance boundary is drawn at the mark, kernel-checked from both sides.