LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Closed formulas for the two-level canonical weights, mean energy, entropy and free energy

Statement

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $ε > 0$ and $β > 0$ be real parameters, let $h$ be a two-dimensional complex Hilbert space with orthonormal basis $(u_{0}, u_{1})$ (Hilbert space, Orthonormal families, complete orthonormal systems and Hilbert bases), and let $H : = T_{u_{1}, u_{1}} ε = ε T_{u_{1}, u_{1}}$ be the self-adjoint operator with eigenvalues $0$ on $C u_{0}$ and $ε$ on $C u_{1}$ (Rank-one operator calculus). Let $Z : = \sum_{j = 0}^{1} e^{- β E_{j}}, ρ_{β} : = \frac{1}{Z} \sum_{j = 0}^{1} e^{- β E_{j}} T_{u_{j}, u_{j}}, s (ρ) : = - \sum_{i : w_{i} > 0} w_{i} \log w_{i}$ be the partition sum, canonical operator and entropy of Finite Gibbs free-energy minimum clause (a), with $E_{0} = 0$ , $E_{1} = ε$ and $w_{i}$ the eigenvalues of a density operator $ρ$ on $h$ (The natural logarithm as the inverse of the exponential function). Then:

(a) $Z = 1 + e^{- β ε} \in (1, 2)$ , and $ρ_{β} = \frac{1}{Z} (T_{u_{0}, u_{0}} + e^{- β ε} T_{u_{1}, u_{1}})$ is a density operator on $h$ that is not the maximally mixed state $\frac{1}{2} i d$ ;

(b) the mean energy is the exact identity $tr (ρ_{β} H) = \frac{ε e^{- β ε}}{Z} = \frac{ε}{e^{β ε} + 1}, 0 < tr (ρ_{β} H) < \frac{ε}{2};$

(c) the entropy and free energy satisfy $s (ρ_{β}) = \log Z + \frac{β ε}{e^{β ε} + 1} = \log (1 + e^{- β ε}) + \frac{β ε e^{- β ε}}{1 + e^{- β ε}}, 0 \leq s (ρ_{β}) < \log 2,$ and, with $F : = - β^{- 1} \log Z$ , $tr (ρ_{β} H) - β^{- 1} s (ρ_{β}) = F;$

(d) scope: clauses (a)-(c) are exact algebraic identities for the declared two-dimensional Hilbert space and the two real parameters $ε, β > 0$ ; no temperature, thermodynamic, equilibrium or measurement interpretation is asserted, and the parameter $β$ carries no physical dimension in this lemma.

Facts & Assumptions

Given: the real parameters $ε > 0$ , $β > 0$ , the two-dimensional complex Hilbert space $h$ with orthonormal basis $(u_{0}, u_{1})$ , the operator $H = ε T_{u_{1}, u_{1}}$ , and the data $Z$ , $ρ_{β}$ , $s$ of the statement.

[F1]

Supplied finite Gibbs data. For the finite-dimensional self-adjoint $H$ with real eigenvalues $E_{1}, \dots, E_{d}$ and orthonormal eigenbasis $(v_{1}, \dots, v_{d})$ , and $β > 0$ , one has $Z = \sum_{j} e^{- β E_{j}} \in (0, \infty)$ and $ρ_{β} = Z^{- 1} \sum_{j} e^{- β E_{j}} T_{v_{j}, v_{j}} \in D$ , with $tr (ρ_{β} H) = Z^{- 1} \sum_{j} e^{- β E_{j}} E_{j}$ , $tr (ρ_{β} H) - β^{- 1} s (ρ_{β}) = - β^{- 1} \log Z$ , and for every density operator $ρ$ one has $s (ρ) \leq \log d$ , with equality if and only if $ρ = d^{- 1} i d$ (Finite Gibbs free-energy minimum clauses (a), (b), (c)).

[F2]

Rank-one calculus. $T_{u, v} x = ⟨ x, v ⟩ u$ is bounded with $T_{u, v}^{*} = T_{v, u}$ , $T_{x, x} \geq 0$ , $tr (T_{u, v}) = ⟨ u, v ⟩$ , and for bounded $B$ one has $B T_{u, v} = T_{B u, v}$ and $T_{u, v} B = T_{u, B^{*} v}$ (Rank-one operator calculus clauses (a)-(d)); the trace is linear (Trace is a linear functional on $M_{n} (F)$ ) and $tr (X Y) = tr (Y X)$ (Cyclicity of the trace).

[F3]

