LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

KMS states are invariant under their dynamics

Statement

Let $ω$ be a $β$ -KMS state for a strongly continuous group $α_{t}$ as in Physical-time KMS strip equilibrium condition, with $b = β ℏ > 0$ . Then

$ω (α_{t} (B)) = ω (B) (B \in A, t \in R) .$

Thus invariance is a consequence of the full bounded-strip KMS condition; it is not an extra clause in the definition.

Facts & Assumptions

Given: A unital C $^{*}$ -algebra $A$ , a strongly continuous one-parameter group $α_{t}$ of unital $*$ -automorphisms, $β > 0$ , $ℏ > 0$ , and a $β$ -KMS state $ω$ .

[F1]

Physical-time KMS strip equilibrium condition: for every $A, B \in A$ there is a bounded function $F_{A, B}$ continuous on $S_{b} = {z : 0 \leq Im z \leq b}$ , holomorphic inside, with lower boundary $ω (A α_{t} (B))$ and upper boundary $ω (α_{t} (B) A)$ .

[F2]

Goursat's triangle theorem: a holomorphic function integrates to zero around every triangle contained in its domain: a holomorphic scalar function on an open set has zero integral around every filled triangle contained in that set.

[F3]

Morera's theorem: vanishing triangle integrals characterize holomorphy among continuous functions: a continuous scalar function on an open set is holomorphic if its integral around every contained filled triangle is zero.

[F4]

Liouville's theorem: every bounded entire function is constant: every bounded entire scalar function on $C$ is constant.

Proof

technique · use the KMS condition with the identity observable, glue copies of its strip function periodically, and prove analyticity across the seams by Morera's theorem

Given: [F1]–[F4], $b = β ℏ > 0$ , and an arbitrary $B \in A$ .

1.1F1given

Let $F : = F_{I, B}$ be the strip function from [F1]. Since every $α_{t}$ is unital, its two boundary values coincide: $F (t) = ω (α_{t} (B)) = F (t + i b)$ for every $t \in R$ . Denote this common continuous function of $t$ by $g (t)$ .

2.1F1step 1.1construct

For each integer $k$ , define $\tilde{F} (t + i y) : = F (t + i (y - k b))$ when $k b \leq y \leq (k + 1) b$ . At a shared seam the lower and upper definitions agree by step 1.1, so the definition is single-valued. It is continuous on each closed translated strip and across every seam, is $i b$ -periodic, and is bounded on $C$ by the bound for $F$ on $S_{b}$ . It is holomorphic away from the horizontal seams because there it is a translate of $F$ on its open strip.

3.1F2step 2.1construct

Fix a point on a seam and choose a disk about it that meets no other seam. Let $T$ be any filled triangle in this disk. If $T$ crosses the seam, cut it along that horizontal line; the resulting at most two polygons can each be triangulated by joining one vertex to the other vertices. Every resulting small triangle lies in one of the two closed half-disks. If a small triangle touches the seam, translate it a distance $ϵ > 0$ into that half's open strip; for all sufficiently small $ϵ$ , its translate remains inside that strip and the translated contour integral is zero by [F2]. Uniform continuity of $\tilde{F}$ on a compact neighborhood of the original contour implies the translated integrals converge to the original integral as $ϵ ↓ 0$ . Hence each small triangle has zero integral. Summing their boundary integrals cancels shared edges with opposite orientations and yields $\int_{\partial T} \tilde{F} (z) d z = 0$ . Triangles wholly on one side also have zero integral by [F2].

4.1F3step 2.1step 3.1

Step 3.1 applies to every triangle in the disk. The function $\tilde{F}$ is continuous there by step 2.1, so [F3] makes it holomorphic across the seam in that disk. Away from seams it was already holomorphic by step 2.1; since the point on the seam was arbitrary, $\tilde{F}$ is entire on $C$ .

5.1F4step 1.1step 2.1step 4.1∎

Step 2.1 gives a global bound on $\tilde{F}$ , so [F4] makes it constant. Its restriction to the real axis is $g (t) = ω (α_{t} (B))$ by step 1.1, and at $t = 0$ this is $ω (B)$ . Therefore $ω (α_{t} (B)) = ω (B)$ for every real $t$ . Since $B$ was arbitrary, $ω$ is invariant.

Remarks

The strip tiling below is explanatory only. Each adjacent strip is the translate by $i b$ ; the equality of edge values, not the drawing, is what makes the periodic extension single-valued.

diagram failed to render:
\begin{tikzpicture}[scale=0.85]
  \draw[->] (-3.5,0) -- (3.5,0) node[right] {$\operatorname{Re}z$};
  \draw[->] (-3,0) -- (-3,3.5) node[above] {$\operatorname{Im}z$};
  \draw (-3,0) rectangle (3,1);
  \draw (-3,1) rectangle (3,2);
  \draw (-3,2) rectangle (3,3);
  \node at (0,0.5) {$F(z)$};
  \node at (0,1.5) {$F(z-ib)$};
  \node at (0,2.5) {$F(z-2ib)$};
  \node[left] at (-3,1) {$g(t)$};
  \node[left] at (-3,2) {$g(t)$};
  \node[right] at (3.2,1) {$ib$};
  \node[right] at (3.2,2) {$2ib$};
\end{tikzpicture}

KMS states are invariant under their dynamics

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources