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

A convex density mixture can be admissible without being a projector

Example

In dimension $2$ with particle number $r = 1$ , let $F (X) = diag (0, 1)$ on $U = H_{2}$ and start from $P_{0} = diag (0, 1)$ . Its response projector is $P_{1} = diag (1, 0)$ , and mix with $α = 1 / 2$ .

Facts & Assumptions

Given: The constant Hermitian response $F (X) = diag (0, 1)$ , $P_{0} = diag (0, 1)$ , and $α = 1 / 2$ .

[F1]

Every rank- $r$ orthogonal projector is an admissible density (Every rank-r orthogonal projector is an admissible density).

[F2]

A strict gap defines a unique occupied response projector (The occupied-projector response map on its strict-gap domain, A strict occupied gap defines a unique rank-r spectral projector).

[F3]

Mixing an admissible density with the defined rank- $r$ response projector remains in $D_{r}$ (Density mixing preserves admissibility but need not preserve idempotence).

Verification

1.1givenF1F2algebra

The matrix $P_{0}$ is a Hermitian idempotent of trace $1$ , so $P_{0} \in P_{1}$ and $P_{0} \in D_{1}$ by [F1]. The constant response matrix has eigenvalues $0 < 1$ , so [F2] gives $Φ (P_{0}) = P_{1} = diag (1, 0)$ .

2.1step 1.1givenF3algebra

Direct calculation gives $D = (1 - α) P_{0} + α Φ (P_{0}) = \frac{1}{2} I_{2}$ . By [F3], $D \in D_{1}$ ; explicitly it is Hermitian, satisfies $0 ⪯ D ⪯ I_{2}$ , and has trace $1$ .

3.1step 2.1algebra∎

But $D^{2} = \frac{1}{4} I_{2} \neq D$ , so $D$ is not idempotent and hence $D \notin P_{1}$ . This verifies that relaxed density iterates must not be silently identified with projectors.

Depends on

Used by

Nothing in the library uses this result yet.

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, §4.4 (standard reference, not scraped)