Theorem 3.8: two cognitive limits of one sequence coincide

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$ and every cognitive similarity distance $D$ on $C$ (a function $\mathrm{Cog} : C \times C \to \mathbb R$ with values in $[0,1]$ and a relation $\approx$ with $\mathrm{Cog}(x,y)=0 \iff x \approx y$, symmetry, $x \approx z \Rightarrow \mathrm{Cog}(x,y) = \mathrm{Cog}(z,y)$, and the triangle inequality), every sequence $s : \mathbb N \to C$ and all $x_1, x_2 \in C$: if for every $\varepsilon \in (0,1)$ there is $m$ with $\mathrm{Cog}(x_1, s_n) < \varepsilon$ for all $n \ge m$, and likewise for $x_2$, then $x_1 \approx x_2$.