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

Formal nonnormalizable solution

Example

Assume the Axiom of Countable Choice (The Axiom of Countable Choice ( ${A C}_{ω}$ )). Let $g_{0} (y) = π^{- 1 / 4} e^{- y^{2} / 2}$ (Hermite recurrence(a)) and define

$F (y) : = \int_{0}^{y} e^{t^{2}} d t, u_{2} (y) : = e^{- y^{2} / 2} F (y) (y \in R) .$

Then:

(a) $F$ is $C^{1}$ with $F^{'} = e^{y^{2}}$ , and $u_{2}$ is $C^{2}$ and solves the ground-state eigenvalue equation

$u_{2}^{''} (y) = (y^{2} - 1) u_{2} (y) (y \in R),$

which is the equation $(- \partial_{y}^{2} + y^{2}) u = u$ satisfied by $g_{0}$ (Hermite orthogonality(b));

(b) the Wronskian is constant and nonzero,

$W : = g_{0} u_{2}^{'} - g_{0}^{'} u_{2} = π^{- 1 / 4},$

so $g_{0}$ and $u_{2}$ are linearly independent solutions;

(c) $u_{2} \notin L^{2} (R, d y)$ : for $y \geq 1$ one has $∣ u_{2} (y) ∣^{2} \geq e^{y^{2} - 4 y + 2}$ , which is not integrable, so $\int_{R} ∣ u_{2} ∣^{2} d y = + \infty$ ;

(d) every $C^{2}$ function $u : R \to C$ (with complex smoothness and derivatives understood componentwise as in Complex Lp classes and Euclidean test-function conventions) that belongs to $L^{2} (R, d y)$ and solves $u^{''} = (y^{2} - 1) u$ is a constant multiple of $g_{0}$ : the quantity $W (u) : = g_{0} u^{'} - g_{0}^{'} u$ is constant for such $u$ ; if this constant is nonzero then $u (y) = g_{0} (y) (C + c π^{1 / 2} F (y))$ for some constants with $c \neq 0$ , which satisfies $∣ u (y) ∣ \geq K e^{y^{2} / 2 - 2 y + 1}$ for some $K > 0$ and all sufficiently large $y$ , and is not in $L^{2}$ ; hence the constant is zero and $u / g_{0}$ is constant.

Thus $u_{2}$ is the classical formal second solution of the ground-state equation, and its failure to be square-integrable is what forces the $L^{2}$ eigenfunction to be the Gaussian.

Facts & Assumptions

Given: $g_{0} (y) = π^{- 1 / 4} e^{- y^{2} / 2}$ , $F (y) = \int_{0}^{y} e^{t^{2}} d t$ , $u_{2} = e^{- y^{2} / 2} F$ , and, in part (d), a componentwise $C^{2}$ function $u : R \to C$ with $u \in L^{2} (R, d y)$ .

[F1]

$g_{0}^{'} = - y g_{0}$ and $g_{0}^{''} = (y^{2} - 1) g_{0}$ , so $(- \partial_{y}^{2} + y^{2}) g_{0} = g_{0}$ ; $g_{0} > 0$ everywhere (Hermite recurrence(a),(d), Hermite orthogonality(b), Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , The exponential function is smooth and $(\exp)^{'} = \exp$ , The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ ).

[F2]

$F (y) = \int_{0}^{y} e^{t^{2}} d t$ uses oriented limits (The integral with oriented limits: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ ). For each $y_{0} \in R$ , choose $a < \min (0, y_{0})$ and $b > \max (0, y_{0})$ and put $G (x) = \int_{a}^{x} e^{t^{2}} d t$ on $[a, b]$ . Oriented additivity gives $F (x) = G (x) - G (0)$ on this interval, and the first FTC applied to the continuous integrand gives $F^{'} (y_{0}) = G^{'} (y_{0}) = e^{y_{0}^{2}}$ (For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ , 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); hence $F \in C^{1} (R)$ . For $t \in R$ , $e^{t^{2}} \geq e^{0} = 1$ by strict increase and the defining series at zero (The exponential function is strictly increasing, The complex exponential by its power series), so $F (y) \geq y \geq 0$ for $y \geq 0$ .

[F5]

For every real $x$ , $e^{x} > 0$ and $e^{- x} = 1 / e^{x}$ (The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ ); the real exponential is strictly increasing (The exponential function is strictly increasing). The complex exponential extends the real one and satisfies $e^{z + w} = e^{z} e^{w}$ for all $z, w \in C$ ( $\exp (z + w) = \exp z \exp w$ , and the complex exponential extends the real exponential).

[F3]

