PhyslibAlpha.AlgebraicFramework.OrderUnit.State.NormalEquivalence

Normality under the state/weight equivalence

A normal state yields a normal finite normalized weight through the canonical map `UnitalPositiveLinearMap.toWeight`. The two predicates have intentionally different domains: state normality is about directed suprema in the whole ordered space, whereas a weight is only defined on the positive cone. The theorem below transports suprema across that inclusion rather than defining a duplicate normal-state predicate.

The converse is deliberately not asserted at this generality. An arbitrary directed set with a supremum need not have one common lower bound, so it cannot in general be shifted wholesale into the positive cone. A reverse theorem requires either a bounded-below version of state normality or a strengthened weight predicate that controls those translated directed families.

1 declaration

theorem

A Normal State Induces a Normal Weight

#toWeight_isNormal

Let $E$ be an ordered real vector space and let $s: E \to \mathbb{R}$ be a state (a unital positive linear map). If $s$ is normal—meaning it preserves the suprema of non-empty directed sets in $E$ —then the induced weight $\omega: \text{PosCone}(E) \to [0, \infty]$ (defined by $\omega(x) = s(x)$ for all $x$ in the positive cone) is also normal.