Experimental relationship theorem (inference ⇔ continuous causal relationship)

Non-blind read-back — not independent testimony. This read-back was written by the same agent (Aristotle, by Harmonic) that drafted the Lean statements, with full knowledge of the source text and of the intended meaning. It was not produced by a blind, independent auditor, so it must not be mistaken for independent testimony; reviewers should compare the Lean code against the source themselves.

Setting (common to all statements of this mission). $\Omega$ is an arbitrary type (it may be empty), and a statement is a subset $s \subseteq \Omega$. $D$ is an arbitrary experimental domain on $\Omega$, i.e. a family $\mathcal D$ of subsets of $\Omega$ such that

• $\Omega \in \mathcal D$ and $\emptyset \in \mathcal D$;
• $s \cap t \in \mathcal D$ whenever $s, t \in \mathcal D$;
• $\bigcup_{n \in \mathbb N} f_n \in \mathcal D$ whenever $f_n \in \mathcal D$ for all $n \in \mathbb N$;
• there is a countable family $B_0 \subseteq \mathcal D$ such that every member of $\mathcal D$ belongs to $\langle B_0 \rangle$, the smallest family containing $B_0$, $\Omega$ and $\emptyset$ and closed under binary intersections and countable unions.

The theoretical domain $\bar{\mathcal D}$ is the smallest family of subsets of $\Omega$ that contains $\mathcal D$ and $\Omega$ and is closed under complement, binary intersection and countable union. A possibility is a set $x \in \bar{\mathcal D}$ with $x \neq \emptyset$ such that for every $t \in \bar{\mathcal D}$ either $x \subseteq t$ or $x \cap t = \emptyset$. $X$ is the type of possibilities (two possibilities are equal exactly when their underlying sets are equal). For $s \subseteq \Omega$ the verifiable set is $U(s) = \{x \in X : x \cap s \neq \emptyset\}$. The space $X$ carries the topology $\mathcal T$ generated by $\{U(s) : s \in \mathcal D\}$, i.e. the coarsest topology on $X$ in which every $U(s)$ with $s \in \mathcal D$ is open.

For two experimental domains $D_X, D_Y$ on the same $\Omega$ (families $\mathcal D_X,\mathcal D_Y$, possibility types $X, Y$, verifiable sets $U_X, U_Y$, natural topologies $\mathcal T_X,\mathcal T_Y$): "$D_Y$ depends on $D_X$" means there is a map $r:\mathcal D_Y\to\mathcal D_X$ with $r(s)=s$ for all $s\in\mathcal D_Y$ (equivalently $\mathcal D_Y\subseteq\mathcal D_X$); "$D_X$ and $D_Y$ are equivalent" means each depends on the other; a function $f: X\to Y$ is a causal relationship if $x\subseteq f(x)$ (as subsets of $\Omega$) for every $x\in X$. For a family $(D_i)_{i\in\iota}$ indexed by a countable type $\iota$, the combined domain has as statements the closure $\langle\bigcup_i\mathcal D_i\rangle$ of all statements of all $D_i$ (together with $\Omega$, $\emptyset$) under binary intersection and countable unions.

Statement. For every type $\Omega$ and all experimental domains $D_X,D_Y$ on $\Omega$: $D_Y$ depends on $D_X$ (there is $r:\mathcal D_Y\to\mathcal D_X$ with $r(s)=s$) if and only if there exists a function $f:X\to Y$ such that (a) $x\subseteq f(x)$ for every possibility $x$ of $D_X$ and (b) $f$ is continuous from $(X,\mathcal T_X)$ to $(Y,\mathcal T_Y)$.