CounterexampleConstruction: 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.

A large adverse zero-order term destroys Dirichlet coercivity

Statement refuted

Assume the Axiom of Choice inherited through the cited general solvability theorem, together with Countable Choice. Let $I = (0, 1)$ , $c \geq 0$ and $a_{c} (u, v) = \int_{0}^{1} u^{'} \overline{v^{'}} d x - c \int_{0}^{1} u \overline{v} d x (u, v \in H_{0}^{1} (I)) .$ The sharp constant is $C_{P} = 1 / π$ by The sharp Dirichlet Poincare inequality on an interval. For $0 \leq c < π^{2}$ , the form is coercive with constant $(π^{2} - c) / (1 + π^{2})$ in the standard $H^{1}$ norm, and The Lax--Milgram theorem gives a unique weak solution for every bounded conjugate-linear functional. For $c \geq π^{2}$ , the nonzero test $ϕ (x) = \sin (π x)$ gives $a_{c} (ϕ, ϕ) = (π^{2} - c) ∥ ϕ ∥_{2}^{2} \leq 0$ , so the form is not coercive. At the endpoint $c = π^{2}$ , the helper's weak identity gives $a_{c} (ϕ, v) = 0$ for every $v \in H_{0}^{1} (I)$ : both $0$ and $ϕ$ solve the homogeneous weak Dirichlet problem. The original polynomial witness also remains valid: $p (x) = x (1 - x) \in H_{0}^{1} (I)$ satisfies $∥ p^{'} ∥_{2}^{2} = 1 / 3$ and $∥ p ∥_{2}^{2} = 1 / 30$ , hence $a_{c} (p, p) = 1 / 3 - c / 30 \leq 0$ for $c \geq 10$ . Thus the lower-order sign/smallness mechanism in Lax--Milgram solvability for coercive divergence-form equations cannot be omitted. In this interval model its energy argument with the local sharp constant gives the exact coercivity condition $c < 1 / C_{P}^{2} = π^{2}$ ; the generic Poincare supplier itself is not claimed to provide that numerical constant.

Facts & Assumptions

Given: The Axiom of Choice and Countable Choice; the interval $I = (0, 1)$ ; a real constant $c \geq 0$ ; the form $a_{c} (u, v) = \int_{0}^{1} u^{'} \overline{v^{'}} d x - c \int_{0}^{1} u \overline{v} d x$ on $H_{0}^{1} (I)$ ; and the helper function $ϕ (x) = \sin (π x)$ .

[F1]

Sharp interval inequality and witness: $∥ u ∥_{L^{2}} \leq (1 / π) ∥ u^{'} ∥_{L^{2}}$ for $u \in H_{0}^{1} (I)$ ; $ϕ \in H_{0}^{1} (I)$ is nonzero, $ϕ^{'} ϕ$ -identities hold, and $\int_{0}^{1} ϕ^{'} \overline{v^{'}} d x = π^{2} \int_{0}^{1} ϕ \overline{v} d x$ for every $v \in H_{0}^{1} (I)$ (The sharp Dirichlet Poincare inequality on an interval).

[F2]

Hilbert structure: $H_{0}^{1} (I)$ is a Hilbert space with $∥ u ∥_{H^{1}}^{2} = ∥ u ∥_{L^{2}}^{2} + ∥ u^{'} ∥_{L^{2}}^{2}$ , and bounded coercive forms on it have unique solutions for every bounded conjugate-linear datum (The Sobolev space $H^{1}$ is a Hilbert space, The Lax--Milgram theorem, Integer-order Sobolev spaces and their norms, Zero-boundary Sobolev space as a norm closure).

[F3]

Estimates: $∣ a_{c} (u, v) ∣ \leq ∥ u^{'} ∥_{L^{2}} ∥ v^{'} ∥_{L^{2}} + c ∥ u ∥_{L^{2}} ∥ v ∥_{L^{2}} \leq (1 + c) ∥ u ∥_{H^{1}} ∥ v ∥_{H^{1}}$ by H"older; and $∥ u ∥_{H^{1}}^{2} \leq (1 + 1 / π^{2}) ∥ u^{'} ∥_{L^{2}}^{2}$ by [F1] (Holder's inequality for integrals, including the endpoint cases, Complex Holder, Minkowski, and the quotient norm, Bounded, coercive and symmetric sesquilinear forms).

[F4]

Cutoff construction on the interval: the standard smooth step $σ$ has $σ^{'} \equiv 0$ outside $(0, 1)$ and $C_{σ} : = \sup ∣ σ^{'} ∣ < \infty$ ; chain and product rules give derivatives of $η_{m} (x) = σ (m x - 1) σ (m (1 - x) - 1)$ ; elementary interval bounds, additivity over subintervals, linearity of the integral, and the agreement of the Riemann and Lebesgue integrals for bounded Riemann integrable functions on a closed interval control the resulting $L^{2}$ norms (The standard smooth step function, 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)$ , 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$ , Extreme value theorem: a continuous real function on a nonempty compact subset of $R$ attains a greatest and a least value, If $m \leq f \leq M$ on $[a, b]$ then $m (b - a) \leq L (f, P) \leq \underline{\int_{a}^{b}} f \leq \overline{\int_{a}^{b}} f \leq U (f, P) \leq M (b - a)$ for every partition $P$ ; in particular every constant function is integrable, with $\int_{a}^{b} c = c (b - a)$ , 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$ , 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$ , A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral).

