Selective Record Conditioning

Abstract

A nonzero record branch determines its normalized selective system state.

Theorem 1.1 (A nonzero record branch forces the selective state).

$$\begin{gathered} \forall n,K:\mathrm{Type},[\mathrm{Fintype}(n)], \\ P:K\to M_n(\mathbb{C}),\rho ,{\rho }_k:M_n(\mathbb{C}), \\ k\in K,\mathrm{Tr}\left(\rho P_k\right)\ne 0, \\ \mathrm{Tr}\left(\rho P_k\right){\rho }_k=P_k\rho P_k\Rightarrow \\ {\rho }_k=\frac{P_k\rho P_k}{\mathrm{Tr}\left(\rho P_k\right)}. \end{gathered}$$

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

Source. Repository-derived.

Commentary.

Let rho be a finite complex matrix and let P_k be the matrix selected by a record value k. The supplied branch law says that multiplying the conditioned state rho_k by its Born weight recovers the unnormalized compression P_k rho P_k.

When the Born weight is nonzero, scalar cancellation uniquely determines rho_k. The proof uses the field inverse law and scalar associativity; the conditioned state is not defined to be the displayed target.

References

• Truth anchor: D5/S3/Observer/Conditioning/SelectiveRecordConditioning.selective_record_conditioning
• Dependency: D5/S3/Observer/Conditioning