ExampleConstruction: AI-adaptedVerification: 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.

No automatic equilibration

Example

Assume the Axiom of Countable Choice and the Axiom of Choice. Let $ω > 0$ , $ℏ > 0$ , let $F (C)$ be the one-mode Fock space with its complete orthonormal family $(e_{n})_{n \in N}$ , number operator $N$ and operators $A_{\pm} (1)$ as in Fixed-mode number law and Number operator domain, and let $A : = ω N, U (t) : = e^{- i t A / ℏ} = \int_{R} e^{- i t λ / ℏ} d E (λ),$ the unitary group generated by the self-adjoint $A$ with spectral projection valued measure $E$ (Spectral theorem for unbounded self-adjoint operators (PVM form), A self-adjoint operator generates a strongly continuous unitary group). Put $ψ_{0} : = \frac{e_{0} + e_{1}}{\sqrt{2}}, ψ (t) : = U (t) ψ_{0}, Y : = A_{+} (1) + A_{-} (1), D (Y) : = D (A_{+} (1)) \cap D (A_{-} (1)) .$ Then $∥ ψ_{0} ∥ = 1$ , $ψ (t) \in D (Y)$ for every $t$ , and with $θ : = ω t / ℏ$ :

(a) $ψ (t) = \frac{e_{0} + e^{- i θ} e_{1}}{\sqrt{2}}$ ;

(b) the expectation $t \mapsto ⟨ ψ (t), Y ψ (t) ⟩$ equals $\cos (ω t / ℏ)$ ; consequently it tends to no limit as $t \to + \infty$ , since it equals $1$ at $t = 2 π ℏ n / ω$ and $- 1$ at $t = (2 n + 1) π ℏ / ω$ ;

(c) the state itself has no norm limit: $∥ ψ (t) - ψ (s) ∥^{2} = 1 - \cos (ω (t - s) / ℏ)$ , so $∥ ψ (t_{n}) - ψ (s_{n}) ∥ = \sqrt{2}$ for the two sequences of (b);

(d) in contrast, the weight operator $G_{β}$ and the density operator $ρ_{β} = G_{β} / Z (β)$ of Single-mode thermal trace are invariant under the same dynamics: $U (t) G_{β} U (t)^{*} = G_{β}, U (t) ρ_{β} U (t)^{*} = ρ_{β} (t \in R, β > 0) .$

Thus a stationary equilibrium weight is available on this space, but the unitary dynamics of the non-stationary unit vector $ψ_{0}$ produces no convergence of the state or of the displayed expectation: equilibration is not a consequence of unitary evolution alone. No physical interpretation of $ψ_{0}$ , $Y$ , $β$ or $ρ_{β}$ is asserted; in particular no thermal state is derived, and the example does not assert that any physical preparation oscillates.

Verification

Given: the one-mode Fock space $F (C)$ with complete orthonormal family $(e_{n})_{n \in N}$ , the self-adjoint $ω N$ , its unitary group $U (t)$ , the vector $ψ_{0}$ , the symmetric operator $Y = A_{+} (1) + A_{-} (1)$ and the objects $G_{β}, ρ_{β}, Z (β)$ of Single-mode thermal trace.

[F1] $A : = ω N$ is self-adjoint on $D (N)$ , $N \geq 0$ , $N e_{n} = n e_{n}$ , and the eigenvalues of $N$ on $F (C)$ are exactly $N$ , each with eigenvector $e_{n}$ ; $D (N) \subseteq D_{1} : = {ψ : \sum_{n} (n + 1) ∥ ψ_{n} ∥^{2} < \infty}$ , and $F_{0}$ is dense (Number operator domain (a), (b), (d), Hilbert direct-sum construction (c)).

