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 bounded form without coercivity need not be solvable

Statement refuted

Let $H$ be a nonzero real or complex Hilbert space and let $a \equiv 0$ , so $a$ is a bounded sesquilinear form with bound $M = 0$ , but $a$ is not coercive: $Re a (u, u) = 0$ for all $u$ , so no $α > 0$ satisfies $Re a (u, u) \geq α ∥ u ∥^{2}$ at any $u \neq 0$ . Let $F \neq 0$ be a bounded conjugate-linear functional on $H$ . Then the equation $a (u, v) = F (v)$ for all $v \in H$ has no solution, since its left side is identically $0$ while the right side is not. Hence boundedness alone does not imply existence or uniqueness, and the coercivity hypothesis of The Lax--Milgram theorem cannot be dropped. The same witness shows that the estimate $∥ u ∥ \leq ∥ F ∥ / α$ has no content without $α > 0$ .

Facts & Assumptions

Given: A nonzero real or complex Hilbert space $H$ ; the zero form $a \equiv 0$ ; and a nonzero bounded conjugate-linear functional $F$ on $H$ .

[F1]

$a \equiv 0$ is sesquilinear and bounded with $M = 0$ ; $Re a (u, u) = 0$ for every $u$ , so $a$ is coercive with no $α > 0$ : a nonzero $u$ would give $α ∥ u ∥^{2} \leq Re a (u, u) = 0$ (Bounded, coercive and symmetric sesquilinear forms, Hilbert space).

[F2]

Since $F \neq 0$ there is $v_{0} \in H$ with $F (v_{0}) \neq 0$ ; also $H \neq {0}$ (A bounded linear operator between normed spaces, The operator norm as the least bound and as the unit-sphere or unit-ball supremum, Real and imaginary parts, complex conjugation, and modulus).

[F3]

A solution of $a (u, v) = F (v)$ for all $v \in H$ would in particular satisfy $a (u, v_{0}) = F (v_{0})$ (The Lax--Milgram theorem records the equation whose hypotheses fail here).

Proof

1.1F1

The form is bounded but not coercive: $∣ a (u, v) ∣ = 0 \leq 0 \cdot ∥ u ∥ ∥ v ∥$ shows the bound $M = 0$ , while for every $u \neq 0$ and every $α > 0$ one has $Re a (u, u) = 0 < α ∥ u ∥^{2}$ .

1.2F2

A datum with nonzero value: $F \neq 0$ means $∥ F ∥ = \sup_{∥ v ∥ \leq 1} ∣ F (v) ∣ > 0$ , so some $v_{0}$ has $F (v_{0}) \neq 0$ .

2.1F1F3step 1.2∎

No solution: if $u \in H$ satisfied $a (u, v) = F (v)$ for all $v$ , then $0 = a (u, v_{0}) = F (v_{0}) \neq 0$ , a contradiction. Hence the equation has no solution, so neither existence nor uniqueness follows from boundedness alone; the estimate $∥ u ∥ \leq ∥ F ∥ / α$ of The Lax--Milgram theorem has no content without $α > 0$ , and the coercivity hypothesis there cannot be dropped.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

24 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)
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)