ExampleConstruction: AI-adaptedVerification: 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.

Attractive contact energy

Example

Assume the Axiom of Choice and Countable Choice (The Axiom of Choice, The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $A_{- 1}$ be the delta interface operator of The one-dimensional delta interface operator with $α = - 1$ : $D (A_{- 1}) = {u \in H^{1} (R) : u ∣_{(0, \infty)}, u ∣_{(- \infty, 0)} \in H^{2}, u^{' *} (0 +) - u^{' *} (0 -) = - u^{*} (0)},$ and put $ψ (x) : = \frac{1}{\sqrt{2}} e^{- ∣ x ∣ / 2}, ∣ ψ (x) ∣^{2} = \frac{1}{2} e^{- ∣ x ∣} .$ Then:

(a) $ψ \in D (A_{- 1})$ , $∥ ψ ∥_{L^{2} (R)} = 1$ , and $A_{- 1} ψ = - \frac{1}{4} ψ$ ; the negative eigenvalue $- \frac{1}{4}$ is the only negative eigenvalue of $A_{- 1}$ and its eigenspace is $C ψ$ ;

(b) more generally, for every $α < 0$ the operator $A_{α}$ has the single negative eigenvalue $- α^{2} / 4$ with normalized eigenvector $\sqrt{- α / 2} e^{α ∣ x ∣ / 2}$ , and for $α \geq 0$ there is none (The unique negative eigenvalue of the attractive delta interface operator);

(c) if $α < 0$ , with the scaling of part (c) of The unique negative eigenvalue of the attractive delta interface operator, if one assigns positive constants $ℏ, m$ and sets $H : = (ℏ^{2} / 2 m) A_{α}$ and $g : = ℏ^{2} α / (2 m)$ , then the bound energy is $- m g^{2} / (2 ℏ^{2})$ ; for the case $α = - 1$ this is $E_{H} = - ℏ^{2} / (8 m)$ .

Verification

Given: the delta interface operator $A_{- 1}$ with $α = - 1$ and the function $ψ (x) = 2^{- 1 / 2} e^{- ∣ x ∣ / 2}$ .

Proof technique: direct verification of the interface conditions and the eigenvalue equation for the explicit function.

[F1] $u \in D (A_{α})$ means $u \in H^{1} (R)$ with $H^{2}$ restrictions to the half-lines, the interface condition $u^{' *} (0 +) - u^{' *} (0 -) = α u^{*} (0)$ , and $A_{α} u = - D^{2} u$ on each half-line (The one-dimensional delta interface operator).

[F2] The representative of $ψ$ is $C^{\infty}$ on each open half-line with $ψ^{''} (x) = \frac{1}{4} ψ (x)$ there, and $ψ^{' *} (0 +) = - \frac{1}{2} ψ (0)$ , $ψ^{' *} (0 -) = + \frac{1}{2} ψ (0)$ ; these are direct computations from the exponential (The complex exponential by its power series, The exponential function is smooth and $(\exp)^{'} = \exp$ ), and the traces exist by Absolutely continuous representative of an L2 function with L2 weak derivative.

1.1F2algebra

[Normalisation] $\int_{R} ∣ ψ ∣^{2} = \frac{1}{2} \int_{R} e^{- ∣ x ∣} d x = \int_{0}^{\infty} e^{- x} d x = 1$ .

2.1step 1.1F1F2algebra

[Membership and eigenvalue] By [F2], $ψ$ is $H^{1}$ with $H^{2}$ half-line restrictions, and its derivative jump is $ψ^{' *} (0 +) - ψ^{' *} (0 -) = - ψ^{*} (0)$ , so $ψ \in D (A_{- 1})$ by [F1] with $α = - 1$ . On each half-line, $A_{- 1} ψ = - D^{2} ψ = - \frac{1}{4} ψ$ , so $A_{- 1} ψ = - \frac{1}{4} ψ$ . This is the verification of (a) for the explicit function; uniqueness of the negative eigenvalue and of its eigenspace is part (b) of The unique negative eigenvalue of the attractive delta interface operator, specialised to $α = - 1$ : $- α^{2} / 4 = - 1 / 4$ and $\sqrt{- α / 2} = \sqrt{1 / 2}$ .

3.1step 2.1∎

[The general and scaled statements] Part (b) is exactly The unique negative eigenvalue of the attractive delta interface operator (b), and part (c) is its (c): for $α < 0$ , $E_{H} = - ℏ^{2} α^{2} / (8 m) = - m g^{2} / (2 ℏ^{2})$ with $g = ℏ^{2} α / (2 m)$ , and at $α = - 1$ this equals $- ℏ^{2} / (8 m)$ .

Attractive contact energy

Example

Verification

Depends on

Dependency tree · 2 levels

Sources