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.

✓ 4 results · all verified · 2 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

First-order least-squares FEM and practical DPG — Examples

1 · Prerequisites

2 · Summary

These examples check the boundary and stability caveats. If the homogeneous Dirichlet condition is dropped, constants give distinct zero-residual states for zero data. If the practical test space has smaller dimension than its trial space, the restricted Riesz map has a kernel and unique solvability cannot be guaranteed.

The finite-dimensional DPG calculation compares ideal and practical trial-to-test vectors for the nonsymmetric matrix $A = (\begin{array}{cc} 1 & 1 \\ 0 & 1 \end{array})$ . It yields coefficients $1 / 2$ and $1$ under the same load, so the practical method need not reproduce the ideal test vector.

On the unit square with a two-triangle conforming mesh, $u = x (1 - x) y (1 - y)$ , $σ = - \nabla u$ , and $f = 2 x (1 - x) + 2 y (1 - y)$ give an exact least-squares residual certificate: the scalar vanishes on the boundary, the first residual is zero by construction, and $div σ = f$ .

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

Dropping the H1-zero boundary condition makes least squares nonunique

Statement

If zero boundary values are removed from the continuous first-order Poisson least-squares problem with zero load, every constant scalar $u$ with $σ = 0$ has zero residual; hence the unconstrained minimizer is not unique.

Facts & Assumptions

Given: The least-squares residual convention and $f = 0$ .

[F1]

The residual is $(σ + \nabla u, d i v σ - f)$ and the intended scalar space is $H_{0}^{1}$ . (First-order least-squares formulation of the Dirichlet Poisson problem)

Proof

1.1F1constructalgebra

Fix any $c \in R$ and set $u (x) = c$ , $σ (x) = 0$ , $f = 0$ . Then $\nabla u = 0$ and $d i v σ = 0$ , so both residual components in [F1] vanish.

2.1step 1.1givenalgebra∎

Distinct constants give distinct H1 functions, and every one has objective zero, the minimum of a sum of squares. They are all admissible after the stated replacement of H1_0 by H1, so the unconstrained minimizer is not unique.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passjudge pass (gpt-6-luna)Open item page →

An exact polynomial Poisson solution has a zero residual certificate

Statement

Assume Countable Choice. On $Ω = (0, 1)^{2}$ with its two-triangle diagonal mesh, let $u = x (1 - x) y (1 - y)$ , $σ = - \nabla u$ , and $f = - Δ u$ . Then $u \in H_{0}^{1} (Ω)$ , $σ \in H (d i v; Ω)$ , $σ + \nabla u = 0$ , and $d i v σ - f = 0$ , so the continuous least-squares residual is zero.

Facts & Assumptions

Given: The square domain and the polynomial fields in the Statement.

[F1]

The first-order Poisson residual and boundary convention. (First-order least-squares formulation of the Dirichlet Poisson problem)

[A1]

Countable Choice is declared by the zero-boundary polynomial density supplier. (The Axiom of Countable Choice ( ${A C}_{ω}$ ))

[F2]

A conforming piecewise polynomial with zero boundary traces on a finite matching mesh belongs to $H_{0}^{1}$ . (Zero-boundary conforming polynomials lie in W0 1p and satisfy Poincare)

[F3]

$H_{0}^{1}$ is the $H^{1}$ closure of compactly supported smooth functions. (Zero-boundary Sobolev space as a norm closure)

[F4]

H(div) consists of L2 vector fields with L2 distributional divergence. (The real H(div) space)

Proof

1.1A1F1F2F3F4givenalgebra

The factor $x (1 - x) y (1 - y)$ vanishes on all four edges. Differentiating gives $Δ u = - 2 x (1 - x) - 2 y (1 - y)$ , so $f = 2 x (1 - x) + 2 y (1 - y)$ is polynomial and [F2] gives $u \in H_{0}^{1}$ . For every $v \in C_{c}^{\infty} (Ω)$ , integration by parts gives $(\nabla u, \nabla v) = (f, v)$ ; both sides are continuous in the H1 norm, so [F3] extends the identity to every $v \in H_{0}^{1}$ . Thus $u$ is the weak Dirichlet solution. Also $σ = - \nabla u$ and $div σ = f$ are polynomials in $L^{2}$ , so [F4] gives $σ \in H (div; Ω)$ .

2.1F1step 1.1algebra∎

By definition $σ + \nabla u = 0$ and $d i v σ = - Δ u = f$ , so both components in [F1] vanish pointwise. The objective is nonnegative and therefore this exact zero residual is a global least-squares minimum.

CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passOpen item page →

A smaller constant test space gives a nontrivial practical DPG kernel

Statement