If $G$ is differentiable with integrable derivative on $[a, b]$ , then $\int_{a}^{b} G^{'} = G (b) - G (a)$ (The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ ). If a nonnegative measurable $h$ satisfies $h \geq 1$ on $[a, \infty)$ for some real $a$ , then for every integer $N \geq 1$ , $1_{[a, a + N]} \leq h$ ; monotonicity of the nonnegative integral and the identity $\int 1_{E} d λ = λ (E)$ for indicators (from the simple-integral definition and its agreement with the nonnegative integral) give $\int h d λ \geq λ ([a, a + N]) = N$ , so $h$ is not integrable (The nonnegative Lebesgue integral, The integral of a nonnegative simple function, The nonnegative integral agrees with the simple integral on simple functions, Monotonicity and nonnegative homogeneity of the nonnegative integral, A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included).

[F4]

For a complex-valued function, $C^{2}$ means its real and imaginary parts are $C^{2}$ , with derivatives taken componentwise (Complex Lp classes and Euclidean test-function conventions).

Verification

1.1givenF1F2algebra

[(a) the formal solution] By [F2], $F \in C^{1}$ with $F^{'} = e^{y^{2}}$ , so $u_{2}$ is $C^{2}$ with, using the product rule and [F1], $u_{2}^{'} = e^{- y^{2} / 2} (F^{'} - y F) = e^{- y^{2} / 2} (e^{y^{2}} - y F)$ and $u_{2}^{''} = e^{- y^{2} / 2} (2 y e^{y^{2}} - F - y F^{'} - y (e^{y^{2}} - y F)) = (y^{2} - 1) u_{2}$ because the $e^{y^{2}}$ terms cancel. Since $(- \partial_{y}^{2} + y^{2}) g_{0} = g_{0}$ by [F1], the equation $u^{''} = (y^{2} - 1) u$ is exactly the ground-state eigenvalue equation.

1.2givenF2F3F5algebra

[(c) nonintegrability] For $y \geq 1$ , $F (y) = \int_{0}^{y} e^{t^{2}} d t \geq \int_{y - 1}^{y} e^{t^{2}} d t \geq e^{(y - 1)^{2}}$ because $t \geq y - 1 \geq 0$ on the interval and the exponential is increasing by [F5]. Hence $∣ u_{2} (y) ∣^{2} = e^{- y^{2}} F (y)^{2} \geq e^{- y^{2}} e^{2 (y - 1)^{2}} = e^{y^{2} - 4 y + 2}$ for $y \geq 1$ ; the lower bound exceeds $1$ for $y \geq 4$ , so [F3] implies $\int_{R} ∣ u_{2} ∣^{2} d y = + \infty$ . Hence $u_{2} \notin L^{2} (R, d y)$ .

2.1step 1.1F1F5algebra

[(b) the Wronskian] Using $g_{0}^{'} = - y g_{0}$ from [F1] and the first formula of step 1.1, $W = g_{0} u_{2}^{'} - g_{0}^{'} u_{2} = π^{- 1 / 4} e^{- y^{2} / 2} \cdot e^{- y^{2} / 2} (e^{y^{2}} - y F) + y π^{- 1 / 4} e^{- y^{2} / 2} \cdot e^{- y^{2} / 2} F = π^{- 1 / 4} (1 - y F e^{- y^{2}} + y F e^{- y^{2}}) = π^{- 1 / 4}$ , a nonzero constant; hence $g_{0}, u_{2}$ are linearly independent (if $a g_{0} + b u_{2} = 0$ , applying $W (g_{0}, v) : = g_{0} v^{'} - g_{0}^{'} v$ gives $b π^{- 1 / 4} = 0$ , hence $b = 0$ , and then $a = 0$ because $g_{0} > 0$ ).

3.1step 1.1step 1.2F1F3F4F5algebra∎

[(d) all complex $L^{2}$ solutions are multiples of $g_{0}$ ] Let $u : R \to C$ be componentwise $C^{2}$ by [F4] and solve $u^{''} = (y^{2} - 1) u$ . Put $W (u) : = g_{0} u^{'} - g_{0}^{'} u$ . Applying the real product rule to the real and imaginary parts gives $W (u)^{'} = g_{0} u^{''} - g_{0}^{''} u = g_{0} (y^{2} - 1) u - (y^{2} - 1) g_{0} u = 0$ using [F1]. Applying [F3] to the real and imaginary parts on any finite interval gives $W (u) (y) = W (u) (0) = c$ , so $W (u)$ is constant. Since $g_{0} > 0$ on all of $R$ , $(u / g_{0})^{'} = W (u) / g_{0}^{2} = c / g_{0}^{2}$ , and $1 / g_{0}^{2} = π^{1 / 2} e^{y^{2}}$ is continuous; applying [F3] separately to the real and imaginary parts and integrating from $0$ to $y$ gives $u (y) = g_{0} (y) (C + c π^{1 / 2} F (y))$ for $C = u (0) / g_{0} (0)$ . If $c \neq 0$ , choose $Y \geq 1$ so large that $∣ c ∣ \sqrt{π} F (y) \geq 2 ∣ C ∣$ for all $y \geq Y$ ; such $Y$ exists by step 1.2. The reverse triangle inequality gives $∣ C + c \sqrt{π} F (y) ∣ \geq \frac{1}{2} ∣ c ∣ \sqrt{π} F (y)$ , hence for $y \geq Y$ , $∣ u (y) ∣ \geq \frac{1}{2} ∣ c ∣ π^{1 / 2} g_{0} (y) e^{(y - 1)^{2}} = \frac{1}{2} ∣ c ∣ π^{1 / 4} e^{y^{2} / 2 - 2 y + 1}$ by the lower bound on $F$ , which tends to $+ \infty$ ; hence $∣ u (y) ∣^{2} \geq 1$ on some half-line $[a, \infty)$ , and [F3] gives $u \notin L^{2}$ . Therefore if $u \in L^{2}$ then $c = 0$ and $u = C g_{0}$ .

Formal nonnormalizable solution

Example

Facts & Assumptions

Verification

Depends on

Dependency tree · 2 levels

Sources