PhyslibAlpha.AlgebraicFramework.CStarAlgebra.SharpEffect

Idempotent effects in a C⋆-algebra are sharp

A projection — an idempotent self-adjoint element `p` with `p * p = p` — is a sharp effect: it cannot be written as a nontrivial mixture of two *different* effects. This is the direction of `Effect.IsSharp` that matters for reading a projection-valued measure as a `PVM` (every projection it assigns is automatically sharp, `PVM.lean`); the converse (every sharp effect is a projection) needs a construction from the continuous functional calculus splitting a non-idempotent effect into a genuine mixture, and is not attempted here.

The proof: write `b := 1 - p`. If `p = t • y₁ + s • y₂` for effects `y₁, y₂` and `t, s > 0`, `t + s = 1`, then conjugating by `b` kills the whole sum (`b * p * b = 0` since `b * p = 0`), and since conjugation by a self-adjoint element preserves nonnegativity, both `b * y₁ * b` and `b * y₂ * b` — being nonnegative terms summing to `0` — vanish individually. The C⋆-identity `‖z⋆z‖ = ‖z‖²`, applied to `z := √y₁ * b`, turns `b * y₁ * b = 0` into `y₁ * b = b * y₁ = 0`, i.e. `y₁` commutes with `p` and is fixed by conjugating it: `p * y₁ * p = y₁`. Since `y₁ ≤ 1`, conjugating by `p` then gives `y₁ ≤ p`; the same argument gives `y₂ ≤ p`, and averaging `p - y₁ ≥ 0`, `p - y₂ ≥ 0` back against the original mixture forces both to be exactly `0`.

Main results

• `IsIdempotentElem.isSharp` : an idempotent effect (in a C⋆-algebra) is sharp.