ExampleConstruction: Literature-sourcedVerification: 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 coercive non-symmetric form can have non-real Galerkin eigenvalues

Example

On $C^{2}$ let $β > 0$ , $M = (\begin{array}{cc} 1 & β \\ - β & 1 \end{array})$ and $a (u, v) : = (M u, v)$ . Then $a$ is bounded and coercive with constant $1$ , since $Re a (u, u) = ∣ u_{1} ∣^{2} + ∣ u_{2} ∣^{2}$ ; but the eigenvalues of $M$ are $1 \pm i β$ , which are non-real. Consequently for every real $λ$ the equation $a (u, v) = λ (u, v)$ for all $v \in C^{2}$ has no nonzero solution: this non-symmetric coercive form has no weak eigenpair with a real eigenvalue, and its $2 \times 2$ Galerkin matrix has a conjugate pair of non-real eigenvalues. This shows that the reality of the eigenvalues in the discrete spectral theorem is a consequence of symmetry and not of coercivity.

Facts & Assumptions

Given: a real $β > 0$ , the matrix $M = (\begin{array}{cc} 1 & β \\ - β & 1 \end{array})$ , and the sesquilinear form $a (u, v) = (M u, v)$ on $C^{2}$ .

[F1]

Boundedness and coercivity of a sesquilinear form on a Hilbert space are defined by $∣ a (u, v) ∣ \leq C ∥ u ∥ ∥ v ∥$ and $Re a (u, u) \geq α ∥ u ∥^{2}$ , with the form linear in the first argument and conjugate-linear in the second (Bounded, coercive and symmetric sesquilinear forms).

[F2]

$C^{2}$ is a complex Hilbert space with the standard inner product, and $(M u, v)$ is computed by matrix multiplication and conjugation accordingly (Real and complex inner-product spaces and their induced length, Hilbert space, Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes, Real and imaginary parts, complex conjugation, and modulus).

[F3]

For an endomorphism of a finite-dimensional complex vector space the spectrum is the root set of its characteristic polynomial, the characteristic polynomial of a matrix $A$ is $χ_{A} (λ) = \det (λ I - A)$ , and a weak eigenpair identity $a (u, v) = λ (u, v)$ for all $v$ is equivalent to $M u = λ u$ when $a (u, v) = (M u, v)$ (Eigenvalues, eigenvectors, eigenspaces $E_{λ} (T) = \ker (T - λ I)$ , and the spectrum $σ_{F} (T)$ of an endomorphism, For $A \in M_{n} (F)$ , the characteristic polynomial is $χ_{A} (x) = \det (x I_{n} - A)$ when $n \geq 1$ , with $χ_{A} (x) = 1$ for the unique $0 \times 0$ matrix, For every finite-dimensional space, $σ_{F} (T)$ is exactly the set of roots in $F$ of $χ_{T}$ ).

[F4]

Cauchy--Schwarz: $∣ (u, v) ∣ \leq ∥ u ∥ ∥ v ∥$ (Cauchy–Schwarz: $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥ ∥ y ∥$ , with equality exactly for dependent pairs).

Verification

technique · direct

1.1F1F2givenalgebra

Coercivity. For $u = (u_{1}, u_{2})$ one computes $M u = (u_{1} + β u_{2}, - β u_{1} + u_{2})$ and $Re a (u, u) = Re (∣ u_{1} ∣^{2} + β u_{2} \overline{u_{1}} - β u_{1} \overline{u_{2}} + ∣ u_{2} ∣^{2}) = ∣ u_{1} ∣^{2} + ∣ u_{2} ∣^{2} = ∥ u ∥^{2},$ because $u_{2} \overline{u_{1}} - \overline{u_{2} \overline{u_{1}}}$ is purely imaginary and $β$ is real. Hence $Re a (u, u) = ∥ u ∥^{2} \geq 1 \cdot ∥ u ∥^{2}$ and $a$ is coercive with constant $1$ .

1.2F1F2F4givenalgebra

Boundedness. Applying Cauchy--Schwarz in the index, $∣ u_{1} + β u_{2} ∣^{2} \leq (1 + β^{2}) (∣ u_{1} ∣^{2} + ∣ u_{2} ∣^{2})$ and $∣ - β u_{1} + u_{2} ∣^{2} \leq (1 + β^{2}) (∣ u_{1} ∣^{2} + ∣ u_{2} ∣^{2})$ , so $∥ M u ∥^{2} = ∣ u_{1} + β u_{2} ∣^{2} + ∣ - β u_{1} + u_{2} ∣^{2} \leq 2 (1 + β^{2}) ∥ u ∥^{2} .$ Thus $∥ M u ∥ \leq \sqrt{2 + 2 β^{2}} ∥ u ∥$ , and [F4] gives $∣ a (u, v) ∣ = ∣ (M u, v) ∣ \leq \sqrt{2 + 2 β^{2}} ∥ u ∥ ∥ v ∥$ , so $a$ is bounded.

1.3F2F3givenalgebra

Spectrum. The characteristic polynomial is $χ_{M} (λ) = \det (λ I - M) = (1 - λ)^{2} + β^{2}$ , and because $β > 0$ its two roots are $λ = 1 \pm i β$ , which are not real. By [F3] the spectrum of the endomorphism $u \mapsto M u$ is exactly ${1 + i β, 1 - i β}$ , a conjugate pair of non-real eigenvalues of the Galerkin matrix $M$ .

2.1F1F3step 1.1step 1.2step 1.3∎

No real-eigenvalue weak eigenpair. Let $λ \in R$ be real and suppose a nonzero $u \in C^{2}$ satisfies $a (u, v) = λ (u, v)$ for every $v$ . Subtracting, $(M u - λ u, v) = 0$ for every $v$ , and testing with $v = M u - λ u$ gives $∥ M u - λ u ∥^{2} = 0$ , so $M u = λ u$ ; by [F3], $λ$ would be a real eigenvalue of $M$ , contradicting step 1.3. Hence there is no real $λ$ with a nonzero weak eigenpair. Since $a$ is nevertheless bounded and coercive by steps 1.1 and 1.2, this two-dimensional model shows that coercivity alone does not force real eigenvalues. Its complex eigenpairs at $1 \pm i β$ do exist; the exclusion just proved concerns real eigenvalues.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

44 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

Richard S. Laugesen, Linear Analysis and Partial Differential Equations (University of Illinois, 2020, complete 158-page graduate notes) (standard reference, not scraped)
Richard S. Laugesen, Spectral Theory of Partial Differential Equations (University of Illinois lecture notes, arXiv:1203.2344, complete 120 pages) (standard reference, not scraped)