Real exponential. $\exp (x) > 0$ , $\exp (- x) = 1 / \exp (x)$ , and $\exp (x + y) = \exp (x) \exp (y)$ for all real $x, y$ (The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ , The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ ); $\exp$ is strictly increasing on $R$ (The exponential function is strictly increasing). Hence $\exp (0) = \exp (0)^{2}$ with $\exp (0) > 0$ , so $\exp (0) = 1$ , and $\exp (t) > \exp (0) = 1$ for every $t > 0$ .

[F4]

Logarithm. $\log : (0, \infty) \to R$ is the inverse function of $\exp$ and satisfies $\log (x y) = \log x + \log y$ , $\log (1 / x) = - \log x$ and $\log 1 = 0$ (The natural logarithm as the inverse of the exponential function, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

Proof

technique · direct; instantiate the supplied finite Gibbs formulas at the two eigenvalues $0,\varepsilon$, and control the exponential factor at $\beta\varepsilon>0$ with strict increase, positivity and the reciprocal law

Given: the data of the statement and [F1]-[F4].

1.1F3algebra

[Exponential comparison] Since $β ε > 0$ , strict increase in [F3] gives $\exp (β ε) > \exp (0) = 1$ , and [F3] gives $\exp (- β ε) = 1 / \exp (β ε) \in (0, 1)$ ; consequently $1 < Z = 1 + \exp (- β ε) < 2$ .

2.1F1step 1.1algebra

[The canonical operator] By [F1] with $E_{0} = 0$ , $E_{1} = ε$ and $(v_{1}, v_{2}) = (u_{0}, u_{1})$ , $Z = 1 + e^{- β ε}$ and $ρ_{β} = Z^{- 1} (T_{u_{0}, u_{0}} + e^{- β ε} T_{u_{1}, u_{1}}) \in D$ , so $ρ_{β}$ is a density operator; its two weights are $Z^{- 1}$ and $e^{- β ε} Z^{- 1}$ , which are distinct because $\exp (- β ε) \neq 1$ by step 1.1.

3.1F1F2F4step 1.1step 2.1algebra

[Mean energy, entropy and free energy] Using [F2] and $T_{u_{0}, u_{0}} T_{u_{1}, u_{1}} = ⟨ u_{1}, u_{0} ⟩ T_{u_{0}, u_{1}} = 0$ by orthogonality, and $T_{u_{1}, u_{1}} T_{u_{1}, u_{1}} = T_{u_{1}, u_{1}}$ with $⟨ u_{1}, u_{1} ⟩ = 1$ , the product $ρ_{β} H$ equals $ε e^{- β ε} Z^{- 1} T_{u_{1}, u_{1}}$ , so [F2] gives $tr (ρ_{β} H) = ε e^{- β ε} / Z$ ; by step 1.1, $e^{- β ε} / Z = e^{- β ε} / (1 + e^{- β ε}) = 1 / (e^{β ε} + 1)$ , hence $tr (ρ_{β} H) = ε / (e^{β ε} + 1)$ lies in $(0, ε / 2)$ . By [F1], $tr (ρ_{β} H) - β^{- 1} s (ρ_{β}) = - β^{- 1} \log Z$ , so $s (ρ_{β}) = \log Z + β tr (ρ_{β} H) = \log (1 + e^{- β ε}) + β ε / (e^{β ε} + 1) = \log (1 + e^{- β ε}) + β ε e^{- β ε} / (1 + e^{- β ε})$ ; by [F1] and [F2], $0 \leq s (ρ_{β}) < \log 2$ because $ρ_{β} \neq \frac{1}{2} i d$ by step 2.1. Finally $tr (ρ_{β} H) - β^{- 1} s (ρ_{β}) = - β^{- 1} \log Z = F$ with $F$ as defined. This proves (b) and (c), and step 2.1 proved (a).

4.1step 1.1step 2.1step 3.1∎

[Conclusion] Steps 1.1-2.1 prove (a), step 3.1 proves (b) and (c), and every identity is an algebraic consequence of the supplied finite-dimensional formulas and the real exponential and logarithm laws, which is (d).

Remarks

High- and low-temperature expectations. By [F3], $0 < e^{- β ε} < 1$ and $e^{- β ε}$ decreases strictly as the product $β ε$ grows, so the upper level is suppressed in the regime of large $β ε$ , while the bound $s < \log 2$ of clause (c) shows that the entropy stays below the maximal mixed-state value for every finite $β > 0$ . The lemma asserts only these algebraic facts about the weights; it identifies no physical temperature with $β$ .
Use. The formulas are the exact two-level data used by the examples and the thought experiment of the companion page; the physical reading of $β$ as an inverse temperature, and of $ρ_{β}$ as a thermal preparation, is supplied separately by the framework's equilibrium postulate.

Closed formulas for the two-level canonical weights, mean energy, entropy and free energy

Statement

Facts & Assumptions

Proof

Remarks

Depends on

Dependency tree · 2 levels

Sources