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

The finite projector energy is real and has the stated Frobenius gradient

Statement

For the data of Finite-basis projector energy model, $E (P)$ is real and $C^{2}$ on its stated neighborhood. For every Hermitian $P$ in that neighborhood and every Hermitian direction $H$ , $D E (P) [H] = tr ((h + G (P) + \nabla E_{x c} (P)) H) = ⟨ F (P), H ⟩_{F} .$ Thus $F (P)$ is the Hermitian Frobenius gradient of $E$ .

Facts & Assumptions

Given: Hermitian $h, P, H$ , a real-linear self-adjoint map $G$ on $H_{n}$ , and a real $C^{2}$ functional $E_{x c}$ on an open neighborhood of $P$ .

[F1]

Trace and Frobenius-linear functionals differentiate by their linear increments (Trace and Frobenius-linear matrix functionals differentiate by inspection).

[F2]

Matrix differentials obey the sum, product, and adjoint rules (Matrix differentials obey the sum rule, product rule, and adjoint rule).

[F3]

In the projector energy model, $G$ is real-linear and self-adjoint and $E_{x c}$ has its Frobenius gradient (Finite-basis projector energy model).

[F4]

For conformable matrices over a field, $tr (A B) = tr (B A)$ (For $A \in M_{m \times n} (F)$ and $B \in M_{n \times m} (F)$ , $tr (A B) = tr (B A)$ ).

Proof

1.1F2F3F4givenalgebra

If $A, B$ are Hermitian, then $\overline{tr (A B)} = tr ((A B)^{*}) = tr (B A) = tr (A B)$ by the trace identity [F4]. Hence $tr (h P)$ and $tr (P G (P))$ are real; $E_{x c}$ is real by [F3]. The first two terms are polynomial in the real coordinates of $P$ , so together with the $C^{2}$ term they give a real $C^{2}$ function.

1.2F1F2F3givenalgebra

For real $t$ , real-linearity gives $G (P + t H) = G (P) + t G (H)$ . Expanding and collecting the coefficient of $t$ yields ${\frac{d}{d t} ∣}_{t = 0} \frac{1}{2} tr ((P + t H) G (P + t H)) = \frac{1}{2} tr (H G (P)) + \frac{1}{2} tr (P G (H))$ . The linear trace term differentiates to $tr (h H)$ by [F1], and the $E_{x c}$ term differentiates to $⟨ \nabla E_{x c} (P), H ⟩_{F}$ by its gradient definition.

2.1F1F3step 1.1step 1.2algebra∎

Self-adjointness of $G$ gives $tr (P G (H)) = ⟨ P, G (H) ⟩_{F} = ⟨ G (P), H ⟩_{F} = tr (G (P) H)$ . Since these traces are real, the two quadratic contributions in step 1.2 combine to $tr (G (P) H)$ . Adding the other derivatives gives $D E (P) [H] = ⟨ h + G (P) + \nabla E_{x c} (P), H ⟩_{F}$ . This is the unique Frobenius gradient pairing, so it equals $⟨ F (P), H ⟩_{F}$ .

Depends on

Used by

Cited to discharge well-definedness by Finite-basis projector energy model.

Dependency tree · two levels

17 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 (standard reference, not scraped)
Alan Edelman and Steven G. Johnson, Matrix Calculus for Machine Learning and Beyond, MIT OpenCourseWare, Lecture 1 (standard reference, not scraped)