LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge 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.

A finite-temperature minimizer has strictly interior occupations

Statement

Assume $E$ in the model of Fixed-particle finite-temperature density-matrix free energy is $C^{1}$ on an open neighborhood of $D_{r}$ , with $0 < r < n$ and $β > 0$ . Every global minimizer $D$ of $F_{β}$ satisfies $0 ≺ D ≺ I$ ; equivalently, each eigenvalue of $D$ lies strictly between $0$ and $1$ .

Facts & Assumptions

Given: A global minimizer $D \in D_{r}$ , a $C^{1}$ energy on a neighborhood of the compact density domain, $0 < r < n$ , and $β > 0$ .

[F1]

The density domain fixes $tr D = r$ and the entropy is $tr ϕ (D)$ (Fixed-particle finite-temperature density-matrix free energy).

[F2]

The eigenvalues of a Hermitian $D$ lie in $[0, 1]$ exactly when $0 ⪯ D ⪯ I$ (Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely).

[F3]

For $0 < x < 1$ , $ϕ^{'} (x) = \log x - \log (1 - x)$ and the endpoint behavior follows from $x \log x \to 0$ (The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t, The finite-temperature trace entropy is continuous at occupation endpoints).

[F4]

A differentiable scalar function with bounded derivative on a short interval changes by at most that derivative bound times the interval length (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

Proof

1.1F1F2F3F4givenalgebra

Diagonalize $D$ by [F2], with eigenvalues $d_{j} \in [0, 1]$ and $\sum_{j} d_{j} = r$ . If $d_{i} = 0$ , then $r > 0$ gives an index $j$ with $d_{j} > 0$ . For small $t > 0$ , $D_{t} = D + t (e_{i} e_{i}^{*} - e_{j} e_{j}^{*})$ remains in $D_{r}$ . If $d_{j} \in (0, 1)$ , $ϕ^{'}$ is bounded near $d_{j}$ , so [F4] gives $ϕ (d_{j} - t) - ϕ (d_{j}) = O (t)$ . Also $(1 - t) \log (1 - t) = O (t)$ because this scalar function is differentiable at $0$ . Thus the entropy change is $ϕ (t) + ϕ (d_{j} - t) - ϕ (0) - ϕ (d_{j}) = t \log t + O (t)$ by [F3]. If $d_{j} = 1$ , it is $ϕ (t) + ϕ (1 - t) = 2 t \log t + O (t)$ by $ϕ (1 - t) = ϕ (t)$ . The energy change is $O (t)$ by Fréchet differentiability of $E$ at $D$ along the fixed direction $e_{i} e_{i}^{*} - e_{j} e_{j}^{*}$ . Dividing the total free-energy change by $t$ gives $β^{- 1} \log t + O (1)$ (or $2 β^{- 1} \log t + O (1)$ ), which is negative for sufficiently small $t$ . This contradicts minimality.

2.1F1F2F3F4givenstep 1.1algebra∎

If $d_{i} = 1$ , then $r < n$ gives $j$ with $d_{j} < 1$ . Transfer $t$ from the $i$ th eigendirection to the $j$ th: $D_{t} = D + t (e_{j} e_{j}^{*} - e_{i} e_{i}^{*})$ . If $d_{j} \in (0, 1)$ , the term that leaves the endpoint $1$ is $ϕ (1 - t) = ϕ (t) = t \log t + O (t)$ and the interior term changes by $O (t)$ by [F4]. If $d_{j} = 0$ , the two endpoint terms change by $2 ϕ (t) = 2 t \log t + O (t)$ . The energy change is $O (t)$ by differentiability as in step 1.1. Dividing by $t$ again gives a negative free-energy change for small $t$ , contradicting minimality. No eigenvalue can equal $0$ or $1$ , proving the claim.

Depends on

Used by

Interior finite-temperature stationarity gives Fermi-Dirac occupations Theorem

Dependency tree · two levels

33 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Daniel Arovas, Thermodynamics and Statistical Mechanics, §7.4 Variational Density Matrix Method, UC San Diego / Physics LibreTexts (standard reference, not scraped)