No state turns orthogonal before πħ / (2ΔE)

The survival amplitude A(t) = ∑ pk e−iEkt is the sum of the arrows on the right. Mandelstam–Tamm, proved in Lean: ‖A(t)‖ ≥ cos(ΔE·t) until ΔE·t = π/2. The arrow tip can never enter the orange disc; the disc shrinks to nothing exactly at π/2.

Two equal branches touch the floor at every time and reach zero exactly at π/2: the constant cannot be improved. Every other spectrum stays strictly above. Energies are rescaled so that ΔE = 1 and centred so that ⟨E⟩ = 0 (a global phase). Lean: MandelstamTamm1945.cos_le_norm_amplitude, orthogonality_time, and on ℂ^d, cos_le_norm_inner_evolve — source.