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.

A positive tangent Hessian gives a strict local projector minimum

Statement

Let $P_{0} \in P_{r}$ be stationary for the $C^{2}$ energy $E$ of Finite-basis projector energy model. Use its graph chart $P (X)$ from Graph charts and tangent directions for complex rank-r projectors, with $P (0) = P_{0}$ , and put $ψ (X) = E (P (X))$ . If there is $c > 0$ such that $D^{2} ψ (0) [X, X] \geq c ∥ X ∥_{F}^{2} for every X : U \to U^{⊥},$ then $P_{0}$ is a strict isolated local minimum on $P_{r}$ . Since projectors identify frames related by unitary rotations, this is a strict local minimum modulo orbital gauge. This is a sufficient condition, not a claim that every stationary point satisfies it.

Facts & Assumptions

Given: A $C^{2}$ energy on $P_{r}$ , a stationary projector $P_{0}$ , its graph chart, and a positive lower bound $c$ for the chart Hessian.

[F1]

Stationarity on $P_{r}$ is the vanishing of the derivative on every tangent direction (Projector-energy stationarity is equivalent to Fock commutation).

[F2]

The graph map $X \mapsto P (X)$ is a smooth one-to-one coordinate chart near $P_{0}$ ; frames differing by a unitary represent the same projector (Graph charts and tangent directions for complex rank-r projectors).

[F3]

The fundamental theorem of calculus differentiates an integral of a continuous function (The first fundamental theorem: if $f$ is integrable on $[a, b]$ and continuous at $c$ , then $F^{'} (c) = f (c)$ ; in particular a continuous $f$ has $F$ as a primitive); applying it twice gives the second-order integral remainder used below.

Proof

1.1F1F2given

The derivative of $ψ$ at $0$ is $D ψ (0) [X] = D E (P_{0}) [D P (0) [X]]$ . The chart differential is tangent by [F2], so stationarity [F1] makes this derivative zero for every $X$ .

2.1F2F3givenstep 1.1algebra

By the assumed Hessian bound and continuity of $D^{2} ψ$ , there is a neighborhood of $0$ in which $D^{2} ψ (Y) [X, X] \geq (c / 2) ∥ X ∥_{F}^{2}$ for every $X$ . For $X$ in this neighborhood, the one-variable fundamental theorem of calculus [F3] applied twice to $t \mapsto ψ (t X)$ gives $ψ (X) - ψ (0) - D ψ (0) [X] = \int_{0}^{1} (1 - t) D^{2} ψ (t X) [X, X] d t \geq \frac{c}{4} ∥ X ∥_{F}^{2}$ . By step 1.1 this is positive for every nonzero $X$ .

3.1F2step 2.1∎

The graph chart is one-to-one and maps an open neighborhood of $0$ onto a neighborhood of $P_{0}$ in projector space by [F2]. Step 2.1 therefore proves that every distinct nearby projector has strictly larger energy. Projectors represent unitary-equivalence classes of occupied frames, so the same statement is strict local minimality modulo orbital gauge.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

40 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

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.5 (standard reference, not scraped)
P.-A. Absil, R. Mahony, and R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Chapter 3, Princeton University Press (2008), §§3.4.4 and 3.5.7 (standard reference, not scraped)