Pipeline-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.

Physical-time KMS strip equilibrium condition — Examples

1 · Prerequisites

2 · Summary

The two-level Gibbs example checks the physical-time sign and the upper-edge Boltzmann factor directly for a nontrivial transition. It is an exact finite-dimensional model calculation, not a measured result or an infinite-volume equilibrium claim.

3 · Logical flowchart

4 · Definitions, postulates, theorems and proofs

None yet.

5 · Examples, experiments and counterexamples

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Two-level Gibbs state has the physical-time KMS boundary factor

Example

Let $H = C^{2}$ with orthonormal basis $∣ 0 ⟩, ∣ 1 ⟩$ , and let $H = ε ∣ 1 ⟩ ⟨ 1 ∣$ for an energy $ε > 0$ in joules. For $β > 0$ in J $^{- 1}$ , the finite Gibbs state has

$Z = 1 + e^{- β ε}, p_{0} = Z^{- 1}, p_{1} = e^{- β ε} Z^{- 1} .$

Define $S_{+} = ∣ 1 ⟩ ⟨ 0 ∣$ and $S_{-} = ∣ 0 ⟩ ⟨ 1 ∣$ . With $α_{t} (X) = e^{i t H / ℏ} X e^{- i t H / ℏ}$ , the correlation for $A = S_{-}$ and $B = S_{+}$ is

$F_{S_{-}, S_{+}} (z) = p_{0} e^{i ε z / ℏ} .$

At the upper strip edge $z = t + i β ℏ$ , the exponential contributes $e^{- β ε}$ , so the boundary value is $p_{1} e^{i ε t / ℏ}$ , exactly the reversed-order Gibbs expectation. The full two-level Gibbs state is KMS for every matrix pair by Finite KMS condition exactly determines the Gibbs density; this example checks the physical-time sign and strip-width convention on a nontrivial pair. No measurement or material parameter is being reported.

Facts & Assumptions

Given: $ε > 0$ in joules, $β > 0$ in J $^{- 1}$ , $ℏ > 0$ in J s, the two-level Hilbert space and basis above, and the finite Gibbs state.

[F1]

Physical-time KMS strip equilibrium condition: the physical-time KMS strip has width $β ℏ$ and its upper boundary reverses the order of the two observables.

[F2]

Finite unitary dynamics and Gibbs KMS identity: for finite self-adjoint $H$ , the Gibbs density is $e^{- β H} / Z$ and the finite-time evolution is $α_{t} (X) = e^{i t H / ℏ} X e^{- i t H / ℏ}$ .

[F3]

Finite KMS condition exactly determines the Gibbs density: under its finite spectral-calculus and finite unital C $^{*}$ -algebra clauses [A1]–[A2], the normalized finite Gibbs trace is a KMS state for every matrix pair.

Verification

technique · direct matrix-unit and exponential calculation

Given: [F1]–[F3], $H = ε ∣ 1 ⟩ ⟨ 1 ∣$ , and the definitions of $S_{+}, S_{-}$ .

1.1givenF2algebra

Since $H ∣ 0 ⟩ = 0$ and $H ∣ 1 ⟩ = ε ∣ 1 ⟩$ , direct conjugation gives $α_{z} (S_{+}) = e^{i ε z / ℏ} S_{+}$ and $α_{z} (S_{-}) = e^{- i ε z / ℏ} S_{-}$ . The Gibbs density is $p_{0} ∣ 0 ⟩ ⟨ 0 ∣ + p_{1} ∣ 1 ⟩ ⟨ 1 ∣$ because its two diagonal exponential entries are $1$ and $e^{- β ε}$ .

2.1F1F2step 1.1algebra

Using $S_{-} S_{+} = ∣ 0 ⟩ ⟨ 0 ∣$ and $S_{+} S_{-} = ∣ 1 ⟩ ⟨ 1 ∣$ , the lower correlation is $Tr (ρ S_{-} α_{t} (S_{+})) = p_{0} e^{i ε t / ℏ}$ . At the upper edge, $p_{0} e^{i ε (t + i β ℏ) / ℏ} = p_{0} e^{i ε t / ℏ} e^{- β ε} = p_{1} e^{i ε t / ℏ} = Tr (ρ α_{t} (S_{+}) S_{-})$ . The exponents are dimensionless because $ε t / ℏ$ and $β ε$ are dimensionless.

3.1F1F3step 2.1∎

By [F3], the same finite Gibbs state satisfies the KMS strip identity for every pair in $B (C^{2})$ , not only for $S_{-}, S_{+}$ . The calculation in step 2.1 verifies that the chosen convention places $e^{- β ε}$ at the upper boundary for this transition.

Remarks

For the reversed pair $A = S_{+}$ , $B = S_{-}$ , the lower value is $p_{1} e^{- i ε t / ℏ}$ and the upper value is $p_{0} e^{- i ε t / ℏ}$ ; the same Boltzmann factor relation holds with the energy difference reversed. All quantities here are model parameters or exact finite-matrix expressions, not empirical measurements.