Finite Record Recovery Error

Abstract

Every CPTP recovery has the finite-record worst-case trace-distance lower bound.

Theorem 1.1 (Signed coefficient conjugation).

$$\forall c\in \mathbb{Z}\to \mathbb{C},ell\in \mathbb{Z},\sum _{k\in \mathbb{Z}}c\left(k-ell\right)\cdot \mathrm{conj}\left(c\left(k\right)\right)=\mathrm{conj}\left(\sum _{k\in \mathbb{Z}}c\left(k+ell\right)\cdot \mathrm{conj}\left(c\left(k\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Decoherence/FiniteRecordRecoveryError.coefficient_gamma_neg (✓ std3). ∎

Source. Repository-derived.

Commentary.

Reindex the integer sum by translation and commute the scalar factors after conjugation.

Theorem 1.2 (The exact complex two-coordinate square root).

$$\forall n\in FiniteType,i\in n,j\in n,z\in \mathbb{C},i\ne j\Rightarrow \mathrm{sqrt}\left({\left(\mathrm{single}\left(i,j,z\right)+\mathrm{single}\left(j,i,\mathrm{conj}\left(z\right)\right)\right)}^{\ast }\cdot \left(\mathrm{single}\left(i,j,z\right)+\mathrm{single}\left(j,i,\mathrm{conj}\left(z\right)\right)\right)\right)=\mathrm{single}\left(i,i,\mathrm{norm}\left(z\right)\right)+\mathrm{single}\left(j,j,\mathrm{norm}\left(z\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Decoherence/FiniteRecordRecoveryError.pair_matrix_sqrt (✓ std3). ∎

Source. Repository-derived.

Commentary.

The two diagonal norm entries form a positive semidefinite matrix whose square is the Gram matrix; uniqueness identifies the positive square root.

Theorem 1.3 (The exact complex two-coordinate trace norm).

$$\forall n\in FiniteType,i\in n,j\in n,z\in \mathbb{C},i\ne j\Rightarrow \mathrm{traceNorm}\left(\mathrm{single}\left(i,j,z\right)+\mathrm{single}\left(j,i,\mathrm{conj}\left(z\right)\right)\right)=2\cdot \mathrm{norm}\left(z\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Decoherence/FiniteRecordRecoveryError.pair_matrix_traceNorm (✓ std3). ∎

Source. Repository-derived.

Commentary.

Take the real trace of the explicit two-coordinate square root.

Theorem 1.4 (Actual plus and minus density states).

$$\forall n\in FiniteType,N\in Nat,c\in \mathbb{Z}\to \mathbb{C},q\in n\to \mathbb{Z},i\in n,j\in n,\left(\left(\left(\forall k\in \mathbb{Z},\left(k<0\vee N<k\right)\Rightarrow c\left(k\right)=0\right)\wedge \sum _{k\in \mathbb{Z}}\mathrm{norm}{\left(c\left(k\right)\right)}^2=1\right)\wedge i\ne j\right)\Rightarrow \mathrm{let}\forall ell\in \mathbb{Z},\gamma \left(ell\right)=\sum _{k\in \mathbb{Z}}c\left(k+ell\right)\cdot \mathrm{conj}\left(c\left(k\right)\right);\mathrm{let}\forall k\in n,vp\left(k\right)=\frac{\mathrm{ite}\left(k=i,1,0\right)+\mathrm{ite}\left(k=j,1,0\right)}{\mathrm{sqrt}\left(2\right)};\mathrm{let}\forall k\in n,vm\left(k\right)=\frac{\mathrm{ite}\left(k=i,1,0\right)-\mathrm{ite}\left(k=j,1,0\right)}{\mathrm{sqrt}\left(2\right)};\exists C\in \mathrm{QuantumChannel}\left(n,n\right),\left(\forall A\in \mathrm{Matrix}\left(n,n,\mathbb{C}\right),k\in n,l\in n,\mathrm{entry}\left(\mathrm{act}\left(C,A\right),k,l\right)=\gamma \left(q\left(k\right)-q\left(l\right)\right)\cdot \mathrm{entry}\left(A,k,l\right)\right)\wedge \left(\exists rho\in \mathrm{DensityState}\left(n\right),sigma\in \mathrm{DensityState}\left(n\right),\left(\left(\mathrm{raw}\left(rho\right)=\mathrm{vecMulVec}\left(vp,\mathrm{conj}\left(vp\right)\right)\wedge \mathrm{raw}\left(sigma\right)=\mathrm{vecMulVec}\left(vm,\mathrm{conj}\left(vm\right)\right)\right)\wedge \mathrm{traceDistance}\left(rho,sigma\right)=1\right)\wedge \mathrm{traceDistance}\left(\mathrm{mapState}\left(C,rho\right),\mathrm{mapState}\left(C,sigma\right)\right)=\mathrm{norm}\left(\gamma \left(q\left(i\right)-q\left(j\right)\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Decoherence/FiniteRecordRecoveryError.finite_record_pair_witnesses (✓ std3). ∎

Source. Repository-derived.

Commentary.

Finite support converts the integer normalization to the frozen channel theorem’s finite sum. The displayed projectors have trace one, and the exact pair norm computes both distances.

Theorem 1.5 (Uniform recovery lower bound).

$$\forall n\in FiniteType,N\in Nat,c\in \mathbb{Z}\to \mathbb{C},q\in n\to \mathbb{Z},i\in n,j\in n,\left(\left(\left(\forall k\in \mathbb{Z},\left(k<0\vee N<k\right)\Rightarrow c\left(k\right)=0\right)\wedge \sum _{k\in \mathbb{Z}}\mathrm{norm}{\left(c\left(k\right)\right)}^2=1\right)\wedge q\left(i\right)-q\left(j\right)\ne 0\right)\Rightarrow \left(\forall R\in \mathrm{QuantumChannel}\left(n,n\right),\mathrm{let}\forall ell\in \mathbb{Z},\gamma \left(ell\right)=\sum _{k\in \mathbb{Z}}c\left(k+ell\right)\cdot \mathrm{conj}\left(c\left(k\right)\right);\mathrm{let}\forall A\in \mathrm{Matrix}\left(n,n,\mathbb{C}\right),k\in n,l\in n,\mathrm{entry}\left(\Lambda \left(A\right),k,l\right)=\gamma \left(q\left(k\right)-q\left(l\right)\right)\cdot \mathrm{entry}\left(A,k,l\right);\mathrm{let}\forall rho\in \mathrm{DensityState}\left(n\right),error\left(rho\right)=\frac{\mathrm{traceNorm}\left(\mathrm{act}\left(R,\Lambda \left(\mathrm{raw}\left(rho\right)\right)\right)-\mathrm{raw}\left(rho\right)\right)}{2};\mathrm{let}errors=\mathrm{range}\left(error\right);\left(\left(\left(\forall rho\in \mathrm{DensityState}\left(n\right),sigma\in \mathrm{DensityState}\left(n\right),0\le \mathrm{traceDistance}\left(rho,sigma\right)\wedge \mathrm{traceDistance}\left(rho,sigma\right)\le 1\right)\wedge \mathrm{Nonempty}\left(errors\right)\right)\wedge \mathrm{BddAbove}\left(errors\right)\right)\wedge \frac{1-\mathrm{norm}\left(\gamma \left(q\left(i\right)-q\left(j\right)\right)\right)}{2}\le \mathrm{sSup}\left(errors\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/Decoherence/FiniteRecordRecoveryError.finite_record_recovery_error_lower_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Deliver the all-density distance interval from nonnegative trace norm and the unit-trace upper bound. Identify the coefficient error range with the actual composed-channel range and bound it by the interval’s upper endpoint. Both witness errors are below its supremum, and two triangle inequalities with CPTP contraction give the bound.

N is any natural number, including zero; c is an arbitrary complex sequence with exactly the stated support and integer-tsum normalization. The finite coordinate type has decidable equality, and other labels may repeat. The nonzero gap can have either sign. All unbounded sums denote Lean tsum.

DensityState and QuantumChannel are the actual canonical FiniteStateChannel carriers. raw applies CStarMatrix.ofMatrix.symm to a state’s value. act applies the channel’s completely positive map in matrix coordinates, and traceDistance is one half of the actual trace norm from FiniteTraceDistance. The channel C is obtained from the frozen shifted-record recording and partial-trace theorem; its multiplier identity holds for every complex matrix.

The displayed vectors define the pure-state projectors via vecMulVec with pointwise conjugation. Positive semidefiniteness, trace one, original distance one, and channel-image distance equal to the norm of gamma are proved. The pair square-root identity includes zero and arbitrary complex phase.

Every pair of density states has trace distance between zero and one. Trace-norm nonnegativity supplies the lower endpoint, and the triangle inequality with unit trace supplies the upper endpoint. The theorem delivers this entire interval and uses its upper endpoint to bound every recovery error. The error range is over all density states. Its equality with the canonical composed-channel error range, nonemptiness, and upper bound one are proved. Both witness errors lie below its real supremum. Canonical CPTP contraction and the triangle inequality give the lower bound. No compactness, attainment, cosine bound, sharpness, Hamiltonian implementation, recovery algorithm, or physical cost conclusion is asserted.

References

• Truth anchor: D5/S3/Quantum/Decoherence/FiniteRecordRecoveryError.coefficient_gamma_neg
• Truth anchor: D5/S3/Quantum/Decoherence/FiniteRecordRecoveryError.finite_record_pair_witnesses
• Truth anchor: D5/S3/Quantum/Decoherence/FiniteRecordRecoveryError.finite_record_recovery_error_lower_bound
• Truth anchor: D5/S3/Quantum/Decoherence/FiniteRecordRecoveryError.pair_matrix_sqrt
• Truth anchor: D5/S3/Quantum/Decoherence/FiniteRecordRecoveryError.pair_matrix_traceNorm
• Dependency: D5/S3/Quantum/Decoherence/FiniteShiftedRecordChannel
• Dependency: D5/S3/Quantum/Foundation/FiniteTraceDistance