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

Every rank-r orthogonal projector is an admissible density

Statement

Every $P \in P_{r}$ belongs to the admissible density domain $D_{r}$ .

Facts & Assumptions

Given: $P \in H_{n}$ satisfies $P = P^{*}$ , $P^{2} = P$ , and $tr P = r$ , where $1 \leq r < n$ .

[F1]

The rank- $r$ projector set is $P_{r} = {P = P^{*} : P^{2} = P, tr P = r}$ (Rank-r orthogonal projector domain).

[F2]

A finite-dimensional Hermitian matrix has an orthonormal eigenbasis and real eigenvalues (Complex spectral theorem: a normal endomorphism of a finite-dimensional complex inner product space has an orthonormal eigenbasis, and conversely).

[F3]

The admissible domain consists of Hermitian positive contractions of trace $r$ (The fixed-particle admissible Hermitian density domain).

Proof

1.1givenF1F2algebra

By [F2], choose a unitary eigenbasis of $P$ with real eigenvalues $μ_{j}$ . From $P^{2} = P$ , each satisfies $μ_{j}^{2} = μ_{j}$ , hence $μ_{j} \in {0, 1}$ . Therefore every eigenvalue lies between $0$ and $1$ , so for each $x$ the quadratic forms $x^{*} P x$ and $x^{*} (I - P) x$ are nonnegative.

2.1step 1.1F1F3∎

The matrix $P$ is Hermitian and has trace $r$ by [F1]; step 1.1 gives $0 ⪯ P ⪯ I$ . These are exactly the conditions in [F3], so $P \in D_{r}$ .

Depends on

Used by

Cited to discharge well-definedness by The fixed-particle admissible Hermitian density domain.

Dependency tree · two levels

11 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

Eric Cancès, Gaspard Kemlin, and Antoine Levitt, Convergence analysis of direct minimization and self-consistent iterations, §2.1 (standard reference, not scraped)
Eric Cancès and Claude Le Bris, On the convergence of SCF algorithms for the Hartree-Fock equations, §2.1 (standard reference, not scraped)