Alphabeta Math
TheoremStatement: AI-adaptedProof: Literature-sourced
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.

Imported positive eigenpairs for a smooth closed elliptic operator

Statement

Let L=−Δh+2t⋅∇+c have the closed connected smooth Riemannian and real smooth coefficient hypotheses of the formal-adjoint lemma. There exist a real eigenvalue λ, a smooth real ϕ>0 with Lϕ=λϕ, and a smooth real χ>0 with L†χ=λχ. This is an established external existence input, not a locally reconstructed resolvent or Krein–Rutman proof.

Facts & Assumptions

[F1]

The formal-adjoint lemma fixes the exact operator, metric density and adjoint conventions. Formal adjoint of a real drift Laplacian on a closed manifold

[A1]

Work in ZFC, including Choice. The Axiom of Choice

External input

Andersson–Mars–Simon §4 Lemma 4.1 applies to the smooth real elliptic operator on the connected compact boundaryless manifold. Apply part (i) also to its formal adjoint, whose coefficients and ellipticity are supplied by the formal-adjoint lemma; part (ii) identifies the principal eigenvalues. We import the resulting positive right and adjoint eigenpairs. No local compact-resolvent construction or proof of Krein–Rutman is claimed.

Depends on

Used by · 1

Dependency tree · 2 levels

Each result is drawn at its shortest distance from this item. Arrows run from prerequisites to the items that use them; this item has a heavier outline. External source nodes link directly to the cited text. The view shows up to two dependency steps; open a prerequisite to continue.

External dependencies

Lars Andersson, Marc Mars and Walter Simon, Stability of marginally outer trapped surfaces and existence of marginally outer trapped tubes · §4, equation (10), standing hypotheses and Lemma 4.1(i)–(ii), printed p.9

On a connected compact smooth manifold without boundary, a real smooth elliptic operator L=-Delta_h+2t^A D_A+c has a real eigenvalue with a smooth everywhere positive eigenfunction, unique up to scale, minimal real part among eigenvalues. Its L2 adjoint has the same principal eigenvalue, with a positive principal eigenfunction by applying (i) to the adjoint.

Hypotheses: Positive dimension; connected compact smooth manifold without boundary; smooth positive-definite Riemannian h and smooth real drift t and zeroth-order coefficient c; no sign hypothesis on c, no energy condition and no selfadjointness assumption. Adjoint is with respect to the Riemannian L2 measure.

Reading limits: Downloaded the complete arXiv PDF; read §4 standing hypotheses and Lemma 4.1 on printed p.9 as text and rendered PDF, its surrounding explanation on p.10, and Appendix B pp.29–30 as extracted text. The existence theorem is imported, not locally reconstructed or proof-reviewed. Local helper arguments independently supply the quotient identities and adjoint pairing actually used here.

Sources