[F5]

The fundamental theorem of calculus and the absolutely continuous representative of a one-dimensional Sobolev class control the polynomial integrals below (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)$ , One-dimensional $W^{1, p}$ functions have unique absolutely continuous representatives, Integral over a measurable subset, The space $L^{p} (μ)$ as the quotient by null functions).

Proof

1.1F1F2F3algebra

Coercivity below the threshold: for $0 \leq c < π^{2}$ and $u \in H_{0}^{1} (I)$ , $a_{c} (u, u) = ∥ u^{'} ∥_{L^{2}}^{2} - c ∥ u ∥_{L^{2}}^{2} \geq (1 - c / π^{2}) ∥ u^{'} ∥_{L^{2}}^{2}$ by [F1], and $∥ u ∥_{H^{1}}^{2} \leq (1 + 1 / π^{2}) ∥ u^{'} ∥_{L^{2}}^{2}$ , so $a_{c} (u, u) \geq \frac{π^{2} - c}{1 + π^{2}} ∥ u ∥_{H^{1}}^{2}$ : the form is coercive with constant $(π^{2} - c) / (1 + π^{2})$ and bounded by [F3]; Lax--Milgram gives a unique solution for every bounded conjugate-linear functional.

1.2F1algebra

Failure at and above the threshold: the helper witness satisfies $ϕ \in H_{0}^{1} (I)$ , $ϕ \neq 0$ , and $a_{c} (ϕ, ϕ) = ∥ ϕ^{'} ∥_{L^{2}}^{2} - c ∥ ϕ ∥_{L^{2}}^{2} = (π^{2} - c) ∥ ϕ ∥_{L^{2}}^{2}$ by the weak identity of [F1] with $v = ϕ$ . For $c \geq π^{2}$ this is at most $0$ while $ϕ \neq 0$ , so no $α > 0$ can satisfy $Re a_{c} (u, u) \geq α ∥ u ∥^{2}$ for all $u$ : coercivity fails.

1.3F4F5algebra

Polynomial witness: let $p (x) = x (1 - x)$ . Then $p$ is smooth on $[0, 1]$ , $p (0) = p (1) = 0$ , $∣ p (x) ∣ \leq \min (x, 1 - x)$ and $∣ p^{'} (x) ∣ \leq 1$ ; for $m \geq 4$ put $η_{m} (x) = σ (m x - 1) σ (m (1 - x) - 1)$ and $p_{m} : = η_{m} p \in C_{c}^{\infty} (I)$ . As in [F4], $∣ η_{m}^{'} ∣ \leq 2 m C_{σ}$ , $p_{m} = p$ on $[2 / m, 1 - 2 / m]$ , and on the two endpoint strips $∣ p_{m} - p ∣ \leq 2 / m$ and $∣ (p_{m} - p)^{'} ∣ \leq 4 C_{σ} + 1$ ; hence $∥ p_{m} - p ∥_{L^{2}}^{2} \leq 4 / m^{2}$ and $∥ (p_{m} - p)^{'} ∥_{L^{2}}^{2} \leq (4 C_{σ} + 1)^{2} \cdot 4 / m$ , so $p_{m} \to p$ in $H^{1}$ and $p \in H_{0}^{1} (I)$ . The fundamental theorem and linearity give $\int_{0}^{1} p^{' 2} = \int_{0}^{1} (1 - 2 x)^{2} d x = 1 - 2 + \frac{4}{3} = \frac{1}{3}$ and $\int_{0}^{1} p^{2} = \int_{0}^{1} (x^{2} - 2 x^{3} + x^{4}) d x = \frac{1}{3} - \frac{1}{2} + \frac{1}{5} = \frac{1}{30}$ ; hence $a_{c} (p, p) = \frac{1}{3} - \frac{c}{30} \leq 0$ for $c \geq 10$ .

2.1F1step 1.2

Endpoint nonuniqueness: at $c = π^{2}$ the same weak identity gives $a_{π^{2}} (ϕ, v) = 0$ for every $v \in H_{0}^{1} (I)$ ; since $ϕ \neq 0$ , both the zero function and $ϕ$ solve the homogeneous weak Dirichlet problem, so uniqueness fails at the endpoint. No claim is made here about nonuniqueness for $c > π^{2}$ .

3.1step 1.1step 2.1step 1.3∎

Conclusion: for $0 \leq c < π^{2}$ the form is coercive with the explicit constant and Lax--Milgram applies; for $c \geq π^{2}$ the nonzero sine witness destroys coercivity with equality of the quadratic form on $ϕ$ at the endpoint, where nonuniqueness is explicit; the polynomial witness independently witnesses failure for $c \geq 10$ . Therefore the sign/smallness mechanism of the general solvability theorem cannot be omitted, and in this interval model the exact threshold is $c < 1 / C_{P}^{2} = π^{2}$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

161 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 two-quarter notes) (standard reference, not scraped)
John K. Hunter, Notes on Partial Differential Equations (UC Davis, revised 18 June 2014, complete 242-page two-quarter notes) (standard reference, not scraped)
Leon Simon, Lectures on Partial Differential Equations (Stanford, complete 223-page author scan) (standard reference, not scraped)
Richard S. Laugesen, Linear Analysis and Partial Differential Equations (University of Illinois, 2020, complete 158-page graduate notes) (standard reference, not scraped)