Properties of orthogonality

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). $I:\mathbb R\times\mathbb R\to\mathbb R$ is an arbitrary function and $E$ an arbitrary topological space. $X$ is an ensemble space with bound $I$ on $E$, consisting of:

• the topology of $E$ is $T_0$ and second countable;
• a mixing map $(p,a,b)\mapsto pa+\bar pb$ for $p\in[0,1]$ ($\bar p=1-p$), jointly continuous on $[0,1]\times E\times E$, with $1a+0b=a$, $pa+\bar pa=a$, $pa+\bar pb=\bar pb+pa$, and the associativity identity $p_1e_1+\bar p_1\big(\tfrac{1-p_1-p_3}{\bar p_1}e_2+\tfrac{p_3}{\bar p_1}e_3\big)=\bar p_3\big(\tfrac{p_1}{\bar p_3}e_1+\tfrac{1-p_1-p_3}{\bar p_3}e_2\big)+p_3e_3$ for $p_1,p_3\in[0,1)$, $p_1+p_3\le1$;
• a continuous entropy $S:E\to\mathbb R$ such that for all $p\in(0,1)$: $S(pa+\bar pb)\ge pS(a)+\bar pS(b)$, with equality iff $a=b$; for all $p\in[0,1]$: $S(pa+\bar pb)\le I(p,\bar p)+pS(a)+\bar pS(b)$;
• writing $a\perp b$ for "$S(qa+\bar qb)=I(q,\bar q)+qS(a)+\bar qS(b)$ for every $q\in(0,1)$": for all $p\in(0,1)$ and $a,b,c$, ($a\perp b$ and $a\perp c$) iff $a\perp(pb+\bar pc)$.

Component: $c$ is a component of $a$ if $a=pc+\bar pd$ for some $d\in E$ and some $p\in(0,1]$. Separate: no common component. Mixing entropy: $MS(a,b)=S(\tfrac12a+\tfrac12b)-\tfrac12S(a)-\tfrac12S(b)$.

Statement. For every $I$, every topological space $E$ and every ensemble space $X$ with bound $I$ on $E$, assuming $I(p,1-p)>0$ for every real $p\in(0,1)$, all of the following hold: (1) no $a\in E$ satisfies $a\perp a$; (2) for all $a,b$: $a\perp b$ iff $b\perp a$; (3) for all $a,b$: if $b$ is a component of $a$ then not $a\perp b$; (4) for all $a,b$: if $a\perp b$ then $a$ and $b$ have no common component.