Orthogonal Additivity

Abstract

A normal positive state is additive on a complete orthogonal projection family.

Theorem 1.1 (Normal-state additivity and pure-state Parseval decomposition).

$$\begin{array}{c}\forall A:\mathrm{Type},H:\mathrm{Type},\\ [\mathrm{CStarAlgebra}(A)],[\mathrm{PartialOrder}(A)],[\mathrm{StarOrderedRing}(A)],\\ [\mathrm{NormedAddCommGroup}(H)],[\mathrm{InnerProductSpace}(\mathbb{C},H)],[\mathrm{CompleteSpace}(H)],\\ P:Nat\to A,\\ pi:\mathrm{StarAlgHom}(\mathbb{C},A,\mathrm{ContinuousLinearEnd}(\mathbb{C},H)),omega:\mathrm{PositiveLinearMap}(\mathbb{C},A,\mathbb{C}),\\ [\forall i,\mathrm{IsStarProjection}(P_i)],\\ [\forall i,j,i\ne j\Rightarrow P_i\times P_j=0],\\ [\forall psi,\sum _{i}pi(P_i)(psi)=psi],\\ [omega(1)=1],\\ [\mathrm{SequentiallyNormal}(pi,omega)]\Rightarrow [\sum _{i}omega(P_i)=1\wedge \forall psi,\sum _i{\Vert pi(P_i)(psi)\Vert }^2={\Vert psi\Vert }^2].\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurements/OrthogonalAdditivity.orthogonal_additivity (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let A be a unital complex C-star algebra represented on a complete complex inner-product space H. The family is a countable sequence of star projections in A, pairwise orthogonal, whose represented strong operator sum is the identity in pointwise form.

The state is a positive linear functional normalized at the identity. Sequential normality is stated publicly as continuity along every monotone sequence with a strong pointwise limit.

The theorem concludes both source clauses: the real state weights have sum one, and every vector has the pure-state Parseval sum of squared projection norms. A finite family is represented by zero extension of its sequence, while the displayed theorem handles the countable case directly.

Pinned Mathlib supplies positivity of star projections, monotone operator partial sums, HasSum transport through continuous linear maps, and the inner-product norm identity. Repository and pinned-library searches found no theorem packaging the normal-state and Parseval clauses together.

References

• Truth anchor: D5/S3/Quantum/Measurements/OrthogonalAdditivity.orthogonal_additivity