Finite Record Cosine Obstruction

Abstract

A strictly positive cosine error floor for every recovery of the finite-record channel.

Theorem 1.1 (Signed coefficient bound).

$$\forall N\in \mathbb{N},c\in \mathbb{Z}\to \mathbb{C},\left(\left(\forall k\in \mathbb{Z},\left(k<0\vee \mathrm{int}\left(N\right)<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)\Rightarrow \left(\forall ell\in \mathbb{Z},ell\ne 0\Rightarrow \mathrm{norm}\left(\sum _{k\in \mathbb{Z}}c\left(k+ell\right)\cdot \mathrm{conj}\left(c\left(k\right)\right)\right)\le \cos \left(\frac{pi}{\mathrm{real}\left(\mathrm{natDiv}\left(N,\mathrm{natAbs}\left(ell\right)\right)\right)+2}\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/FiniteRecordCosineObstruction.coefficient_gamma_le_cosine (✓ std3). ∎

Source. Repository-derived.

Commentary.

The norms of coefficients in each residue class form a zero-padded finite path. Reindexing preserves the entire squared-norm mass, and the triangle inequality bounds the complex autocorrelation by the adjacent products. The squared zero-boundary averaging estimate and finite Cauchy-Schwarz bound each path. Conjugation transports the result to negative gaps.

Theorem 1.2 (Positive recovery obstruction).

$$\forall iota\in Type,fintype\in \mathrm{Fintype}\left(iota\right),decidableEq\in \mathrm{DecidableEq}\left(iota\right),N\in \mathbb{N},c\in \mathbb{Z}\to \mathbb{C},q\in iota\to \mathbb{Z},\left(\left(\forall k\in \mathbb{Z},\left(k<0\vee \mathrm{int}\left(N\right)<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)\Rightarrow \mathrm{let}\forall t\in \mathbb{Z},gamma\left(t\right)=\sum _{k\in \mathbb{Z}}c\left(k+t\right)\cdot \mathrm{conj}\left(c\left(k\right)\right);\mathrm{let}Q=\sum _{i\in iota}\mathrm{natAbs}\left(q\left(i\right)\right);\mathrm{let}L=N+2\cdot Q+1;\mathrm{let}\forall a\in \mathrm{Fin}\left(L\right),coord\left(a\right)=\mathrm{int}\left(\mathrm{val}\left(a\right)\right)-\mathrm{int}\left(Q\right);\mathrm{let}\forall i\in iota,a\in \mathrm{Fin}\left(L\right),record\left(i,a\right)=c\left(coord\left(a\right)+q\left(i\right)\right);\mathrm{let}\forall p\in \mathrm{Product}\left(iota,\mathrm{Fin}\left(L\right)\right),j\in iota,V\left(p,j\right)=\mathrm{ite}\left(j=\mathrm{fst}\left(p\right),record\left(\mathrm{fst}\left(p\right),\mathrm{snd}\left(p\right)\right),0\right);\mathrm{let}\forall joint\in \mathrm{Matrix}\left(\mathrm{Product}\left(iota,\mathrm{Fin}\left(L\right)\right),\mathrm{Product}\left(iota,\mathrm{Fin}\left(L\right)\right),\mathbb{C}\right),i\in iota,j\in iota,partialTrace\left(joint\right)\left(i,j\right)=\sum _{a\in \mathrm{Fin}\left(L\right)}joint\left(\mathrm{pair}\left(i,a\right),\mathrm{pair}\left(j,a\right)\right);\mathrm{let}\forall A\in \mathrm{Matrix}\left(iota,iota,\mathbb{C}\right),Lambda\left(A\right)=partialTrace\left(V\cdot A\cdot \mathrm{conjTranspose}\left(V\right)\right);\exists C\in \mathrm{QuantumChannel}\left(iota,iota\right),\left(\left(\forall A\in \mathrm{Matrix}\left(iota,iota,\mathbb{C}\right),\mathrm{act}\left(C,A\right)=Lambda\left(A\right)\right)\wedge \left(\forall A\in \mathrm{Matrix}\left(iota,iota,\mathbb{C}\right),i\in iota,j\in iota,Lambda\left(A\right)\left(i,j\right)=gamma\left(q\left(i\right)-q\left(j\right)\right)\cdot A\left(i,j\right)\right)\right)\wedge \left(\forall i\in iota,j\in iota,ell\in \mathbb{Z},ell\ne 0\Rightarrow \left(q\left(i\right)-q\left(j\right)=ell\Rightarrow \left(\forall R\in \mathrm{QuantumChannel}\left(iota,iota\right),\mathrm{let}f=\mathrm{IntFloor}\left(\frac{\mathrm{real}\left(N\right)}{\mathrm{abs}\left(\mathrm{real}\left(ell\right)\right)}\right);\mathrm{let}bound=\frac{1-\cos \left(\frac{pi}{\mathrm{real}\left(f\right)+2}\right)}{2};\mathrm{let}errors=\mathrm{range}\left(rho\in \mathrm{DensityState}\left(iota\right)\mapsto \mathrm{traceDistance}\left(\mathrm{mapState}\left(R,\mathrm{mapState}\left(C,rho\right)\right),rho\right)\right);\mathrm{let}matrixErrors=\mathrm{range}\left(rho\in \mathrm{DensityState}\left(iota\right)\mapsto \frac{\mathrm{traceNorm}\left(\mathrm{act}\left(R,Lambda\left(\mathrm{raw}\left(rho\right)\right)\right)-\mathrm{raw}\left(rho\right)\right)}{2}\right);\left(\left(\left(\left(errors=matrixErrors\wedge \left(\forall rho\in \mathrm{DensityState}\left(iota\right),sigma\in \mathrm{DensityState}\left(iota\right),0\le \mathrm{traceDistance}\left(rho,sigma\right)\wedge \mathrm{traceDistance}\left(rho,sigma\right)\le 1\right)\right)\wedge \mathrm{Nonempty}\left(errors\right)\right)\wedge \mathrm{BddAbove}\left(errors\right)\right)\wedge bound\le \mathrm{sSup}\left(errors\right)\right)\wedge 0<bound\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Quantum/QuantumChannels/FiniteRecordCosineObstruction.finite_record_cosine_obstruction (✓ std3). ∎

Source. Repository-derived.

Commentary.

The recording matrix followed by the displayed partial trace realizes one canonical CPTP channel with the stated action on every complex matrix. The all-density recovery lower bound in terms of the norm of gamma combines with the signed coefficient estimate. Natural division equals the natural floor of the nonnegative real quotient, whose integer floor is its integer cast. The angle is strictly positive and at most pi over two, so this same cosine margin is strictly positive.

The coefficients are complex and may have arbitrary phases and internal zeros. N may be zero, the selected gap may have either sign or exceed N in absolute value, and all other labels may repeat. The type iota has an arbitrary universe, a Fintype instance, and decidable equality.

Every sum over the integers denotes the literal Lean tsum. natDiv denotes division in Nat; the fraction inside IntFloor is division in Real. real and int denote the displayed scalar casts, and natAbs is integer absolute value valued in Nat. The nonzero gap gives a nonzero absolute-value denominator; its floor plus two is positive and nonzero.

QuantumChannel and DensityState are the canonical CPTP maps and all density matrices from FiniteStateChannel. raw applies CStarMatrix.ofMatrix.symm to the density state’s value. act is the canonical map in matrix coordinates. traceNorm is the real trace of the positive square root of the matrix Gram matrix, and traceDistance is one half of that trace norm on the difference. The supremum is the real sSup of the displayed range over all density states.

This obstruction is specific to the displayed finite-record channel and a realized nonzero label gap. Unaffected degenerate subspaces remain outside its obstruction claim. It does not assert an obstruction for arbitrary encodings or physical realizations, nor a Hamiltonian, energy, locality, cost, or recovery-algorithm statement. Cosine-bound attainment and the adjacent uniform-coefficient example are separate statements.

References

• Truth anchor: D5/S3/Quantum/QuantumChannels/FiniteRecordCosineObstruction.coefficient_gamma_le_cosine
• Truth anchor: D5/S3/Quantum/QuantumChannels/FiniteRecordCosineObstruction.finite_record_cosine_obstruction
• Dependency: D5/S3/Quantum/Decoherence/FiniteRecordRecoveryError
• Dependency: D5/S3/QuantumBounds/ReferenceFrameTaxOptimal