Sharp and Effect Complement Fixed Points

Abstract

Projection complement is fixed-point-free, while effect complement fixes the half-identity.

Theorem 1.1 (Projection complement is sharp-fixed-point-free but fixes a general effect).

$$\begin{gathered} \forall H,0<{\dim }_{\mathbb{C}}(H)<\infty , \\ (\forall P:\mathrm{End}\left(H\right),\mathrm{Projection}\left(P\right)\Rightarrow [\mathrm{Projection}\left(I-P\right)\wedge I-P\ne P])\wedge \\ [\mathrm{Pos}\left(\frac{1}{2}I\right)\wedge \mathrm{Pos}\left(I-\frac{1}{2}I\right)\wedge I-\frac{1}{2}I=\frac{1}{2}I]\wedge \\ (\forall \tau :\mathrm{End}\left(H\right)\to \mathrm{End}\left(H\right),(\forall E,\mathrm{Pos}\left(E\right)\wedge \mathrm{Pos}\left(I-E\right)\Rightarrow \tau (E)\ne E)\Rightarrow \tau \ne (E\mapsto I-E)). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Sharpness/SharpEffectComplementBoundary.sharp_effect_complement_boundary (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let H be a nonzero finite-dimensional complex Hilbert space and let its continuous endomorphisms carry the adjoint operation. For every sharp projection P, I-P is again a sharp projection and differs from P.

Positivity is the library predicate requiring a symmetric, equivalently self-adjoint, operator with nonnegative quadratic form. Thus an effect E is stated directly by Pos(E) and Pos(I-E). Both conditions hold for I/2, and complement fixes I/2 exactly.

It follows that any codomain twist declared fixed-point-free on every effect must differ from ordinary complement. The proof uses Mathlib’s projection-complement closure theorem directly; projection non-fixedness then follows from idempotence and nontriviality of H.

References

• Truth anchor: D5/S3/Quantum/Sharpness/SharpEffectComplementBoundary.sharp_effect_complement_boundary