Theorem 5.1: no convergence into a Gödel incompleteness black hole

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 similarity distance $D$ on $C$, every $A \subseteq C$, every sequence $s : \mathbb N \to C$ and every $x \in C$: if there are $\varepsilon \in (0,1)$ and $k \in \mathbb N$ such that $\mathrm{Cog}(x, s_n) \ge \varepsilon$ for all $n \ge k$ and $\{y : \mathrm{Cog}(x,y) < \varepsilon\} \subseteq A$, then it is not the case that for every $\varepsilon' \in (0,1)$ there is $m$ with $\mathrm{Cog}(x, s_n) < \varepsilon'$ for all $n \ge m$. The set $A$ plays no role in the conclusion.