TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-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.

Projector-energy stationarity is equivalent to Fock commutation

Statement

Let $E$ and $F (P) = \nabla E (P)$ be the finite-basis model and gradient of Finite-basis projector energy model. A projector $P \in P_{r}$ is stationary for $E$ restricted to $P_{r}$ —meaning $D E (P) [H] = 0$ for every $H \in T_{P} P_{r}$ —if and only if $[F (P), P] : = F (P) P - P F (P) = 0.$ Stationarity is only a first-order condition; it does not assert that $P$ is a minimum.

Facts & Assumptions

Given: A $C^{2}$ finite-basis projector energy, $P \in P_{r}$ , and the real Frobenius inner product on Hermitian matrices.

[F1]

The Hermitian Frobenius gradient satisfies $D E (P) [H] = tr (F (P) H)$ for Hermitian $H$ (The finite projector energy is real and has the stated Frobenius gradient).

[F2]

The tangent directions at $P$ are exactly $[K, P]$ for skew-Hermitian $K$ , and each is the velocity of a feasible unitary-conjugation curve (Complex projector tangents are skew-Hermitian commutator directions).

Proof

1.1F1F2givenalgebra

Let $K^{*} = - K$ . By [F2], $H_{K} = [K, P]$ is the velocity at zero of a feasible curve through $P$ . The gradient formula [F1] gives $D E (P) [H_{K}] = tr (F (P) (K P - P K))$ . Cyclicity of trace, which follows from $tr (A B) = \sum_{i, j} A_{i j} B_{j i} = tr (B A)$ , rewrites this as $- tr ([F (P), P] K)$ .

2.1F2step 1.1givenalgebra∎

Put $C = [F (P), P]$ . Since $F (P)$ and $P$ are Hermitian, $C^{*} = - C$ . If $P$ is stationary, step 1.1 vanishes for every skew-Hermitian $K$ ; choosing $K = C$ gives $0 = - tr (C^{2}) = tr (C^{*} C) = ∥ C ∥_{F}^{2}$ , so $C = 0$ . Conversely, if $C = 0$ , step 1.1 vanishes for every $K$ , and [F2] says these are all tangent directions, so $P$ is stationary.

Depends on

Used by

Dependency tree · two levels

27 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, ESAIM: Mathematical Modelling and Numerical Analysis 34 (2000), §2.1 and Lemma 2 (standard reference, not scraped)
Alan Edelman, Tomás A. Arias, and Steven T. Smith, The Geometry of Algorithms with Orthogonality Constraints, SIAM Journal on Matrix Analysis and Applications 20 (1998), §§2.3.2 and 2.5 (standard reference, not scraped)