Finite Record Pinching Idempotence

Abstract

A finite complete orthogonal projection family defines an idempotent unread-record map.

Theorem 1.1 (Finite complete record pinching is idempotent).

$$\begin{gathered} \forall n,K,\mathrm{Finite}\left(n\right),\mathrm{Finite}\left(K\right), \\ P:K\to M_n(\mathbb{C}), \\ (\forall k\in K,P_k^{\ast }=P_k\wedge P_k{P}_k=P_k)\wedge \\ (\forall k,l\in K,k\ne l\Rightarrow P_k{P}_l=0)\wedge \\ \sum _{k\in K}{P}_k=I, \\ E:M_n(\mathbb{C})\to M_n(\mathbb{C}),E(\rho ):=\sum _{k\in K}{P}_k\rho P_k, \\ E\circ E=E. \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/Conditioning/FiniteRecordPinchingIdempotence.finite_record_pinching_idempotent (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let P be a finite family of complex matrix projections. Each P_k is self-adjoint and idempotent, distinct projections are pairwise orthogonal, and their sum is the identity.

The unread-record map sends rho to the sum of the diagonal compressions P_k rho P_k. Applying it twice introduces two projection indices; orthogonality removes every cross term and projection idempotence retains each diagonal term, so the two functions are equal.

The proof directly applies the frozen pointwise idempotence theorem and uses function extensionality only to expose the source claim as an equality of endomorphisms.

References

• Truth anchor: D5/S3/Observer/Conditioning/FiniteRecordPinchingIdempotence.finite_record_pinching_idempotent
• Dependency: D5/S3/Observer/Conditioning