TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Finite spectral balance and distributional fluctuation response

Statement

Let $H$ be finite-dimensional, $H = H^{*}$ with unit J, $ℏ > 0$ with unit J s, $β > 0$ with unit J $^{- 1}$ , and $σ = Z_{β}^{- 1} e^{- β H}$ as in Finite unitary dynamics and stationary Gibbs states. Let $A = A^{*}$ be a matrix observable, write $H u_{i} = E_{i} u_{i}$ in an orthonormal eigenbasis, $r_{i} = e^{- β E_{i}} / Z_{β}$ , $A_{i j} = ⟨ A u_{j}, u_{i} ⟩$ , and $ω_{j i} = (E_{j} - E_{i}) / ℏ$ . Define the finite positive spectral measure $S_{A A} = 2 π \sum_{i, j} r_{i} ∣ A_{i j} ∣^{2} δ_{ω_{j i}},$ where $δ_{ν}$ is unit point mass at frequency $ν$ and $S_{A A} (- \cdot)$ denotes pushforward under $ω \mapsto - ω$ ; $ω_{j i}$ has unit s $^{- 1}$ . With observable unit $[A]$ , the atomic masses of the finite measure $S_{A A}$ have units $[A]^{2}$ . For every smooth compactly supported complex-valued function $φ : R \to C$ , the distribution represented by the measure $S_{A A}$ acts as $⟨ S_{A A}, φ ⟩ = \int_{R} φ (ω) d S_{A A} (ω)$ . In the Fourier convention below, the generalized density $S_{A A} (ω)$ relative to $d ω$ has units $[A]^{2}$ multiplied by seconds; it is a finite sum of Dirac distributions, not an ordinary function density. For time $t \in R$ measured in s, the equilibrium correlation is $C_{A A} (t) = Tr (σ α_{t} (A) A)$ ; its Fourier variable $ω$ is measured in s $^{- 1}$ , and its Fourier convention is $S_{A A} (ω) = \int_{R} e^{i ω t} C_{A A} (t) d t$ in the distributional sense.

For $t \geq 0$ , set $R_{A A} (t) = \frac{i}{ℏ} Tr (σ [α_{t} (A), A])$ . For $ω \in R$ and regulator $η > 0$ , both measured in s $^{- 1}$ , define the retarded transform $χ_{η} (ω) = \int_{0}^{\infty} e^{(i ω - η) t} R_{A A} (t) d t$ . With observable unit $[A]$ , $R_{A A}$ has units $[A]^{2} / (J s)$ and $χ_{η}$ has units $[A]^{2} / J$ . Then $χ_{η} (ω) = \sum_{i, j} \frac{(r_{i} - r_{j}) ∣ A_{i j} ∣^{2}}{ℏ (ω_{j i} - ω - i η)} .$ As $η ↓ 0$ , its boundary value is the corresponding sum of principal-value real parts and Lorentzian imaginary terms weighted by $r_{i} - r_{j}$ , and distributionally $Im χ = \frac{1}{2 ℏ} (1 - e^{- β ℏ ω}) S_{A A} (ω) .$ Detailed balance is $S_{A A} (- d ω) = e^{- β ℏ ω} S_{A A} (d ω)$ . Thus, on $R ∖ {0}$ , $S_{s y m} (d ω) = ℏ \coth ⁣ (\frac{β ℏ ω}{2}) Im χ (d ω), S_{s y m} = \frac{1}{2} (S_{A A} + S_{A A} (- \cdot)) .$ Any zero-frequency mass of $S_{A A}$ is retained separately: the commutator factor vanishes there, so the formula does not determine that atom or define a value for the singular product with $\coth$ at $ω = 0$ .

Facts & Assumptions

Given: The finite-dimensional Hamiltonian, Gibbs matrix, bounded self-adjoint observable, Fourier convention, and positive regulator $η$ above.

[F1]

Finite unitary dynamics and stationary Gibbs states: the finite Hermitian spectral decomposition gives $U (t)$ and the stationary Gibbs matrix $σ$ .

[F2]

Finite matrix spectral and state calculus: finite Hermitian matrices admit basis-independent real spectral decompositions and the finite trace is cyclic.

[F3]

Finite-time Kubo formula with norm remainder: under the fixed Gibbs preparation and control $H - ϵ h (t) B$ , the retarded commutator kernel has the sign $+ i / ℏ$ and is the finite-time first variation.

[F4]

Lorentzian kernels converge to delta and principal-value distributions: $η / (x^{2} + η^{2})$ converges to $π δ_{0}$ and $x / (x^{2} + η^{2})$ to $PV (1 / x)$ on compactly supported $C^{1}$ test functions, with full dominated-convergence proofs.

Proof

technique · finite spectral expansion, exact retarded transform, and the Lorentzian distribution limits

Given: [F1]–[F4], finite $d \geq 1$ , $β > 0$ , and $A = A^{*}$ .

1.1givenF1F2constructalgebra

In the eigenbasis of $H$ , $α_{t} (A)_{i j} = e^{- i ω_{j i} t} A_{i j}$ , so $C_{A A} (t) = \sum_{i, j} r_{i} ∣ A_{i j} ∣^{2} e^{- i ω_{j i} t}$ and the displayed $S_{A A}$ is its Fourier measure under the stated convention. Swapping $i, j$ in the finite sum changes $S_{A A} (- d ω)$ to coefficients $r_{j} ∣ A_{i j} ∣^{2}$ at $ω_{j i}$ ; since $r_{j} / r_{i} = e^{- β ℏ ω_{j i}}$ , this proves detailed balance. The coefficients of $S_{A A}$ are nonnegative.

2.1F1F2F3step 1.1algebra

Expanding the commutator and swapping indices in its second trace term gives $R_{A A} (t) = \frac{i}{ℏ} \sum_{i, j} (r_{i} - r_{j}) ∣ A_{i j} ∣^{2} e^{- i ω_{j i} t}$ . For $η > 0$ , each term is integrable on $[0, \infty)$ and $\int_{0}^{\infty} e^{(i (ω - ω_{j i}) - η) t} d t = - i / (ω_{j i} - ω - i η)$ ; multiplying by $i / ℏ$ yields the stated rational expression.

3.1F1F4step 2.1algebra

For each summand, write $x = ω_{j i} - ω$ and $1 / (x - i η) = x / (x^{2} + η^{2}) + i η / (x^{2} + η^{2})$ . Applying [F4] after the affine change from $ω$ to $x$ gives the principal-value real part and $π δ (ω - ω_{j i})$ imaginary part. On each atom $ω = ω_{j i}$ , detailed balance gives $r_{i} - r_{j} = r_{i} (1 - e^{- β ℏ ω})$ , so summing the finite terms proves the distributional commutator relation.

4.1F1step 1.1step 3.1algebra∎

Detailed balance gives $S_{s y m} = \frac{1}{2} (1 + e^{- β ℏ ω}) S_{A A}$ away from zero, while step 3.1 gives $Im χ = \frac{1}{2 ℏ} (1 - e^{- β ℏ ω}) S_{A A}$ . Dividing on $R ∖ {0}$ yields the stated $ℏ \coth (β ℏ ω / 2)$ factor. At $ω = 0$ , the detailed-balance pair has equal Gibbs weights and the commutator coefficient is zero, whereas the positive correlation measure may have a nonzero atom; therefore that atom must be retained separately.

Finite spectral balance and distributional fluctuation response

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources