ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedprecheck 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 broken P1 test exposes a nonzero consistency residual

Example

Assume Countable Choice. Encode a one-dimensional zero-boundary function by its derivative. The exact Hilbert space is the mean-zero subspace $V : = {g \in L^{2} (0, 1) : \int_{0}^{1} g = 0}$ , with $a (g, h) = \int_{0}^{1} g h$ . Its associated function is $U_{g} (x) : = \int_{0}^{x} g (t) d t$ . The source functional is $F (h) : = \int_{0}^{1} 6 x U_{h} (x) d x$ . Its exact solution is $g_{u} (x) = 1 - 3 x^{2}$ , whose associated function is $U_{g_{u}} (x) = x - x^{3}$ .

For the nonconforming discrete space, take broken piecewise-affine functions on the disjoint cells $[0, 1 / 2]$ and $(1 / 2, 1]$ that vanish at $0$ and $1$ , with no continuity imposed at $1 / 2$ . Identify each such function with its two cellwise slopes, a two-dimensional space $V_{h}$ of piecewise-constant fields. For $ω_{h} = s_{L} 1_{[0, 1 / 2]} + s_{R} 1_{(1 / 2, 1]}$ , define its associated broken function by $U_{ω_{h}} (x) = s_{L} x$ for $0 \leq x \leq 1 / 2$ and $U_{ω_{h}} (x) = s_{R} (x - 1)$ for $1 / 2 < x \leq 1$ . Thus the midpoint value is assigned by the left cell; cellwise derivatives and all integrals are unchanged by this representative convention. Use ${\tilde{a}}_{h} (g, ω_{h}) : = \int_{0}^{1} g ω_{h}$ and $F_{h} (ω_{h}) : = \int_{0}^{1} 6 x U_{ω_{h}} (x) d x$ . The left basis function $ϕ_{L} (x) = 2 x$ on the first cell and $0$ on the second corresponds to slope field $ω_{L} = 21_{[0, 1 / 2]}$ ; it has residual $F_{h} (ω_{L}) - {\tilde{a}}_{h} (g_{u}, ω_{L}) = - 1 / 4$ . Thus the exact solution does not satisfy the broken discrete equation on $V_{h}$ : its consistency residual is nonzero. This is the term retained by the second Strang estimate in place of an exact Galerkin identity. The conforming Céa hypothesis $V_{h} \subseteq V$ is also false.

Facts & Assumptions

Given: Countable Choice; $L^{2} (0, 1)$ with its integral inner product; the mean-zero subspace $V$ ; the exact and broken forms and loads in the Example; and the broken basis functions $ϕ_{L} (x) = 2 x$ on the first cell and $0$ on the second, and $ϕ_{R} (x) = 0$ on the first cell and $2 (x - 1)$ on the second.

[F1]

$L^{2}$ with the integral pairing is a Hilbert space and Hilbert space: under Countable Choice, $L^{2} (0, 1)$ is a Hilbert space for the integral pairing; a complete inner-product space is a Hilbert space.

[F2]

Holder's inequality for integrals, including the endpoint cases: $\int_{0}^{1} ∣ g ∣ \leq ∥ g ∥_{2}$ , and $∣ \int f g ∣ \leq ∥ f ∥_{2} ∥ g ∥_{2}$ .

[F3]

Two integrable functions are equal almost everywhere exactly when all of their indefinite integrals agree: the primitive $U_{g} (x) = \int_{0}^{x} g (t) d t$ is independent of the representative of the $L^{2}$ class $g$ .

[F4]

Tonelli and Fubini for the completed product, with only almost-everywhere section measurability: under Countable Choice, absolutely integrable functions on the product have equal iterated integrals.

[F5]

The Lax--Milgram theorem under The Axiom of Countable Choice ( ${A C}_{ω}$ ): a bounded coercive form on a Hilbert space with bounded load has a unique variational solution.

[F6]