On one triangle, take a four-dimensional trial subspace of $P_{1} (K)^{2} \times P_{0} (K)$ and the three-dimensional constant test space $P_{0} (K)^{2} \times P_{0} (K)$ . The practical trial-to-test map has a nontrivial kernel, so the normal equations cannot have a unique trial solution for any load for which a solution exists.

Facts & Assumptions

Given: A nondegenerate triangle, the ultraweak form, and the finite Riesz construction.

[F1]

The cell trial/test form and polynomial setting are specified in the DPG formulation. (Ultraweak Poisson DPG spaces and plan-consistent bilinear form)

[F2]

The practical trial-to-test map is the finite Riesz representative. (Exact local finite Riesz solves for practical DPG tests)

Proof

1.1F1constructalgebra

Choose $W_{h} = span {(e_{1}, 0), (e_{2}, 0), (x_{1} e_{1}, 0), (x_{2} e_{2}, 0)}$ in the vector/scalar volume trial variables; these four fields are linearly independent as $L^{2}$ pairs. The constant test space has dimension $2 + 1 = 3$ .

2.1F2step 1.1algebra∎

In a fixed basis of the constant test space, the Gram matrix is positive definite, and [F2] returns $G^{- 1} g (w)$ in that basis. The right-hand side $g (w)$ is linear in $w$ , so the restricted practical trial-to-test map is linear from the four-dimensional trial subspace into the three-dimensional test space. The images of four independent basis vectors are therefore linearly dependent; the corresponding nonzero coefficient vector is in the kernel. The normal matrix is $B_{r}^{*} B_{r}$ , so this vector has zero quadratic energy; if a solution exists, adding any multiple produces another trial solution.

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passOpen item page →

An explicit finite model separates ideal and practical test vectors

Statement

Let $U = V = R^{2}$ with Euclidean inner product, $A = (\begin{array}{cc} 1 & 1 \\ 0 & 1 \end{array})$ , $b (x, y) = (A x) \cdot y$ , $U_{h} = span (e_{2})$ , practical test space $V_{r} = span (e_{1})$ , and load $F (y) = e_{1} \cdot y$ . Then $T e_{2} = (1, 1)$ , $T^{r} e_{2} = e_{1}$ , and ideal and practical trial coefficients are $1 / 2$ and $1$ .

Facts & Assumptions

Given: The stated finite-dimensional trial/test data.

[F1]

In this finite model, define $T w \in V$ by $(T w, y)_{V} = b (w, y)$ for every $y \in V$ ; existence and uniqueness follow from finite-dimensional Riesz representation. (Finite-dimensional Riesz representation: every functional is uniquely $v \mapsto ⟨ v, w ⟩$ )

[F2]

Define $T^{r} w \in V_{r}$ by $(T^{r} w, y)_{V} = b (w, y)$ for every $y \in V_{r}$ ; finite-dimensional Riesz representation again gives existence and uniqueness. (Finite-dimensional Riesz representation: every functional is uniquely $v \mapsto ⟨ v, w ⟩$ )

[F3]

Finite-dimensional Riesz systems have unique representatives. (Finite-dimensional Riesz representation: every functional is uniquely $v \mapsto ⟨ v, w ⟩$ )

Proof

1.1F1F2givenalgebra

$A e_{2} = (1, 1)$ , so $(A e_{2}, y)_{V} = b (e_{2}, y)$ for every $y \in V$ , and [F1] gives $T e_{2} = (1, 1)$ . For every $y = t e_{1} \in V_{r}$ , $(e_{1}, y)_{V} = t = b (e_{2}, y)$ , so [F2] gives $T^{r} e_{2} = e_{1}$ .

2.1F1F2F3step 1.1algebra∎

For ideal coefficient $c$ , the equation is $b (c e_{2}, T e_{2}) = F (T e_{2})$ , hence $2 c = 1$ and $c = 1 / 2$ . For practical tests it is $b (c e_{2}, e_{1}) = F (e_{1})$ , hence $c = 1$ . Uniqueness follows from the positive Gram scalars $2$ and $1$ in [F3].

Remarks

The Euclidean Riesz maps defined here give a finite-dimensional analogue of Ideal Poisson DPG trial-to-test Riesz map and Exact local finite Riesz solves for practical DPG tests.

First-order least-squares FEM and practical DPG — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

Dropping the H1-zero boundary condition makes least squares nonunique

Statement

Facts & Assumptions

Proof

An exact polynomial Poisson solution has a zero residual certificate

Statement

Facts & Assumptions

Proof

A smaller constant test space gives a nontrivial practical DPG kernel

Statement

Facts & Assumptions

Proof

An explicit finite model separates ideal and practical test vectors

Statement

Facts & Assumptions

Proof

Remarks

Sources