ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

The Rayleigh quotient on an interval

Example

Assume the Axiom of Choice, the ultrafilter lemma, DC and HB (The Axiom of Choice, The ultrafilter extension principle (UL/BPI), The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain, The real dominated-extension principle as an additional hypothesis over ZF), inherited from The first Dirichlet eigenfunction by constrained minimisation; the explicit computation below consumes only Countable Choice, through The sharp Dirichlet Poincare inequality on an interval. On $Ω = (0, 1)$ the constrained minimisation of The first Dirichlet eigenfunction by constrained minimisation is explicit: a minimiser of $E (u) = \int_{0}^{1} u^{' 2}$ on the $L^{2}$ -unit sphere $S \subseteq H_{0}^{1} (0, 1)$ is $u_{0} (x) = \sqrt{2} \sin (π x)$ , the minimum is $λ_{1} = π^{2}$ , and the weak eigenvalue equation is $- u_{0}^{''} = π^{2} u_{0}$ with $u_{0} (0) = u_{0} (1) = 0$ .

Facts & Assumptions

Given: The interval $(0, 1)$ , the energy $E (u) = \int_{0}^{1} u^{' 2} d x$ on $H_{0}^{1} (0, 1; R)$ , the unit sphere $S = {u \in H_{0}^{1} (0, 1) : ∥ u ∥_{L^{2}} = 1}$ (The notation $H^{k}$ and the reserved zero-boundary symbol, Integer-order Sobolev spaces and their norms, Zero-boundary Sobolev space as a norm closure), and $u_{0} (x) = \sqrt{2} \sin (π x)$ .

[F1]

The sharp Dirichlet Poincare inequality on an interval: with $L = 1$ and $ϕ (x) = \sin (π x)$ , every $u \in H_{0}^{1} (0, 1)$ satisfies $∥ u ∥_{L^{2}} \leq π^{- 1} ∥ u^{'} ∥_{L^{2}}$ , the function $ϕ$ attains equality, and $\int_{0}^{1} ϕ^{'} v^{'} d x = π^{2} \int_{0}^{1} ϕ v d x$ for every $v \in H_{0}^{1} (0, 1)$ .

[F2]

The derivatives of sine and cosine are cosine and minus sine, 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)$ : $u_{0}^{'} (x) = \sqrt{2} π \cos (π x)$ and $u_{0}^{''} (x) = - \sqrt{2} π^{2} \sin (π x) = - π^{2} u_{0} (x)$ .

[F3]

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)$ : for every $ψ \in C_{c}^{\infty} (0, 1)$ , choose $0 < a < b < 1$ with $ψ = 0$ near $a, b$ ; applying the fundamental theorem to $u_{0} ψ$ on $[a, b]$ gives $\int_{0}^{1} u_{0} ψ^{'} = - \int_{0}^{1} u_{0}^{'} ψ$ . Thus the classical derivative $u_{0}^{'}$ is also the weak derivative.

[F4]

Explicit compactly supported smooth cutoffs: in dimension one there is $χ \in C_{c}^{\infty} (R)$ with $0 \leq χ \leq 1$ , $χ = 1$ on $[- 1, 1]$ , and $χ = 0$ outside $[- 2, 2]$ ; for every $R > 0$ , the dilate $χ_{R} (x) = χ (x / R)$ has derivative $R^{- 1} χ^{'} (x / R)$ . The construction requires no choice.

[F5]

Double-angle and quadratic power-reduction identities, 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)$ , The derivatives of sine and cosine are cosine and minus sine, Integrable functions on $[a, b]$ form a set closed under sums and scalar multiples, and $\int_{a}^{b} (λ f + μ g) = λ \int_{a}^{b} f + μ \int_{a}^{b} g$ , Pi is the first positive zero of sine: $\sin^{2} t = (1 - \cos 2 t) / 2$ and $\cos^{2} t = (1 + \cos 2 t) / 2$ ; $\sin (π) = \sin (2 π) = 0$ ; and the fundamental theorem of calculus applied to $\sin (2 π x) / (2 π)$ gives $\int_{0}^{1} \cos (2 π x) d x = 0$ , since the integral is linear.

[F6]

The first Dirichlet eigenfunction by constrained minimisation: on a nonempty bounded open set, $E$ attains its infimum $λ_{1}$ on $S$ , and every minimiser $u_{0}$ satisfies $\int u_{0}^{'} h^{'} = λ_{1} \int u_{0} h$ for all $h \in H_{0}^{1}$ with $λ_{1} = E (u_{0})$ .

Verification

technique · direct

Given: The interval, the energy and the function $u_{0}$ above.

1.1givenF2F3F4F5

The function $u_{0}$ is smooth on $[0, 1]$ , with classical derivative $u_{0}^{'} (x) = \sqrt{2} π \cos (π x)$ by [F2]. For each test function $ψ \in C_{c}^{\infty} (0, 1)$ , integration of $(u_{0} ψ)^{'}$ over an interior interval containing its support gives $\int_{0}^{1} u_{0} ψ^{'} = - \int_{0}^{1} u_{0}^{'} ψ$ [F3], so $u_{0}^{'}$ is its weak derivative; both $u_{0}$ and $u_{0}^{'}$ are bounded, hence $u_{0} \in H^{1} (0, 1)$ . Take $χ$ from [F4] and put $M = ∥ χ^{'} ∥_{L^{\infty} (R)} < \infty$ . For integers $m \geq 5$ , define $ξ_{m} (x) = (1 - χ (m x)) (1 - χ (m (1 - x)))$ . Then $ξ_{m} \in C_{c}^{\infty} (0, 1)$ , $ξ_{m} = 1$ on $[2 / m, 1 - 2 / m]$ , $∥ ξ_{m}^{'} ∥_{\infty} \leq 2 M m$ , and both $1 - ξ_{m}$ and $ξ_{m}^{'}$ are supported in $B_{m} = (0, 2 / m) \cup (1 - 2 / m, 1)$ . On $B_{m}$ , $∣ u_{0} (x) ∣ \leq 2 \sqrt{2} π / m$ , while $∣ u_{0}^{'} (x) ∣ \leq \sqrt{2} π$ everywhere; since $∣ B_{m} ∣ \leq 4 / m$ , these bounds give $∥ (1 - ξ_{m}) u_{0} ∥_{L^{2}} \to 0$ and $∥ (1 - ξ_{m}) u_{0}^{'} - ξ_{m}^{'} u_{0} ∥_{L^{2}} \to 0$ . Hence $ξ_{m} u_{0} \to u_{0}$ in $H^{1} (0, 1)$ , and the closure definition of $H_{0}^{1}$ gives $u_{0} \in H_{0}^{1} (0, 1)$ . Finally $u_{0} (0) = u_{0} (1) = 0$ because $\sin 0 = \sin π = 0$ [F5].

2.1step 1.1F5

Normalisation and energy: by the power-reduction identities and the vanishing of $\int_{0}^{1} \cos (2 π x) d x$ [F5], $\int_{0}^{1} \sin^{2} (π x) d x = \frac{1}{2} \int_{0}^{1} (1 - \cos (2 π x)) d x = \frac{1}{2}$ and $\int_{0}^{1} \cos^{2} (π x) d x = \frac{1}{2}$ ; hence $∥ u_{0} ∥_{L^{2}}^{2} = 2 \cdot \frac{1}{2} = 1$ , so $u_{0} \in S$ , and $E (u_{0}) = \int_{0}^{1} u_{0}^{' 2} = 2 π^{2} \int_{0}^{1} \cos^{2} (π x) d x = π^{2}$ .

3.1step 1.1step 2.1F1

Minimality: for every $v \in S$ the sharp inequality [F1] gives $1 = ∥ v ∥_{L^{2}} \leq π^{- 1} ∥ v^{'} ∥_{L^{2}}$ , that is $E (v) = ∥ v^{'} ∥_{L^{2}}^{2} \geq π^{2}$ ; since $u_{0} \in S$ with $E (u_{0}) = π^{2}$ by step 2.1, the infimum over $S$ is the minimum $λ_{1} = π^{2}$ , attained at $u_{0}$ .

4.1step 1.1step 3.1F1F2F5

Weak eigenvalue equation: the weak identity of [F1] for $ϕ = \sin (π x)$ scales by $\sqrt{2}$ to $\int_{0}^{1} u_{0}^{'} h^{'} = π^{2} \int_{0}^{1} u_{0} h$ for every $h \in H_{0}^{1} (0, 1)$ , and by [F2] $u_{0}^{''} = - π^{2} u_{0}$ classically with $u_{0} (0) = u_{0} (1) = 0$ ; thus $- u_{0}^{''} = π^{2} u_{0}$ holds in the weak sense, with $λ_{1} = π^{2}$ as the eigenvalue.

5.1step 1.1step 2.1step 3.1step 4.1F1F6∎

Steps 1.1-4.1 exhibit the minimiser, the minimum and the eigenvalue equation explicitly, so the constrained minimisation of [F6] on $(0, 1)$ has $u_{0} (x) = \sqrt{2} \sin (π x)$ as a minimiser with $λ_{1} = π^{2}$ , in agreement with the general statement; the only choice principle consumed by this computation is Countable Choice through the sharp interval inequality [F1].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

102 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

Riccardo Cristoferi, Calculus of Variations: Lecture Notes, Carnegie Mellon University 2016 (complete 133-page notes) (standard reference, not scraped)
Richard S. Laugesen, Spectral Theory of Partial Differential Equations: Lecture Notes (arXiv:1203.2344, complete monograph) (standard reference, not scraped)