Record Action Controls Coherence Survival

Abstract

Normalized record overlaps control coherence survival and its logarithmic rate.

Theorem 1.1 (Record action controls coherence survival).

$$\forall I\in Type,E\in Type,R\in \mathbb{N}\to \left(I\to E\right),i\in I,j\in I,rho0\in \mathbb{C},\left(\left(\mathrm{NormedAddCommGroup}\left(E\right)\wedge \mathrm{InnerProductSpace}\left(\mathbb{C},E\right)\right)\wedge \left(\left(\forall r\in \mathbb{N},i\in I,\Vert R\left(r,i\right)\Vert =1\right)\wedge rho0\ne 0\right)\right)\Rightarrow \mathrm{let}g:\mathbb{N}\to \mathbb{C}=r:\mathbb{N}\mapsto \mathrm{inner}\left(R\left(r,j\right),R\left(r,i\right)\right);\mathrm{let}Gamma:\mathbb{N}\to \mathbb{C}=N:\mathbb{N}\mapsto \mathrm{rangeProduct}\left(N,g\right);\mathrm{let}A:\mathbb{N}\to [0,\infty ]=N:\mathbb{N}\mapsto \mathrm{toENNReal}\left(\mathrm{negLog}\left(\mathrm{ofReal}\left(\Vert Gamma\left(N\right)\Vert \right)\right)\right);\mathrm{let}rho:\mathbb{N}\to \mathbb{C}=N:\mathbb{N}\mapsto Gamma\left(N\right)\cdot rho0;\left(\forall N\in \mathbb{N},\mathrm{ofReal}\left(\Vert rho\left(N\right)\Vert \right)=\exp \left(-\mathrm{coeEReal}\left(A\left(N\right)\right)\right)\cdot \mathrm{ofReal}\left(\Vert rho0\Vert \right)\right)\wedge \left(\mathrm{Monotone}\left(A\right)\wedge \left(\forall lambda\in EReal,\mathrm{TendstoAtTop}\left(N,\mathbb{N},\frac{\mathrm{coeEReal}\left(A\left(N\right)\right)}{\mathrm{coeEReal}\left(N\right)},lambda\right)\Rightarrow \mathrm{TendstoAtTop}\left(N,\mathbb{N},\frac{\mathrm{negLog}\left(\frac{\mathrm{ofReal}\left(\Vert rho\left(N\right)\Vert \right)}{\mathrm{ofReal}\left(\Vert rho0\Vert \right)}\right)}{\mathrm{coeEReal}\left(N\right)},lambda\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

Each record overlap is constructed from the Hilbert inner product of the normalized record vectors. Their finite product defines the surviving coherence, and its extended negative logarithm defines the record action.

References

• Truth anchor: D5/S3/Quantum/Decoherence/RecordActionCoherenceSurvival.record_action_controls_coherence_survival
• Dependency: D5/S3/Quantum/PureState/RecordCoherenceComplementarity