Second Strang estimate with a bounded extension to the comparison space: a bounded extension to $V + V_{h}$ and a coercive discrete form yield an error estimate with the exact-solution consistency residual.

[F7]

Céa quasi-optimality for coercive conforming Galerkin problems: its conforming hypothesis is $V_{h} \subseteq V$ .

[F8]

The reals are complete: every Cauchy sequence of real numbers has a real limit.

[F9]

The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ and For a natural $n \geq 1$ the function $x \mapsto x^{n}$ is differentiable everywhere with derivative $ι (n) x^{n - 1}$ ; for $n = 0$ it is the constant $1$ , with derivative $0$ ; for a natural $n \geq 1$ the function $x \mapsto x^{- n}$ is differentiable at every $x \neq 0$ with derivative $- ι (n) x^{- n - 1}$ ; consequently every polynomial function is differentiable at every real, with the derivative computed term by term: the displayed polynomial integrals are evaluated by explicit antiderivatives and the fundamental theorem of calculus.

[F10]

Under Countable Choice, $λ_{1} ([0, 1]) = 1$ and every interval has Lebesgue measure equal to its length (A box in $R^{n}$ with parameters $a_{i} \leq b_{i}$ is Lebesgue measurable of measure $\prod_{i < n} (b_{i} - a_{i})$ , whichever of its faces are included, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F11]

Under Countable Choice, a bounded Riemann-integrable function on a closed interval is Lebesgue integrable and the two integrals agree (A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral, The Axiom of Countable Choice ( ${A C}_{ω}$ )).

[F12]

The Lebesgue integral is linear on $L^{1}$ (The Lebesgue integral is linear on $L^{1} (μ)$ ).

[F13]

