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 continuous P1 pressure gives a nonconservative primal flux
Statement
Assume Countable Choice.
On the unit square split along the diagonal from to , the continuous piecewise-affine pressure with nodal values at has negative gradient below the diagonal and above it. Each cellwise divergence is zero, but the normal flux jumps by magnitude across the diagonal; hence this piecewise field is not in and does not have a locally conservative global flux.
Facts & Assumptions
Given: The unit square mesh and the nodal data stated above; all vector fields and distributional pairings are real.
Countable Choice is inherited from the real H(div) definition. (The Axiom of Countable Choice ())
H(div) consists of vector fields whose distributional divergence is an function. (The real H(div) space)
Cauchy–Schwarz bounds the pairing of any hypothetical divergence with a test function. (Cauchy-Schwarz inequality for )
Proof
Let and . The affine formulas and agree on and attain the four stated vertex values, so they define a continuous piecewise-P1 function. Their negative gradients are and , each with classical divergence zero. With fixed diagonal normal , and , so the jump magnitude is .
For , integration by parts on the two triangles shows that the distributional divergence of the piecewise field is the nonzero line measure on the diagonal with density in this orientation (the distributional pairing is the negative of the summed outward boundary flux). To see it cannot be an function, choose a nonnegative smooth supported in the open diagonal with positive line integral and a smooth transverse cutoff with ; set in tubular coordinates, extended by zero. The surface pairing is the fixed nonzero number , whereas . If the distribution were represented by , [F2] would give , a contradiction. By [F1] the field is not in H(div).
Mesh diagram
The square coordinates are the unit-square vertices, and the diagonal is the shared facet. The fixed normal points from to ; arrow lengths are schematic, while the proof gives the exact normal components and their jump.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
18 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
- Jean-Luc Guermond, MATH 661 Fall 2025, Part III Chapter 14: H(div) finite elements (standard reference, not scraped)
- Francisco-Javier Sayas, A gentle introduction to the Finite Element Method (2015) (standard reference, not scraped)