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

A shift removes a negative zero-order obstruction

Example

Assume the Axiom of Choice and Countable Choice, for the invoked Sobolev and interval-eigenpair suppliers; The Lax--Milgram theorem itself requires only Countable Choice. Over $K \in {R, C}$ , on $Ω = (0, π)$ take $L u = - u^{''} - 10 u$ , so that $a (u, v) = \int_{0}^{π} (u^{'} \overline{v^{'}} - 10 u \overline{v}) d x$ (Uniformly elliptic divergence-form operators and their sesquilinear forms with $a^{11} = 1$ , $b = 0$ , $c = - 10$ ). Then $a$ is not coercive and not even nonnegative: for $u = \sin x$ one has $a (u, u) = \frac{π}{2} (1 - 10) < 0$ . Garding's inequality with $θ = 1$ , $M_{b} = 0$ , $M_{c} = 10$ gives $Re a (u, u) \geq \frac{1}{2} ∥ u ∥_{H_{0}^{1}}^{2} - \frac{21}{2} ∥ u ∥_{L^{2}}^{2},$ so the shift corollary makes $a_{μ}$ coercive for every $μ \geq \frac{21}{2}$ , and Lax--Milgram gives unique solvability of $- u^{''} - 10 u + μ u = f$ with zero boundary values for such $μ$ (The shifted elliptic solution operator). Directly, $a_{μ} (u, u) = \int_{0}^{π} (∣ u^{'} ∣^{2} + (μ - 10) ∣ u ∣^{2}) d x \geq \min (1, μ - 10) ∥ u ∥_{H_{0}^{1}}^{2} .$ Thus $a_{μ}$ is coercive already for every $μ > 10$ ; the displayed lower bound is strictly positive when $u \neq 0$ , and this sharper threshold improves on the general Gårding threshold. No boundary regularity is used.

Facts & Assumptions

Given: the Axiom of Choice and Countable Choice; $K \in {R, C}$ ; the interval $Ω = (0, π)$ ; the coefficients $a^{11} = 1$ , $b = 0$ , $c = - 10$ , hence $θ = 1$ , $M_{b} = 0$ , $M_{c} = 10$ ; the form $a (u, v) = \int_{0}^{π} (u^{'} \overline{v^{'}} - 10 u \overline{v}) d x$ ; a shift $μ \in R$ .

[F1]

Uniform ellipticity and coefficient data: $a^{11} = 1$ gives $θ = 1$ , and $∣ c ∣ = 10$ gives $M_{c} = 10$ in the convention of the divergence-form operator (Uniformly elliptic divergence-form operators and their sesquilinear forms).

[F2]

Garding and the shift: with these constants Garding reads $Re a (u, u) \geq \frac{1}{2} ∥ u ∥_{H_{0}^{1}}^{2} - \frac{21}{2} ∥ u ∥_{L^{2}}^{2}$ , and the shifted form $a_{μ} = a + μ (\cdot, \cdot)_{L^{2}}$ is bounded and coercive with constant $1 / 2$ for every $μ \geq \frac{21}{2}$ ; the solution operator $K_{μ}$ is defined by Lax--Milgram for such $μ$ (Garding's inequality for a divergence-form elliptic operator, A sufficiently large shift is coercive, The shifted elliptic solution operator, Bounded, coercive and symmetric sesquilinear forms).

[F3]

Explicit integrals: $\int_{0}^{π} \cos^{2} x d x = \int_{0}^{π} \sin^{2} x d x = π / 2$ by the second fundamental theorem of calculus and the product-to-sum identities, and $\sin x \in H_{0}^{1} (0, π)$ with weak derivative $\cos x$ (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)$ , Dirichlet Laplacian eigenpairs on an interval, Integer-order Sobolev spaces and their norms, Zero-boundary Sobolev space as a norm closure, The Lax--Milgram theorem).

Verification

technique · direct

1.1F1F3givenalgebra

Failure of coercivity. For $u = \sin x \in H_{0}^{1} (0, π)$ one has $u^{'} = \cos x$ , so by [F3] $a (u, u) = \int_{0}^{π} (\cos^{2} x - 10 \sin^{2} x) d x = \frac{π}{2} - 10 \cdot \frac{π}{2} = - \frac{9 π}{2} < 0.$ Hence $a$ is neither coercive nor nonnegative.

1.2F2givenalgebra

The general shift. With $θ = 1$ , $M_{b} = 0$ , $M_{c} = 10$ the Garding constants are $α = 1 / 2$ and $β = 1 / 2 + 0 + 10 = 21 / 2$ , so [F2] gives $Re a (u, u) \geq \frac{1}{2} ∥ u ∥_{H_{0}^{1}}^{2} - \frac{21}{2} ∥ u ∥_{L^{2}}^{2}$ and makes $a_{μ}$ bounded and coercive for every $μ \geq 21 / 2$ . By Lax--Milgram the problem $- u^{''} - 10 u + μ u = f$ with zero boundary values has a unique weak solution for every $f \in L^{2} (0, π)$ at those shifts.

2.1F1F3step 1.2givenalgebra∎

The sharper direct threshold. For every $u \in H_{0}^{1} (0, π)$ the shifted form is $a_{μ} (u, u) = \int_{0}^{π} (∣ u^{'} ∣^{2} + (μ - 10) ∣ u ∣^{2}) d x \geq \min (1, μ - 10) (∥ u^{'} ∥_{L^{2}}^{2} + ∥ u ∥_{L^{2}}^{2}) = \min (1, μ - 10) ∥ u ∥_{H_{0}^{1}}^{2} .$ For $μ > 10$ the constant $\min (1, μ - 10)$ is strictly positive and $a_{μ}$ is coercive with that constant, sharper than the general threshold $21 / 2$ of step 1.2; the displayed inequality is positive for every nonzero $u$ , so the shifted problem is uniquely solvable for every $μ > 10$ as well. No boundary regularity of $Ω$ was used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

75 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

John K. Hunter, Notes on Partial Differential Equations (UC Davis, revised 18 June 2014, complete 242-page notes) (standard reference, not scraped)
Gerald Teschl, Partial Differential Equations: From Classical to Modern (2025 archived author manuscript, complete 392 pages) (standard reference, not scraped)