PhyslibAlpha.AlgebraicFramework.JordanOrderUnit.JB.GeneratedByOne.Effect

Let $E$ be a nontrivial normed Jordan algebra with a JB-order unit. For an element $a \in E$ and a continuous real-valued function $f \in C(\sigma(a), \mathbb{R})$ defined on the Jordan spectrum $\sigma(a)$, if $f$ satisfies $0 \le f(x) \le 1$ for all $x \in \sigma(a)$, then the element $f(a)$ obtained via the Jordan continuous functional calculus is an **effect** (an element $e \in E$ such that $0 \le e \le 1$).

Let $E$ be a nontrivial normed Jordan algebra with a JB-order unit. For any element $a \in E$ and any continuous real-valued function $f \in C(\sigma(a), \mathbb{R})$ on the Jordan spectrum $\sigma(a)$ such that $0 \le f(x) \le 1$ for all $x \in \sigma(a)$, the element $f(a)$ constructed as an effect (i.e., an element proven to satisfy $0 \le f(a) \le 1$) is equal to the element $f(a)$ obtained via the standard Jordan continuous functional calculus when coerced to the algebra $E$.