A dominant population keeps a state away from orthogonality

For a probability distribution p on ℕ and complex numbers u k of modulus one (the phases e^{−i E_k t} of a state with populations p k), 2 p j − 1 ≤ ‖∑ p k u k‖ for every index j, by the triangle inequality: a level that carries more than half of the population keeps the autocorrelation away from zero at every time, whatever the energy moments. This is the cut-off inequality |A(t)| ≥ α|Ā(t)| − (1 − α) of Uffink, in the form of M. Andrews, Phys. Rev. A 75, 062112 (2007), Eq. (21), with the cut-off isolating one level.

Main results

• Dilog.two_mul_sub_one_le_norm_tsum: 2 p j − 1 ≤ ‖∑ p k u k‖ for phases of modulus one
• Dilog.tsum_ne_zero_of_half_lt: the autocorrelation never vanishes when some p j > 1/2

References

• C. Marín, The Clock That Never Ticks: a machine-checked path from the dilogarithm to quantum speed limits in Lean 4, Zenodo (2026), doi:10.5281/zenodo.20675271, thm:clock.

theorem Dilog.two_mul_sub_one_le_norm_tsum (p : ℕ → ℝ) (hp : ∀ (k : ℕ), 0 ≤ p k) (hs : HasSum p 1) (u : ℕ → ℂ) (hu : ∀ (k : ℕ), ‖u k‖ = 1) (j : ℕ) : 2 * p j - 1 ≤ ‖∑' (k : ℕ), ↑(p k) * u k‖

The dominant-population floor. For a probability distribution p and phases u k of modulus one, 2 p j - 1 ≤ ‖∑ p k u k‖ for every index j.

theorem Dilog.tsum_ne_zero_of_half_lt (p : ℕ → ℝ) (hp : ∀ (k : ℕ), 0 ≤ p k) (hs : HasSum p 1) (u : ℕ → ℂ) (hu : ∀ (k : ℕ), ‖u k‖ = 1) {j : ℕ} (hj : 1 / 2 < p j) : ∑' (k : ℕ), ↑(p k) * u k ≠ 0

A dominant population forbids orthogonality. If some population exceeds 1/2, the autocorrelation ∑ p k u k never vanishes.