Theorem 3.1: arbitrary unions of CWO sets are CWO

Non-blind read-back — not independent testimony. This read-back was written by the same agent that drafted these Lean statements, not by an independent auditor working blind from the code alone. The author knew the intended meaning while writing it, so it may read that intent into the code. Do not treat it as independent verification; compare the Lean code against the source directly.

For every type $C$, every cognitive-consequence space $S$ on $C$ (axioms as in the definition: countable $C$, inclusion, monotonicity, idempotence, finiteness, deduction property for $\Rightarrow$, and $\mathrm{Cn}(\varnothing) \ne \varnothing$), every index type $\iota$ (possibly empty) and every family $(A_i)_{i \in \iota}$ of subsets of $C$ such that $\mathrm{Cn}(C \setminus A_i) = C \setminus A_i$ for every $i$, the union $U = \bigcup_i A_i$ satisfies $\mathrm{Cn}(C \setminus U) = C \setminus U$. For empty $\iota$ this says $\mathrm{Cn}(C) = C$.