Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generated
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 form need not be symmetric

Statement refuted

Assume Countable Choice for the Lax--Milgram conclusion. On H=C2 with the standard inner product define a(u,v):=u1v1‾+u2v2‾+iu1v2‾. Then a is sesquilinear in the convention of Bounded, coercive and symmetric sesquilinear forms, bounded with ∣a(u,v)∣≤2∥u∥∥v∥ and coercive with Re⁡a(u,u)≥12∥u∥2, so α=12. It is not symmetric: with e1=(1,0), e2=(0,1) one has a(e1,e2)=i while a(e2,e1)‾=0. Hence the Lax--Milgram theorem The Lax--Milgram theorem applies to this nonsymmetric form, and symmetry is not needed for existence and uniqueness; the energy-minimisation corollary Symmetric Lax--Milgram is energy minimisation is the part that genuinely uses symmetry. The example is consistent with the abstract forcing remark Nonsymmetric Lax--Milgram is not a scalar minimisation principle.

Facts & Assumptions

Given: Countable Choice; the Hilbert space H=C2 with the standard inner product ∥u∥2=∣u1∣2+∣u2∣2; the form a(u,v)=u1v1‾+u2v2‾+iu1v2‾; and the vectors e1=(1,0), e2=(0,1).

[F1]

Sesquilinearity in the convention linear in the first argument and conjugate-linear in the second, with boundedness and coercivity as in Bounded, coercive and symmetric sesquilinear forms (Real and complex inner-product spaces and their induced length, Hilbert space).

[F2]

Scalar facts: ∣zw‾∣=∣z∣∣w∣, i‾=−i, i2=−1; and for vectors in C2, ∣z1w1∣+∣z2w2∣≤(∣z1∣2+∣z2∣2)1/2(∣w1∣2+∣w2∣2)1/2 by Cauchy--Schwarz (Real and imaginary parts, complex conjugation, and modulus, Cauchy-Schwarz ∣⟨x,y⟩∣≤∥x∥2∥y∥2 with its equality case, the triangle inequality for ∥⋅∥2, the parallelogram law and polarisation).

[F3]

Lax--Milgram applies to bounded coercive forms and does not assume symmetry; the energy-minimisation corollary does assume it (The Lax--Milgram theorem, Symmetric Lax--Milgram is energy minimisation, Nonsymmetric Lax--Milgram is not a scalar minimisation principle).

Proof

1.1F1F2

Sesquilinearity, boundedness and coercivity: for scalars λ, a(λu,v)=λa(u,v) and a(u,λv)=λ‾a(u,v) directly from the definition, so a is sesquilinear in the stated convention. Moreover ∣a(u,v)∣≤∣u1∣∣v1∣+∣u2∣∣v2∣+∣u1∣∣v2∣, and Cauchy--Schwarz applied to the pairs (∣u1∣,∣u2∣), (∣v1∣,∣v2∣) gives ∣a(u,v)∣≤(∣u1∣+∣u2∣)(∣v1∣+∣v2∣)≤2∥u∥ ∥v∥; and a(u,u)=∣u1∣2+∣u2∣2+iu1u2‾ has real part at least ∥u∥2−∣u1∣∣u2∣≥12∥u∥2, using 2∣u1∣∣u2∣≤∣u1∣2+∣u2∣2. Thus a is coercive with constant α=12.

1.2F1F2

Nonsymmetry: for the standard basis vectors, a(e1,e2)=i while a(e2,e1)‾=0‾=0, so a(e1,e2)≠a(e2,e1)‾ and a is not symmetric.

2.1F1F3step 1.1step 1.2∎

Consequences: a is bounded and coercive but not symmetric, so Lax--Milgram applies and gives existence and uniqueness of solutions for every bounded conjugate-linear datum, while the energy-minimisation characterisation, which requires symmetry, does not apply. Thus symmetry is not needed for solvability but is genuinely used by the variational principle.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

45 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