Alphabeta Math
CounterexampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck pass
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 smaller constant test space gives a nontrivial practical DPG kernel

Statement

On one triangle, take a four-dimensional trial subspace of P1(K)2×P0(K) and the three-dimensional constant test space P0(K)2×P0(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 Wh=span⁡{(e1,0),(e2,0),(x1e1,0),(x2e2,0)} in the vector/scalar volume trial variables; these four fields are linearly independent as L2 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−1g(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 Br∗Br, so this vector has zero quadratic energy; if a solution exists, adding any multiple produces another trial solution.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 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