[F2] Oscillator coefficients (in particular $e_{n} \in D (A_{+} (1)) \cap D (A_{-} (1))$ for every $n$ , as required by these operator equalities): $A_{+} (1) e_{n} = \sqrt{n + 1} e_{n + 1}$ and $A_{-} (1) e_{n} = \sqrt{n} e_{n - 1}$ for $n \geq 1$ , $A_{-} (1) e_{0} = 0$ (Fixed-mode number law (a)); $(e_{n})$ is a complete orthonormal family of $F (C)$ (Fixed-mode number law, Orthonormal families, complete orthonormal systems and Hilbert bases).

[F3] Spectral calculus: for a self-adjoint operator $T$ with PVM $E_{T}$ and $x \in D (T)$ , $∥ (T - a) x ∥^{2} = \int (λ - a)^{2} d E_{T}^{x} (λ)$ ; for bounded Borel $h$ the operator $h (T)$ is bounded with $∥ h (T) x ∥^{2} = \int ∣ h ∣^{2} d E_{T}^{x}$ ; if additionally $\int ∣ h - h (λ_{0}) ∣^{2} d E_{T}^{x} = 0$ then $h (T) x = h (λ_{0}) x$ ; and $U_{T} (t) = e^{- i t T / ℏ}$ is a strongly continuous unitary group expressed by the functional calculus (Spectral theorem for unbounded self-adjoint operators (PVM form), Unbounded Borel functional calculus: domains, products, spectral mapping, Projection valued measure, Integral of a measurable function against a projection-valued measure, A self-adjoint operator generates a strongly continuous unitary group).

[F4] A nonnegative measurable function has zero integral exactly when it vanishes almost everywhere w.r.t. the measure (A nonnegative measurable function has integral $0$ exactly when it vanishes almost everywhere).

[F5] $∣ e^{i α} - e^{i β} ∣^{2} = 2 - 2 \cos (α - β)$ and $∣ e^{i α} ∣ = 1$ ( $\exp (x + i y) = e^{x} (\cos y + i \sin y)$ , $∣ \exp (x + i y) ∣ = e^{x}$ , and $e^{i π} + 1 = 0$ , The derivatives of sine and cosine are cosine and minus sine).

[F6] $G_{β}$ is bounded self-adjoint, $G_{β} = ⨁_{n \in N} e^{- β ω n} i d$ on the Fock sectors, $Z (β) = 1 / (1 - e^{- β ω})$ , and $ρ_{β} = G_{β} / Z (β)$ (Single-mode thermal trace (a), (b), (d)).

[F7] Limits at $+ \infty$ : if a function has a limit then every sequence tending to $+ \infty$ has that limit (Limits at $+ \infty$ and $- \infty$ , and infinite limits at a point).

1.1F1F3F4algebra

[ $U (t)$ on eigenstates] For $n \in N$ the vector $e_{n}$ satisfies $N e_{n} = n e_{n}$ by [F1], hence $A e_{n} = ω n e_{n}$ ; by [F3] with $T = A$ , $a = ω n$ and $x = e_{n}$ , $\int (λ - ω n)^{2} d E^{e_{n}} = 0$ with a nonnegative integrand, so by [F4] the measure $E^{e_{n}}$ gives full mass to ${ω n}$ . Applying [F3] to the bounded Borel function $h_{n} (λ) : = e^{- i t λ / ℏ}$ and $λ_{0} = ω n$ gives $∥ h_{n} (A) e_{n} - e^{- i t ω n / ℏ} e_{n} ∥^{2} = \int ∣ h_{n} - h_{n} (ω n) ∣^{2} d E^{e_{n}} = 0$ ; hence $U (t) e_{n} = h_{n} (A) e_{n} = e^{- i t ω n / ℏ} e_{n}$ . For $n \in {0, 1}$ this gives $U (t) e_{0} = e_{0}$ and $U (t) e_{1} = e^{- i θ} e_{1}$ , so by linearity $ψ (t) = (e_{0} + e^{- i θ} e_{1}) / \sqrt{2}$ , which is (a); also $∥ ψ_{0} ∥^{2} = (∥ e_{0} ∥^{2} + ∥ e_{1} ∥^{2}) / 2 = 1$ .

