LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Element and edge residual representation for P1 Galerkin errors

Statement

Assume Countable Choice, as in the Sobolev and simplex trace suppliers.

Let $T$ be a matching triangular mesh, $U \in V (T)$ , and $u$ solve the weak model from Residual indicators and data oscillation for P1 AFEM. For every $v \in H_{0}^{1} (Ω)$ , $\int_{Ω} \nabla (u - U) \cdot \nabla v + (b \cdot \nabla (u - U)) v = \sum_{K \in T} \int_{K} R_{K} (U) v - \sum_{E i n t e r i o r} \int_{E} J_{E} (U) v .$

Facts & Assumptions

[A1]

Countable Choice is assumed in the cited Sobolev and reference-simplex suppliers (The Axiom of Countable Choice ( ${A C}_{ω}$ )).

Given: Countable Choice, the weak equation, matching affine triangles, continuous P1 function $U$ , and $v \in H_{0}^{1} (Ω)$ .

[F1]

On an affine simplex, Green's identity holds for the polynomial vector field $\nabla U$ and Sobolev test functions; opposite outward normals cancel on a shared matching facet (Sobolev face traces and Gauss–Green on a reference simplex, Interior facet orientations cancel in a matching mesh).

[F2]

$H_{0}^{1}$ is the closure of smooth compactly supported functions, and continuous matching piecewise-affine functions with zero boundary values belong to this space (Zero-boundary Sobolev space as a norm closure, Continuous matching piecewise polynomials belong to W1p, Zero-boundary conforming polynomials lie in W0 1p and satisfy Poincare).

Proof

1.1A1F1given

For smooth compactly supported $v$ , integrate $\int_{K} \nabla U \cdot \nabla v = - \int_{K} Δ U v + \int_{\partial K} (\nabla U \cdot n_{K}) v$ on every cell using [F1]. Since $U ∣_{K}$ is affine, $Δ U = 0$ . The sum of boundary integrals on each interior edge is $\int_{E} J_{E} (U) v$ , and boundary-edge terms vanish because $v$ is compactly supported.

2.1step 1.1givenalgebra

The weak residual is $(f, v) - \int \nabla U \cdot \nabla v - \int (b \cdot \nabla U) v$ . Substituting step 1.1 gives cell integrands $f - b \cdot \nabla U = R_{K} (U)$ and the negative of the summed outward flux jumps. This is the displayed formula for smooth compactly supported $v$ .

3.1A1F1F2step 2.1∎

Smooth compactly supported functions are dense in $H_{0}^{1}$ by its definition. Every term in the identity is continuous in the $H^{1}$ norm: volume terms use $f, \nabla U \in L^{2}$ , and edge terms use the trace inequality from [F1] on the finite mesh. Passing to the limit extends step 2.1 to all $v \in H_{0}^{1}$ .

Depends on

Used by

Dependency tree · two levels

39 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

Ricardo H. Nochetto, Adaptive Finite Element Methods, Lecture 2 (standard reference, not scraped)
Bonito, Canuto, Nochetto & Veeser, Adaptive Finite Element Methods (2024) (standard reference, not scraped)