TH5c: the eigenstate thermalisation hypothesis as a hypothesis field, and what follows from it

Category: 3-Local (conceptually 1-Mathlib; CSD-free finite-dimensional quantum statistical mechanics) with a CSD reading; kept in the CSD.Thermo tree alongside TH1–TH5d (specs/thermo-plan.md TH5; specs/BACKLOG.md ▶ OPEN QUEUE #3).

What ETH is, and what this module does and doesn't claim

The eigenstate thermalisation hypothesis (Deutsch 1991, Srednicki 1994) says that for a generic many-body Hamiltonian the diagonal matrix elements ⟨eₙ, A eₙ⟩ of a physical observable vary smoothly with the energy, so ⟨eₙ, A eₙ⟩ ≈ f(Eₙ) for a smooth f. It's a statement about which Hamiltonians are generic and belongs to random-matrix theory, and the corpus doesn't prove it (BACKLOG #21, research). This module does the other half. It states ETH as a hypothesis field SatisfiesETH and proves what a system that satisfies it does.

1. dephasing. Sample the Heisenberg expectation ⟨A⟩ₜ = ⟨ψₜ, A ψₜ⟩ along the Schrödinger orbit ψₜ = exp(−itτH) ψ at a timestep τ. Its Birkhoff (time) average converges, and the limit is the diagonal ensemble value ∑ₙ |cₙ|² ⟨eₙ, A eₙ⟩, as long as the sampled phases e^{iτ(Eₙ − Eₘ)} are never 1 for n ≠ m (Nonresonant). Every off-diagonal term is a geometric sequence on the unit circle with ratio ≠ 1, and those average to zero.
2. ETH turns the diagonal ensemble into a function of the energy. If SatisfiesETH holds with tolerance ε, the diagonal ensemble is within ε of ∑ₙ |cₙ|² f(Eₙ). If moreover the state lives in an energy window of half-width δ around E on which f moves by at most η, both the time average and the microcanonical average of ⟨eₙ, A eₙ⟩ over that window are within ε + η of f(E), so the time average is within 2(ε + η) of the microcanonical value. That's thermalisation, as the long-time value of A then depends on the initial state only through its energy.

Main results

• energyPhase hH τ n = e^{−iτEₙ}; schrodingerUnitary_eq_conj (the Schrödinger unitary in the eigenbasis is the diagonal of phases), schrodingerUnitary_pow_mulVec (its powers act on the eigencoordinates by powers of the phases);
• heisenbergObs A v = re ⟨v, A v⟩, eigenCoord hH ψ n = ⟨eₙ, ψ⟩, diagonalEnsemble hH A ψ;
• tendsto_cesaro_geom — the Cesàro average of a unit-modulus geometric sequence with ratio ≠ 1 tends to 0; tendsto_cesaro_trigPoly — a finite sum of such sequences averages to the sum of its ratio-one coefficients;
• ★★ tendsto_birkhoffAverage_heisenbergObs (dephasing): under Nonresonant hH τ, the Birkhoff average of heisenbergObs A along v ↦ U v converges to the diagonal ensemble; nonresonant_of_nondegenerate — a non-degenerate spectrum sampled with a timestep smaller than 2π / max|Eₙ − Eₘ| is nonresonant;
• SatisfiesETH hH A f ε, microcanonicalDiag hH A E δ;
• ★ abs_diagonalEnsemble_sub_le_of_eth (the diagonal ensemble tracks f to within ε), ★ abs_diagonalEnsemble_sub_le_of_window (within ε + η of f(E) on a window), ★ abs_microcanonicalDiag_sub_le (the microcanonical average too);
• ★★ eth_time_average (TH5c): under nonresonance, ETH, and an energy window, the time average converges to a value within 2(ε + η) of the microcanonical value.

CSD reading

Records read ⟨A⟩ₜ at the sampled times, and the Birkhoff average is the record frequency the long run delivers (Thermo/Equilibration.lean sets this up for the same birkhoffAverage). Nothing here needs mixing, which Equilibration.lean proves unitary dynamics can't supply. The mechanism is dephasing of the off-diagonal terms, and it holds for every finite-dimensional unitary orbit once the sampling is nonresonant. What ETH adds is that the value the records settle to depends on the preparation only through its energy, so an apparatus can't tell thermal preparations apart by their long-time averages. Whether the de-isolation dynamics of Σ produces Hamiltonians that satisfy ETH is BACKLOG #21.

Honest scope

• Discrete sampling. The time average is Mathlib's birkhoffAverage along the one-step map v ↦ exp(−iτH) v, as in Equilibration.lean. The continuous-time average (1/T)∫₀ᵀ is not stated; it's the same dephasing with ∫e^{iωt} in place of the geometric sum.
• Nonresonance is a hypothesis about the timestep, not only about the spectrum. A non-degenerate spectrum makes every sufficiently small timestep nonresonant (nonresonant_of_nondegenerate), and a resonant timestep genuinely fails to dephase.
• ETH is stated for the diagonal elements only, which is all the time average sees, so the off-diagonal part of ETH (the e^{−S/2} suppression that governs fluctuations) isn't stated.
• Finite dimension, one observable, one state; no bath.

Provenance

Foundational-triple only; no sorry, no new axioms. Consumes TH3/TH5a's eigenbasis lemmas, LF4/ProjectedDynamics.lean's schrodingerUnitary, and Mathlib's matrix exponential, geom_sum_eq, birkhoffAverage and Complex.exp_eq_one_iff.

References

specs/thermo-plan.md TH5; specs/BACKLOG.md (▶ OPEN QUEUE #3; #21 for ETH itself); Thermo/Equilibration.lean (E4, the same birkhoffAverage; not_hasCorrelationDecay_blockPop_of_unitary); Thermo/Jarzynski.lean (star_dotProduct_eigenvectorBasis_self); Thermo/FreeEnergy.lean (eigenvectorUnitary_isUnit, smul_conj); LF4/ProjectedDynamics.lean (schrodingerUnitary, schrodingerGen); specs/future-work.md.

The Schrödinger unitary in the eigenbasis

noncomputable def CSD.Thermo.energyPhase {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (τ : ℝ) (n : Fin N) : ℂ

The phase e^{−iτEₙ} the n-th eigenvector picks up in one timestep.

Equations

• CSD.Thermo.energyPhase hH τ n = Complex.exp (-↑τ * Complex.I * ↑(hH.eigenvalues n))

theorem CSD.Thermo.norm_energyPhase {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (τ : ℝ) (n : Fin N) : ‖energyPhase hH τ n‖ = 1

theorem CSD.Thermo.star_energyPhase {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (τ : ℝ) (n : Fin N) : star (energyPhase hH τ n) = Complex.exp (↑τ * Complex.I * ↑(hH.eigenvalues n))

theorem CSD.Thermo.schrodingerUnitary_eq_conj {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (τ : ℝ) : ↑(Matrix.schrodingerUnitary hH τ) = ↑hH.eigenvectorUnitary * Matrix.diagonal (energyPhase hH τ) * star ↑hH.eigenvectorUnitary

The Schrödinger unitary in the eigenbasis: exp(−iτH) = V · diag(e^{−iτEₙ}) · Vᴴ.

noncomputable def CSD.Thermo.eigenCoord {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (ψ : Fin N → ℂ) (n : Fin N) : ℂ

The eigencoordinates of ψ: cₙ = ⟨eₙ, ψ⟩.

Equations

• CSD.Thermo.eigenCoord hH ψ n = star (hH.eigenvectorBasis n).ofLp ⬝ᵥ ψ

theorem CSD.Thermo.eigenCoord_eq_star_mulVec {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (ψ : Fin N → ℂ) : eigenCoord hH ψ = (star ↑hH.eigenvectorUnitary).mulVec ψ

theorem CSD.Thermo.schrodingerUnitary_pow_mulVec {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (τ : ℝ) (t : ℕ) (ψ : Fin N → ℂ) : (↑(Matrix.schrodingerUnitary hH τ) ^ t).mulVec ψ = (↑hH.eigenvectorUnitary).mulVec fun (n : Fin N) => energyPhase hH τ n ^ t * eigenCoord hH ψ n

The powers of the Schrödinger unitary act on the eigencoordinates by powers of the phases: Uᵗ ψ = V · (e^{−iτEₙ t} cₙ)ₙ.

The Heisenberg time series

noncomputable def CSD.Thermo.heisenbergObs {N : ℕ} (A : Matrix (Fin N) (Fin N) ℂ) (v : Fin N → ℂ) : ℝ

The expectation re ⟨v, A v⟩ of A in the (unnormalised) vector v.

Equations

• CSD.Thermo.heisenbergObs A v = RCLike.re (star v ⬝ᵥ A.mulVec v)

noncomputable def CSD.Thermo.eigenMatrix {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (A : Matrix (Fin N) (Fin N) ℂ) : Matrix (Fin N) (Fin N) ℂ

A read in the eigenbasis of H: à = Vᴴ A V, with Ãₙₘ = ⟨eₙ, A eₘ⟩.

Equations

• CSD.Thermo.eigenMatrix hH A = star ↑hH.eigenvectorUnitary * A * ↑hH.eigenvectorUnitary

theorem CSD.Thermo.eigenMatrix_apply {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (A : Matrix (Fin N) (Fin N) ℂ) (n m : Fin N) : eigenMatrix hH A n m = star (hH.eigenvectorBasis n).ofLp ⬝ᵥ A.mulVec (hH.eigenvectorBasis m).ofLp

theorem CSD.Thermo.star_mulVec_dotProduct {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (A : Matrix (Fin N) (Fin N) ℂ) (w : Fin N → ℂ) : star ((↑hH.eigenvectorUnitary).mulVec w) ⬝ᵥ A.mulVec ((↑hH.eigenvectorUnitary).mulVec w) = star w ⬝ᵥ (eigenMatrix hH A).mulVec w

The quadratic form of A in a vector V w is the quadratic form of Ã in w.

theorem CSD.Thermo.star_dotProduct_mulVec_eq_sum {N : ℕ} (M : Matrix (Fin N) (Fin N) ℂ) (w : Fin N → ℂ) : star w ⬝ᵥ M.mulVec w = ∑ n : Fin N, ∑ m : Fin N, star (w n) * M n m * w m

The quadratic form as a double sum over the eigenbasis.

theorem CSD.Thermo.heisenbergObs_pow {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (τ : ℝ) (A : Matrix (Fin N) (Fin N) ℂ) (ψ : Fin N → ℂ) (t : ℕ) : heisenbergObs A ((↑(Matrix.schrodingerUnitary hH τ) ^ t).mulVec ψ) = RCLike.re (∑ n : Fin N, ∑ m : Fin N, star (eigenCoord hH ψ n) * eigenMatrix hH A n m * eigenCoord hH ψ m * (star (energyPhase hH τ n) * energyPhase hH τ m) ^ t)

The Heisenberg time series is a trigonometric polynomial: sampled at timestep τ, ⟨A⟩ₜ = re ∑ₙₘ (c̄ₙ Ãₙₘ cₘ) · (e^{iτ(Eₙ − Eₘ)})ᵗ.

Cesàro averages of geometric sequences on the unit circle

theorem CSD.Thermo.tendsto_cesaro_geom {l : ℂ} (hl : ‖l‖ = 1) (h1 : l ≠ 1) : Filter.Tendsto (fun (T : ℕ) => (↑T)⁻¹ * ∑ t ∈ Finset.range T, l ^ t) Filter.atTop (nhds 0)

A unit-modulus geometric sequence with ratio ≠ 1 has Cesàro average tending to 0.

theorem CSD.Thermo.tendsto_cesaro_one : Filter.Tendsto (fun (T : ℕ) => (↑T)⁻¹ * ∑ t ∈ Finset.range T, 1 ^ t) Filter.atTop (nhds 1)

The Cesàro average of the constant sequence 1 tends to 1.

theorem CSD.Thermo.tendsto_cesaro_trigPoly {ι : Type u_1} [Fintype ι] (α l : ι → ℂ) (hl : ∀ (q : ι), ‖l q‖ = 1) : Filter.Tendsto (fun (T : ℕ) => (↑T)⁻¹ * ∑ t ∈ Finset.range T, ∑ q : ι, α q * l q ^ t) Filter.atTop (nhds (∑ q : ι, if l q = 1 then α q else 0))

A finite sum of unit-modulus geometric sequences averages to the sum of its ratio-one coefficients.

★★ Dephasing: the time average is the diagonal ensemble

def CSD.Thermo.Nonresonant {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (τ : ℝ) : Prop

Nonresonant sampling: no two distinct eigenvectors have the same sampled phase, e^{iτ(Eₙ − Eₘ)} ≠ 1 for n ≠ m.

Equations

• CSD.Thermo.Nonresonant hH τ = ∀ (n m : Fin N), n ≠ m → star (CSD.Thermo.energyPhase hH τ n) * CSD.Thermo.energyPhase hH τ m ≠ 1

noncomputable def CSD.Thermo.diagonalEnsemble {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (A : Matrix (Fin N) (Fin N) ℂ) (ψ : Fin N → ℂ) : ℝ

The diagonal ensemble: ∑ₙ |cₙ|² ⟨eₙ, A eₙ⟩, the value the time average settles to.

Equations

• CSD.Thermo.diagonalEnsemble hH A ψ = ∑ n : Fin N, ‖CSD.Thermo.eigenCoord hH ψ n‖ ^ 2 * RCLike.re (CSD.Thermo.eigenMatrix hH A n n)

theorem CSD.Thermo.mulVec_iterate {N : ℕ} (U : Matrix (Fin N) (Fin N) ℂ) (t : ℕ) (v : Fin N → ℂ) : (fun (w : Fin N → ℂ) => U.mulVec w)^[t] v = (U ^ t).mulVec v

The iterates of v ↦ U v are the powers of U.

theorem CSD.Thermo.tendsto_birkhoffAverage_heisenbergObs {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) {τ : ℝ} (hres : Nonresonant hH τ) (A : Matrix (Fin N) (Fin N) ℂ) (ψ : Fin N → ℂ) : Filter.Tendsto (fun (T : ℕ) => birkhoffAverage ℝ (fun (v : Fin N → ℂ) => (↑(Matrix.schrodingerUnitary hH τ)).mulVec v) (heisenbergObs A) T ψ) Filter.atTop (nhds (diagonalEnsemble hH A ψ))

★★ Dephasing. Under nonresonant sampling, the Birkhoff average of the Heisenberg expectation of A along the Schrödinger orbit of ψ converges to the diagonal ensemble value. The off-diagonal terms of the trigonometric polynomial ⟨A⟩ₜ are unit-modulus geometric sequences with ratio ≠ 1, and their Cesàro averages vanish.

theorem CSD.Thermo.nonresonant_of_nondegenerate {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) {τ : ℝ} (hsmall : ∀ (n m : Fin N), n ≠ m → 0 < |τ * (hH.eigenvalues n - hH.eigenvalues m)| ∧ |τ * (hH.eigenvalues n - hH.eigenvalues m)| < 2 * Real.pi) : Nonresonant hH τ

A non-degenerate spectrum sampled with a small enough timestep is nonresonant: if 0 < |τ(Eₙ − Eₘ)| < 2π for all n ≠ m, no sampled phase ratio is 1.

ETH as a hypothesis field, and what it buys

def CSD.Thermo.SatisfiesETH {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (A : Matrix (Fin N) (Fin N) ℂ) (f : ℝ → ℝ) (ε : ℝ) : Prop

The eigenstate thermalisation hypothesis, diagonal form, as a hypothesis field: the diagonal matrix elements ⟨eₙ, A eₙ⟩ are within ε of a function f of the energy Eₙ.

Equations

• CSD.Thermo.SatisfiesETH hH A f ε = ∀ (n : Fin N), |RCLike.re (CSD.Thermo.eigenMatrix hH A n n) - f (hH.eigenvalues n)| ≤ ε

theorem CSD.Thermo.sum_normSq_eigenCoord {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (ψ : Fin N → ℂ) (hψ : star ψ ⬝ᵥ ψ = 1) : ∑ n : Fin N, ‖eigenCoord hH ψ n‖ ^ 2 = 1

The eigencoordinates of a unit vector carry unit total weight.

theorem CSD.Thermo.abs_sum_weighted_sub_le {ι : Type u_1} (s : Finset ι) (w a b : ι → ℝ) (hw : ∀ i ∈ s, 0 ≤ w i) (hsum : ∑ i ∈ s, w i = 1) {ε : ℝ} (hab : ∀ i ∈ s, w i ≠ 0 → |a i - b i| ≤ ε) : |∑ i ∈ s, w i * a i - ∑ i ∈ s, w i * b i| ≤ ε

A weighted average of numbers within ε of their targets is within ε of the weighted average of the targets.

theorem CSD.Thermo.abs_diagonalEnsemble_sub_le_of_eth {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) {A : Matrix (Fin N) (Fin N) ℂ} {f : ℝ → ℝ} {ε : ℝ} (heth : SatisfiesETH hH A f ε) (ψ : Fin N → ℂ) (hψ : star ψ ⬝ᵥ ψ = 1) : |diagonalEnsemble hH A ψ - ∑ n : Fin N, ‖eigenCoord hH ψ n‖ ^ 2 * f (hH.eigenvalues n)| ≤ ε

★ ETH makes the diagonal ensemble a function of the energy distribution: for a unit state, |∑ₙ |cₙ|² ⟨eₙ, A eₙ⟩ − ∑ₙ |cₙ|² f(Eₙ)| ≤ ε.

def CSD.Thermo.InEnergyWindow {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (ψ : Fin N → ℂ) (E δ : ℝ) : Prop

An energy window for a state: every eigencomponent it carries has energy within δ of E.

Equations

• CSD.Thermo.InEnergyWindow hH ψ E δ = ∀ (n : Fin N), CSD.Thermo.eigenCoord hH ψ n ≠ 0 → |hH.eigenvalues n - E| ≤ δ

theorem CSD.Thermo.abs_diagonalEnsemble_sub_le_of_window {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) {A : Matrix (Fin N) (Fin N) ℂ} {f : ℝ → ℝ} {ε : ℝ} (heth : SatisfiesETH hH A f ε) {E δ η : ℝ} (hflat : ∀ (x : ℝ), |x - E| ≤ δ → |f x - f E| ≤ η) (ψ : Fin N → ℂ) (hψ : star ψ ⬝ᵥ ψ = 1) (hwin : InEnergyWindow hH ψ E δ) : |diagonalEnsemble hH A ψ - f E| ≤ ε + η

★ On an energy window where f is η-flat, the diagonal ensemble is within ε + η of f(E).

The microcanonical value, and TH5c

noncomputable def CSD.Thermo.microcanonicalDiag {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) (A : Matrix (Fin N) (Fin N) ℂ) (E δ : ℝ) : ℝ

The microcanonical average of A over the energy window |Eₙ − E| ≤ δ: the plain average of the diagonal elements ⟨eₙ, A eₙ⟩ over the eigenstates in the window.

Equations

• CSD.Thermo.microcanonicalDiag hH A E δ = (∑ n : Fin N with |hH.eigenvalues n - E| ≤ δ, RCLike.re (CSD.Thermo.eigenMatrix hH A n n)) / ↑{n : Fin N | |hH.eigenvalues n - E| ≤ δ}.card

theorem CSD.Thermo.abs_microcanonicalDiag_sub_le {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) {A : Matrix (Fin N) (Fin N) ℂ} {f : ℝ → ℝ} {ε : ℝ} (heth : SatisfiesETH hH A f ε) {E δ η : ℝ} (hflat : ∀ (x : ℝ), |x - E| ≤ δ → |f x - f E| ≤ η) (hne : {n : Fin N | |hH.eigenvalues n - E| ≤ δ}.Nonempty) : |microcanonicalDiag hH A E δ - f E| ≤ ε + η

★ Under ETH the microcanonical average is within ε + η of f(E), whenever the window contains at least one eigenstate.

theorem CSD.Thermo.window_nonempty_of_inEnergyWindow {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) {ψ : Fin N → ℂ} {E δ : ℝ} (hwin : InEnergyWindow hH ψ E δ) (hψ : star ψ ⬝ᵥ ψ = 1) : {n : Fin N | |hH.eigenvalues n - E| ≤ δ}.Nonempty

A state in an energy window that carries any weight at all puts an eigenstate in it.

theorem CSD.Thermo.eth_time_average {N : ℕ} {H : Matrix (Fin N) (Fin N) ℂ} (hH : H.IsHermitian) {τ : ℝ} (hres : Nonresonant hH τ) {A : Matrix (Fin N) (Fin N) ℂ} {f : ℝ → ℝ} {ε : ℝ} (heth : SatisfiesETH hH A f ε) {E δ η : ℝ} (hflat : ∀ (x : ℝ), |x - E| ≤ δ → |f x - f E| ≤ η) (ψ : Fin N → ℂ) (hψ : star ψ ⬝ᵥ ψ = 1) (hwin : InEnergyWindow hH ψ E δ) : Filter.Tendsto (fun (T : ℕ) => birkhoffAverage ℝ (fun (v : Fin N → ℂ) => (↑(Matrix.schrodingerUnitary hH τ)).mulVec v) (heisenbergObs A) T ψ) Filter.atTop (nhds (diagonalEnsemble hH A ψ)) ∧ |diagonalEnsemble hH A ψ - microcanonicalDiag hH A E δ| ≤ 2 * (ε + η)

★★ TH5c — ETH implies thermalisation of the time average. Take a Hamiltonian H, an observable A satisfying ETH with tolerance ε for a function f of the energy, a unit state ψ in an energy window of half-width δ around E on which f moves by at most η, and a nonresonant sampling timestep τ. Then the time average of ⟨A⟩ₜ along the Schrödinger orbit converges, and its limit is within 2(ε + η) of the microcanonical average of A over the window. The long-time value of A depends on the preparation only through its energy.