Exact Conditioning Certificate

Abstract

The matrix defect of finite record conditioning vanishes exactly, without a tolerance term.

Theorem 1.1 (The conditioning certificate defect vanishes exactly).

$$\begin{gathered} \forall n,\kappa [\mathrm{Fintype}(n)][\mathrm{Fintype}(\kappa )], \\ \forall P:\kappa \to M_n(\mathbb{C}),\rho \in M_n(\mathbb{C}), \\ \mathrm{Record}(P)\wedge \mathrm{PosSemidef}(\rho )\Rightarrow \\ {d}_P(\rho )=0,d_P(\rho ):=U_P(\rho )-\sum _{k\in \kappa }{w}_k(\rho )\cdot {\rho }_k. \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Observer/ConditioningCertificate.certificate_identity_zero_tolerance (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let P be a finite complete family of pairwise orthogonal self-adjoint projections and let rho be positive semidefinite. Define the certificate defect as the unread matrix minus the record-weighted ensemble of the totalized conditional branches. Zero-weight branches cause no residual because their positive compressed blocks vanish. The established weighted-ensemble identity therefore makes the matrix-valued defect exactly zero; no norm, error bound, or approximation parameter is introduced.

References

• Truth anchor: D5/S3/Observer/ConditioningCertificate.certificate_identity_zero_tolerance
• Dependency: D5/S3/Observer/Conditioning