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 two-level nonlinear projector model has a stationary strict maximum

Example

In $C^{2}$ with $r = 1$ , let $H = diag (1, - 1)$ , $h = 0$ , $E_{x c} = 0$ , and define $G (A) = 2 tr (H A) H$ on Hermitian $A$ . Then $G$ is a self-adjoint real-linear map, so it defines the allowed nonlinear projector energy $E (P) = tr (H P)^{2}$ . At $P_{0} = e_{1} e_{1}^{*}$ the commutator stationarity condition holds, but $P_{0}$ is a strict local maximum, not a minimum.

Facts & Assumptions

Given: $n = 2$ , $r = 1$ , $H = diag (1, - 1)$ , $h = 0$ , $E_{x c} = 0$ , and $G (A) = 2 tr (H A) H$ .

[F1]

A rank-one orthogonal projector has the form $u u^{*}$ for a unit vector $u$ (Rank-r orthogonal projector domain).

[F2]

The energy gradient is $F (P) = h + G (P) + \nabla E_{x c} (P)$ (Finite-basis projector energy model, The finite projector energy is real and has the stated Frobenius gradient).

[F3]

A projector is stationary exactly when it commutes with its model gradient (Projector-energy stationarity is equivalent to Fock commutation).

Verification

1.1F2givenalgebra

For Hermitian $A, B$ , $tr (H A)$ and $tr (H B)$ are real, and $⟨ G (A), B ⟩_{F} = 2 tr (H A) tr (H B) = ⟨ A, G (B) ⟩_{F}$ . Thus $G$ is self-adjoint and real-linear; the model's quadratic term is $\frac{1}{2} tr (P G (P)) = tr (H P)^{2}$ .

2.1F1step 1.1algebra

For an arbitrary unit vector $u = (u_{1}, u_{2}) \in C^{2}$ , put $s = ∣ u_{2} ∣^{2}$ . Then $P = u u^{*} \in P_{1}$ by [F1], $tr (H P) = ∣ u_{1} ∣^{2} - ∣ u_{2} ∣^{2} = 1 - 2 s$ , and $E (P) = (1 - 2 s)^{2}$ . A neighborhood of $P_{0} = e_{1} e_{1}^{*}$ is given by $0 \leq s < 1 / 2$ ; every distinct projector there has $s > 0$ and hence $(1 - 2 s)^{2} < 1 = E (P_{0})$ . Thus $P_{0}$ is a strict local maximum in the full complex projector domain.

3.1F2F3step 2.1algebra∎

At $P_{0}$ , $F (P_{0}) = G (P_{0}) = 2 H$ , which is diagonal and therefore commutes with $P_{0}$ . By [F3], $P_{0}$ is stationary, while step 2.1 shows it is not a local minimum.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

16 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.