Phase-Record Recovery Criterion

Abstract

Finite phase records recover exactly at unit overlap, while strict overlap contraction leaves a squared residual factor.

Theorem 1.1 (Finite phase-record recovery and its two obstructions).

$$\begin{array}{c}\forall Copy:\mathrm{Type},[\mathrm{Fintype}\left(Copy\right)],[\mathrm{DecidableEq}\left(Copy\right)],\\ R:Copy\to \mathrm{EnvironmentRecord},\rho :\mathrm{QubitMatrix},i:\mathrm{Fin}\left(2\right),j:\mathrm{Fin}\left(2\right),\\ ((\forall k,|\mathrm{recordOverlap}\left(R(k),i,j\right)|=1)\Rightarrow \mathrm{multiRecordChannel}\left(\mathrm{reverseOn}\left(univ,R\right),\mathrm{multiRecordChannel}\left(R,\rho \right)\right)(i)(j)=\rho (i)(j))\wedge \\ ((\exists k,|\mathrm{recordOverlap}\left(R(k),i,j\right)|<1)\Rightarrow \exists k,\\ |\mathrm{recordOverlap}\left(R(k),i,j\right)|<1\wedge |\mathrm{recordOverlap}\left(R(k),i,j\right){|}^2<1\wedge \\ \mathrm{recordChannel}\left(\mathrm{reverseRecord}\left(R(k)\right),\mathrm{recordChannel}\left(R(k),\rho \right)\right)(i)(j)=|\mathrm{recordOverlap}\left(R(k),i,j\right){|}^2\rho (i)(j)\wedge \\ (\rho (i)(j)\ne 0\Rightarrow \mathrm{recordChannel}\left(\mathrm{reverseRecord}\left(R(k)\right),\mathrm{recordChannel}\left(R(k),\rho \right)\right)(i)(j)\ne \rho (i)(j)))\wedge \\ (\forall k,(\forall l,l\ne k\Rightarrow |\mathrm{recordOverlap}\left(R(l),i,j\right)|=1)\Rightarrow \mathrm{recordOverlap}\left(R(k),i,j\right)\ne 1\Rightarrow \rho (i)(j)\ne 0\Rightarrow \\ \mathrm{reverseChannelOn}\left(\mathrm{erase}\left(univ,k\right),R,\mathrm{multiRecordChannel}\left(R,\rho \right)\right)(i)(j)\ne \rho (i)(j)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/CoherentReversal/PhaseRecordRecoveryCriterion.phase_record_recovery_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let a finite family of canonical environment records act on one selected matrix entry. If every record overlap has norm one, the imported all-copy reversal theorem restores that entry after every record is amplitude-conjugated.

If some overlap has norm strictly below one, the same record followed by its conjugate record channel multiplies the entry by the squared overlap norm, which is still strictly below one. Consequently a nonzero selected entry is not restored.

Finally, if one overlap unequal to one is left unreversed while every other overlap has norm one, the imported surviving-copy theorem shows that a nonzero selected entry is not restored. The statement uses the frozen record, overlap, channel, and reversal operations throughout; it introduces no replacement model.

References

• Truth anchor: D5/S3/ObserverMemory/CoherentReversal/PhaseRecordRecoveryCriterion.phase_record_recovery_criterion
• Dependency: D5/S3/ObserverMemory/JointCoherentReversal