Incomplete Budget Physical Certificate

Abstract

A nonzero invisible Hermitian direction gives an explicit physical readout certificate.

Theorem 1.1 (An invisible direction yields two indistinguishable physical states).

$$\begin{gathered} \forall d:Nat,\mathrm{NeZero}(d), \\ A:\mathrm{Type}, \\ E:A\to \{F:\mathrm{HermitianSpace}(d)\mid \mathrm{PosSemidef}(\mathrm{matrix}(F))\wedge \mathrm{PosSemidef}(1-\mathrm{matrix}(F))\}, \\ D:\mathrm{HermitianSpace}(d), \\ \mathrm{let}V=\mathrm{span}(\mathbb{R},\mathrm{insert}(\mathrm{identityHermitian}(d),\{\mathrm{hermitian}(E(i)):i\in A\})),N=\mathrm{orthogonal}(V); \\ (D\in N\wedge D\ne 0)\Rightarrow \\ \exists epsilon:\mathbb{R},0<epsilon\wedge \\ \mathrm{let}rh{o}_{+}:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C})=\mathrm{inv}(\mathrm{complex}(d))\cdot \mathrm{identityMatrix}(d)+\mathrm{complex}(epsilon)\cdot \mathrm{matrix}(D), \\ rh{o}_{-}:\mathrm{Matrix}(\mathrm{Fin}(d),\mathrm{Fin}(d),\mathbb{C})=\mathrm{inv}(\mathrm{complex}(d))\cdot \mathrm{identityMatrix}(d)-\mathrm{complex}(epsilon)\cdot \mathrm{matrix}(D); \\ 0\le \mathrm{ofMatrix}(rh{o}_{+})\wedge \left(0\le \mathrm{ofMatrix}(rh{o}_{-})\wedge \left(\mathrm{Tr}(rh{o}_{+})=1\wedge \left(\mathrm{Tr}(rh{o}_{-})=1\wedge \left(rh{o}_{+}\ne rh{o}_{-}\wedge \left(\forall i\in A,\mathrm{Tr}(rh{o}_{+}\cdot \mathrm{matrix}(E(i)))=\mathrm{Tr}(rh{o}_{-}\cdot \mathrm{matrix}(E(i)))\right)\right)\right)\right)\right). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Measurement/IncompleteBudgetPhysicalCertificate.incomplete_budget_physical_certificate (✓ std3). ∎

Source. Repository-derived.

Commentary.

The visible space is constructed from the identity and the declared positive effects. The supplied nonzero Hermitian direction lies in its Hilbert–Schmidt orthogonal residual.

A norm-controlled positive epsilon perturbs the maximally mixed state in both directions. The public statement records positivity, both trace-one identities, distinction, and equality of every declared Born readout.

References

• Truth anchor: D5/S3/Quantum/Measurement/IncompleteBudgetPhysicalCertificate.incomplete_budget_physical_certificate
• Dependency: D5/S3/Quantum/Tomography/InformationalCompletenessEquivalence