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 finite-basis occupied projector map can two-cycle despite a uniform gap

Example

Take $n = 2$ , $r = 1$ , overlap $S = I_{2}$ , Cholesky factor $L = I_{2}$ , $h = 0$ , and $E_{x c} = 0$ in Finite-basis projector energy model. Define $G : H_{2} \to H_{2}$ by $G (X) = diag (X_{11}, X_{22})$ . Here matrix-entry labels $1, 2$ mean the first and second rows/columns, corresponding to canonical indices $0, 1$ . The associated response map is $F (P) = G (P)$ . Let $P_{0} = (\begin{array}{cc} 1 & 0 \\ 0 & 0 \end{array}), P_{1} = (\begin{array}{cc} 0 & 0 \\ 0 & 1 \end{array}) .$ For the undamped occupied-projector iteration, $P_{0}$ and $P_{1}$ form a strict two-cycle even though the occupied/unoccupied eigenvalue gap equals $1$ at both iterates.

Facts & Assumptions

Given: The finite-basis model data above, the rank-one projectors $P_{0}, P_{1}$ , and $Φ (P)$ equal to the projector onto the lowest eigenvalue of $F (P)$ whenever the gap is positive.

[F1]

The finite-basis model permits Hermitian $h$ , real-linear self-adjoint $G$ , and real $C^{2}$ $E_{x c}$ , with $F (P) = h + G (P) + \nabla E_{x c} (P)$ (Finite-basis projector energy model).

[F2]

The occupied projector is selected from the $r$ lowest eigenvalues when a strict gap is present (The occupied-projector response map on its strict-gap domain).

[F3]

The undamped update is $P_{k + 1} = Φ (P_{k})$ and checks the gap before updating (Finite-budget undamped self-consistent projector iteration).

[F4]

A strict gap makes the selected occupied projector unique (A strict occupied gap defines a unique rank-r spectral projector).

[F5]

The exact diagonal eigensolver returns the ordered eigenvalues and occupied projector of each displayed diagonal matrix.

Verification

1.1givenF1algebra

For Hermitian $X, Y$ , the diagonal entries are real and $⟨ G (X), Y ⟩_{F} = X_{11} Y_{11} + X_{22} Y_{22} = ⟨ X, G (Y) ⟩_{F} .$ Thus $G$ is real-linear, Hermitian-valued, and self-adjoint for the Frobenius inner product, so the stated data satisfy [F1]. Each $P_{i}$ is Hermitian, idempotent, and has trace $1$ , hence lies in $P_{1}$ .

1.2givenF2F4F5algebra

Direct substitution gives $F (P_{0}) = diag (1, 0)$ and $F (P_{1}) = diag (0, 1)$ . Each matrix has eigenvalues $0 < 1$ , so the strict occupied gap is $1$ by [F5]. By [F2], the lowest eigenspace of $F (P_{0})$ is $span {(0, 1)^{T}}$ and that of $F (P_{1})$ is $span {(1, 0)^{T}}$ ; [F4] guarantees these give the unique projectors $Φ (P_{0}) = P_{1}$ and $Φ (P_{1}) = P_{0}$ . Thus $K = {P_{0}, P_{1}}$ is invariant.

2.1step 1.2F3algebra∎

By [F3], starting at $P_{0}$ yields $P_{0}, P_{1}, P_{0}, P_{1}, \dots$ . Since $∥ P_{0} - P_{1} ∥_{F} = \sqrt{2} > 0$ , this sequence does not converge. Thus a positive uniform gap at the iterates alone does not imply convergence.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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 and Claude Le Bris, On the convergence of SCF algorithms for the Hartree-Fock equations, §2.2 and Example 9 (standard reference, not scraped)