2.1F2F5step 1.1algebra

[The expectation] By [F2], $Y e_{0} = A_{+} (1) e_{0} = e_{1}$ and $Y e_{1} = A_{-} (1) e_{1} + A_{+} (1) e_{1} = e_{0} + \sqrt{2} e_{2}$ , so $Y$ maps $span {e_{0}, e_{1}}$ into $span {e_{0}, e_{1}, e_{2}}$ ; since $e_{0}, e_{1} \in D (A_{+} (1)) \cap D (A_{-} (1))$ by the operator equalities in [F2] and both domains are linear subspaces, both $ψ (t)$ and $Y ψ (t)$ lie in the finite-particle space, and $⟨ ψ (t), Y ψ (t) ⟩$ is well-defined. With $Y ψ (t) = \frac{1}{\sqrt{2}} (e_{1} + e^{- i θ} e_{0} + \sqrt{2} e^{- i θ} e_{2})$ , orthonormality of $(e_{0}, e_{1}, e_{2})$ and linearity in the first argument give $⟨ ψ (t), Y ψ (t) ⟩ = \frac{1}{2} (⟨ e_{0}, e_{1} ⟩ + e^{i θ} ⟨ e_{0}, e_{0} ⟩ + e^{- i θ} ⟨ e_{1}, e_{1} ⟩) = \frac{1}{2} (e^{i θ} + e^{- i θ}) = \cos θ$ .

2.2F2F6step 1.1algebra

[The stationary thermal weight] By [F6], $G_{β}$ is the direct sum of the scalars $e^{- β ω n}$ on the one-dimensional sectors of $F (C)$ ; since the sector $n$ is spanned by $e_{n}$ , this says $G_{β} e_{n} = e^{- β ω n} e_{n}$ , so $G_{β}$ is diagonal in the complete orthonormal family $(e_{n})$ . By step 1.1, $U (t) G_{β} U (t)^{*} e_{n} = U (t) G_{β} e^{i θ n} e_{n} = e^{i θ n} e^{- β ω n} e^{- i θ n} e_{n} = e^{- β ω n} e_{n} = G_{β} e_{n}$ for every $n$ , $θ n = ω n t / ℏ$ . Both $U (t) G_{β} U (t)^{*}$ and $G_{β}$ are bounded and agree on the complete orthonormal family, hence on its dense span, hence everywhere; dividing by the finite positive scalar $Z (β)$ gives $U (t) ρ_{β} U (t)^{*} = ρ_{β}$ . This is (d).

3.1F5F7step 1.1step 2.1

[Failure of convergence of the expectation and of the state] By step 2.1, $⟨ ψ (t), Y ψ (t) ⟩ = \cos (ω t / ℏ)$ equals $1$ at $t_{n} = 2 π ℏ n / ω$ and $- 1$ at $s_{n} = (2 n + 1) π ℏ / ω$ for every $n$ ; if a limit existed along $t \to + \infty$ , [F7] would give $1 = - 1$ , a contradiction. This is (b). For two times $t, s$ , [F5] gives $∥ ψ (t) - ψ (s) ∥^{2} = \frac{1}{2} ∣ e^{- i ω t / ℏ} - e^{- i ω s / ℏ} ∣^{2} = 1 - \cos (ω (t - s) / ℏ)$ , which equals $2$ for $t = t_{n}$ , $s = s_{n}$ ; hence the family $(ψ (t))$ is not Cauchy at $+ \infty$ and has no limit in norm. This is (c).

4.1step 1.1step 2.1step 3.1step 2.2∎

[Conclusion and scope] Steps 1.1 and 2.1 establish the setting and the expectation $\cos (ω t / ℏ)$ , step 3.1 proves (b) and (c), and step 2.2 proves (d). The scope paragraph of the example records that no physical interpretation of the state, the coupling or the weights is asserted and that relaxation to equilibrium is not derived. This completes the verification.

No automatic equilibration

Example

Verification

Depends on

Dependency tree · 2 levels

Sources