Zero Norm Propagation for Matrix States

Abstract

A positive normalized matrix trace functional propagates a zero quadratic value to every mixed value.

Theorem 1.1 (The mixed trace is a Gram pairing after multiplication by the square root).

$$\forall d\in \mathrm{Type},[\mathrm{Fintype}\left(d\right)][\mathrm{DecidableEq}\left(d\right)]\forall rho\in \mathrm{Matrix}\left(d,d,\mathbb{C}\right),\forall h\in \mathrm{Matrix}\left(d,d,\mathbb{C}\right),\forall g\in \mathrm{Matrix}\left(d,d,\mathbb{C}\right),Matrix.PosSemidef\left(rho\right)\Rightarrow D5.S3.QuantumStates.GNSZeroPropagation.stateFunctional\left(rho,Matrix.conjTranspose\left(h\right)\cdot g\right)=Matrix.trace\left(Matrix.conjTranspose\left(h\cdot CFC.sqrt\left(rho\right)\right)\cdot g\cdot CFC.sqrt\left(rho\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/QuantumStates/GNSZeroPropagation.cross_trace_factorization (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a positive semidefinite matrix rho and arbitrary matrices h and g, the trace pairing of rho with the conjugate transpose of h times g equals the Gram trace of h times the positive square root of rho and g times that square root.

Theorem 1.2 (A zero quadratic value annihilates every mixed value).

$$\forall d,[\mathrm{Fintype}(d)],[\mathrm{DecidableEq}(d)],\forall \rho ,g\in \mathrm{Matrix}(d,d,,C),\mathrm{PosSemidef}(\rho )\wedge \mathrm{trace}(\rho )=1\wedge \mathrm{stateFunctional}(\rho ,g^{\ast }g)=0\Rightarrow \forall h\in \mathrm{Matrix}(d,d,,C),\mathrm{stateFunctional}(\rho ,h^{\ast }g)=0.$$

Proof. Machine-checked in Lean as D5/S3/QuantumStates/GNSZeroPropagation.gns_zero_norm_propagation (✓ std3). ∎

Source. Repository-derived.

Commentary.

The state functional is the source trace pairing Tr(rho times a), with rho positive semidefinite and trace one. Its quadratic value at g is the squared Frobenius norm of g times the positive square root of rho.

A zero quadratic value therefore makes g times the square root of rho equal to zero. The same factorization for an arbitrary h proves the mixed trace value Tr(rho h star g) is zero.

The matrix GNS identity is reused directly; the deposited statement retains positivity, normalization, and the universal mixed-value conclusion as public clauses.

References

• Truth anchor: D5/S3/QuantumStates/GNSZeroPropagation.cross_trace_factorization
• Truth anchor: D5/S3/QuantumStates/GNSZeroPropagation.gns_zero_norm_propagation
• Dependency: D5/S3/Quantum/GNSMatrix