Repeated Record Exponential Decay

Abstract

Repeated finite records contract cross-class coherence at the uniform Gram rate.

Theorem 1.1 (Repeated records converge exponentially to record-class pinching).

$$\begin{gathered} \forall d:Nat,e:Nat, \\ E:\mathrm{Fin}\left(d\right)\to \left(\mathrm{Fin}\left(e\right)\to \mathbb{C}\right), \\ \forall i\in \mathrm{Fin}\left(d\right),\sum _{a\in \mathrm{Fin}\left(e\right)}\Vert E\left(i\right)\left(a\right)\Vert \cdot \Vert E\left(i\right)\left(a\right)\Vert =1, \\ q:\mathrm{Ico}\left(0,1\right), \\ \forall i\in \mathrm{Fin}\left(d\right),j\in \mathrm{Fin}\left(d\right),E\left(i\right)\ne E\left(j\right)\Rightarrow \Vert \mathrm{recordGram}\left(E,i,j\right)\Vert \le q\Rightarrow \\ \mathrm{let}Pch:\mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right)\to \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\rho \mapsto \sum _{l\in \mathrm{range}\left(E\right)}\mathrm{recordClassProjector}\left(E,l\right)\cdot \rho \cdot \mathrm{recordClassProjector}\left(E,l\right);\left(\forall N\in Nat,rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),i\in \mathrm{Fin}\left(d\right),j\in \mathrm{Fin}\left(d\right),\mathrm{entry}\left(\mathrm{iterate}\left(\mathrm{recordChannel}\left(E\right),N,\rho \right),i,j\right)=\mathrm{recordGram}{\left(E,i,j\right)}^N\cdot \mathrm{entry}\left(\rho ,i,j\right)\right)\wedge \left(\left(\forall rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),i\in \mathrm{Fin}\left(d\right),j\in \mathrm{Fin}\left(d\right),\mathrm{entry}\left(Pch\left(\rho \right),i,j\right)=\mathrm{ite}\left(E\left(i\right)=E\left(j\right),\mathrm{entry}\left(\rho ,i,j\right),0\right)\right)\wedge \left(\forall N\in Nat,rho\in \mathrm{Matrix}\left(\mathrm{Fin}\left(d\right),\mathrm{Fin}\left(d\right),\mathbb{C}\right),\Vert \mathrm{iterate}\left(\mathrm{recordChannel}\left(E\right),N,\rho \right)-Pch\left(\rho \right)\Vert \le q^N\cdot \Vert \rho -Pch\left(\rho \right)\Vert \right)\right). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

The record amplitudes construct both the Gram channel and the class projectors. The projector sum therefore uses the actual equality classes of environment records.

The first clause is the exact entrywise iterate. The second computes the projector sum, and the final clause is its Frobenius norm contraction under the stated cross-class Gram bound.

References

• Truth anchor: D5/S3/Quantum/Decoherence/RepeatedRecordExponentialDecay.repeated_record_exponential_decay
• Dependency: D5/S3/Quantum/Decoherence/EnvironmentMarginalChannel