Continuous functions on closed intervals are Riemann integrable; changing finitely many values preserves integrability and the integral; and the Riemann integral is additive over adjacent intervals (A continuous function on $[a, b]$ is Riemann integrable, by Heine-Cantor and Riemann's criterion, Changing an integrable function at finitely many points changes neither its integrability nor its integral, For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ ).

[A1]

The exact solution candidate is $g_{u} (x) = 1 - 3 x^{2}$ and its associated function is $U_{g_{u}} (x) = x - x^{3}$ .

[A2]

$V_{h} = span {ω_{L}, ω_{R}}$ with $ω_{L} = 21_{[0, 1 / 2]}$ and $ω_{R} = 21_{(1 / 2, 1]}$ . Its norm is $∥ ω_{h} ∥_{h} = ∥ ω_{h} ∥_{L^{2}}$ , and ${\tilde{a}}_{h} (g, ω_{h}) = \int_{0}^{1} g ω_{h}$ .

Verification

1.1F1F2F10F12givenalgebra

The functional $L (g) : = \int_{0}^{1} g$ is linear by [F12] and bounded by [F2], since $∥ 1 ∥_{2} = 1$ by [F10]. Thus $V = \ker L$ is a closed linear subspace of $L^{2}$ . If $(g_{n})$ is Cauchy in $V$ , [F1] gives an $L^{2}$ limit $g$ ; continuity of $L$ gives $L (g) = 0$ , so $g \in V$ . Hence $V$ is a Hilbert space.

1.2A2F2F6F8F9F10F11F13algebra

For $ω_{h} = c_{L} ω_{L} + c_{R} ω_{R}$ , [F10, F11, F13] give $∥ ω_{h} ∥_{h}^{2} = \int_{0}^{1} ∣ ω_{h} ∣^{2} = 2 (c_{L}^{2} + c_{R}^{2})$ and $∥ U_{ω_{h}} ∥_{2}^{2} = (c_{L}^{2} + c_{R}^{2}) / 6 = ∥ ω_{h} ∥_{h}^{2} / 12$ , by integrating the bounded piecewise-polynomial representatives. They also give $∥ 6 x ∥_{2}^{2} = \int_{0}^{1} 36 x^{2} d x = 12$ . A Cauchy sequence in $V_{h}$ therefore has Cauchy coefficient sequences; [F8] gives their limits and the same norm formula gives convergence in $V_{h}$ . Thus $V_{h}$ is a two-dimensional Hilbert space. Moreover, $ω_{L} + ω_{R} = 2$ is constant, and every $g \in L^{2} (0, 1)$ decomposes as $g = (g - \int_{0}^{1} g) + \frac{1}{2} (\int_{0}^{1} g) (ω_{L} + ω_{R})$ ; the first summand lies in $V$ and the second in $V_{h}$ . Thus $X_{h} = V + V_{h} = L^{2} (0, 1)$ , with the common $L^{2}$ norm restricting to both spaces. The discrete form has coercivity constant $1$ , and the extension ${\tilde{a}}_{h} (g, ω_{h}) = \int g ω_{h}$ is bounded by [F2]. Holder [F2] and the displayed finite $L^{2}$ norms show $F_{h} (ω_{h}) = \int_{0}^{1} 6 x U_{ω_{h}} (x) d x$ is bounded. Hence the stability and bounded-extension hypotheses of [F6] hold.

2.1A1F2F3F4F5F9F10F11F12step 1.1step 1.2algebra

The polynomial $g_{u} = 1 - 3 x^{2}$ has Lebesgue integral zero by [F9, F11], so $g_{u} \in V$ , and its primitive is $U_{g_{u}} = x - x^{3}$ . By [F2], $∣ U_{h} (x) ∣ \leq ∥ h ∥_{2}$ , hence $∥ U_{h} ∥_{2} \leq ∥ h ∥_{2}$ using [F10]. Since $∥ 6 x ∥_{2}^{2} = 12$ by step 1.2, Holder [F2] bounds $F (h) = \int_{0}^{1} 6 x U_{h} (x) d x$ for $h \in V$ ; [F3] makes the primitive representative-independent. The function $(x, t) \mapsto 6 x h (t) 1_{0 \leq t \leq x \leq 1}$ is absolutely integrable, with absolute integral at most $6 ∥ h ∥_{1} \leq 6 ∥ h ∥_{2}$ . Fubini [F4] gives $F (h) = \int_{0}^{1} h (t) 3 (1 - t^{2}) d t$ . Linearity [F12] and $\int h = 0$ yield $F (h) = \int_{0}^{1} h (t) (1 - 3 t^{2}) d t = a (g_{u}, h)$ . The form is the $L^{2}$ inner product, hence bounded and coercive, so [F5] confirms the unique exact solution is $g_{u}$ .

2.2A1A2F9F11F13step 1.2algebra

The associated broken function for $ω_{L}$ is $ϕ_{L}$ . By [F9, F11, F13], $F_{h} (ω_{L}) = \int_{0}^{1 / 2} 12 x^{2} d x = 1 / 2$ , whereas ${\tilde{a}}_{h} (g_{u}, ω_{L}) = \int_{0}^{1 / 2} 2 (1 - 3 x^{2}) d x = 2 [x - x^{3}]_{0}^{1 / 2} = 3 / 4$ . The residual is $- 1 / 4$ and $∥ ω_{L} ∥_{h} = \sqrt{2}$ , so $δ_{h}^{n c} (g_{u}) \geq 1 / (4 \sqrt{2}) > 0$ .

3.1F6F7step 2.2∎

The slope field $ω_{L}$ has integral $1$ , so $ω_{L} \notin V$ and $V_{h} ⊈ V$ . Thus the conforming hypothesis in [F7] fails; independently, step 2.2 shows that the exact solution does not satisfy the discrete equation on $V_{h}$ . This is the consistency term retained by [F6].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

130 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 VI, Chapter 27, Error analysis with variational crimes (standard reference, not scraped)
Joachim Schöberl, Numerical Methods for Partial Differential Equations, Chapter 25, Non-conforming Finite Element Methods (standard reference, not scraped)