Pipeline-generated

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.

✓ 3 results · all verified · 0 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 3 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Elliptic finite-difference methods

1 · Prerequisites

None. This page is self-contained.

2 · Summary

On a rectangular uniform grid, this page defines the five-point Dirichlet Laplacian and a scalar divergence-form flux stencil with midpoint face coefficients. A discrete summation-by-parts identity and a discrete Poincaré estimate give a mesh-uniform inverse bound in the weighted grid $L^{2}$ norm. Taylor expansion with bounded fourth derivatives controls the complete interior residual and yields a second-order error estimate when exact Dirichlet boundary values are imposed. The rate is stated for a smooth solution; nonsmooth weak solutions require a separate approximation argument.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: AI-adaptedProof: Not applicableOpen item page →

Rectangular grid and Dirichlet flux stencil

Definition

Let $L_{x}, L_{y} > 0$ , let $N_{x}, N_{y}$ be integers at least $2$ , and set $h_{x} = L_{x} / N_{x}$ and $h_{y} = L_{y} / N_{y}$ . The rectangular grid nodes are $(x_{i}, y_{j}) = (i h_{x}, j h_{y})$ for $0 \leq i \leq N_{x}$ and $0 \leq j \leq N_{y}$ . The interior index set is $I_{h} = {(i, j) : 1 \leq i < N_{x}, 1 \leq j < N_{y}}$ , and its boundary is the set of grid nodes with $i \in {0, N_{x}}$ or $j \in {0, N_{y}}$ . A grid function is a real-valued function on all grid nodes; $X_{h, 0}$ is the vector space of grid functions that vanish on the boundary.

For real vectors $v, w$ indexed by $I_{h}$ , define the weighted interior inner product and norm by

⟨ v, w ⟩_{h} = h_{x} h_{y} \sum_{i = 1}^{N_{x} - 1} \sum_{j = 1}^{N_{y} - 1} v_{i j} w_{i j}, ∥ v ∥_{h} = ⟨ v, v ⟩_{h}^{1 / 2} .

For full grid functions, the same notation applies to their restrictions to $I_{h}$ ; it gives a semidefinite bilinear form and a seminorm on all grid functions, and an inner product and norm on $X_{h, 0}$ .

The edge differences are $D_{x} v_{i + 1 / 2, j} = (v_{i + 1, j} - v_{i j}) / h_{x}$ for $0 \leq i < N_{x}$ , $1 \leq j < N_{y}$ , and $D_{y} v_{i, j + 1 / 2} = (v_{i, j + 1} - v_{i j}) / h_{y}$ for $1 \leq i < N_{x}$ , $0 \leq j < N_{y}$ . For a scalar coefficient $a$ sampled at face midpoints, write $a_{i + 1 / 2, j} = a (x_{i} + h_{x} / 2, y_{j})$ and $a_{i, j + 1 / 2} = a (x_{i}, y_{j} + h_{y} / 2)$ .

The divergence-form Dirichlet operator on interior nodes is

(A_{h}^{a} v)_{i j} = - \frac{a_{i + 1 / 2, j} D_{x} v_{i + 1 / 2, j} - a_{i - 1 / 2, j} D_{x} v_{i - 1 / 2, j}}{h_{x}} - \frac{a_{i, j + 1 / 2} D_{y} v_{i, j + 1 / 2} - a_{i, j - 1 / 2} D_{y} v_{i, j - 1 / 2}}{h_{y}} .

For $a \equiv 1$ , this is the five-point Dirichlet Laplacian $- D_{x}^{+} D_{x}^{-} - D_{y}^{+} D_{y}^{-}$ . The associated edge energy is

E_{h}^{a} (v, w) = h_{x} h_{y} (\sum_{j = 1}^{N_{y} - 1} \sum_{i = 0}^{N_{x} - 1} a_{i + 1 / 2, j} D_{x} v_{i + 1 / 2, j} D_{x} w_{i + 1 / 2, j} + \sum_{i = 1}^{N_{x} - 1} \sum_{j = 0}^{N_{y} - 1} a_{i, j + 1 / 2} D_{y} v_{i, j + 1 / 2} D_{y} w_{i, j + 1 / 2}) .

The homogeneous scheme solves $A_{h}^{a} v = f_{h}$ in $I_{h}$ with $v = 0$ on the boundary. For Dirichlet data $g$ , it solves the same interior equations with $v = g$ at boundary nodes. This definition specifies the rectangular Dirichlet stencil; it does not specify a Neumann or nonrectangular boundary closure.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

Discrete summation by parts, Poincaré inequality and inverse bound

Statement

On the grid of Rectangular grid and Dirichlet flux stencil, put $q_{i + 1 / 2, j}^{x} = a_{i + 1 / 2, j} D_{x} v_{i + 1 / 2, j}$ and $q_{i, j + 1 / 2}^{y} = a_{i, j + 1 / 2} D_{y} v_{i, j + 1 / 2}$ . For any grid functions $v, w$ ,

⟨ A_{h}^{a} v, w ⟩_{h} = E_{h}^{a} (v, w) - h_{y} \sum_{j = 1}^{N_{y} - 1} (q_{N_{x} - 1 / 2, j}^{x} w_{N_{x}, j} - q_{1 / 2, j}^{x} w_{0, j}) - h_{x} \sum_{i = 1}^{N_{x} - 1} (q_{i, N_{y} - 1 / 2}^{y} w_{i, N_{y}} - q_{i, 1 / 2}^{y} w_{i, 0}) .

In particular, if $w$ vanishes on the boundary, then $⟨ A_{h}^{a} v, w ⟩_{h} = E_{h}^{a} (v, w)$ . For every $v \in X_{h, 0}$ ,

∥ v ∥_{h}^{2} \leq L_{x}^{2} h_{x} h_{y} \sum_{j = 1}^{N_{y} - 1} \sum_{i = 0}^{N_{x} - 1} ∣ D_{x} v_{i + 1 / 2, j} ∣^{2} .

If all horizontal and vertical face values satisfy $a_{i + 1 / 2, j}, a_{i, j + 1 / 2} \geq a_{0} > 0$ , then the homogeneous Dirichlet matrix $A_{h}^{a}$ is invertible and

∥ (A_{h}^{a})^{- 1} ∥_{ℓ_{h}^{2} \to ℓ_{h}^{2}} \leq \frac{L_{x}^{2}}{a_{0}},

where $ℓ_{h}^{2}$ is the norm $∥ \cdot ∥_{h}$ on interior vectors. The constants are independent of $N_{x}, N_{y}$ .

Facts & Assumptions

Given: $L_{x}, L_{y} > 0$ , integers $N_{x}, N_{y} \geq 2$ , the grid, its real grid functions, the inner product, the flux operator $A_{h}^{a}$ , and edge energy $E_{h}^{a}$ defined in Rectangular grid and Dirichlet flux stencil.

[F1]

Rectangular grid and Dirichlet flux stencil: $A_{h}^{a}$ is the negative horizontal and vertical flux divergence; $E_{h}^{a}$ is the weighted sum of the horizontal and vertical edge-gradient products; $X_{h, 0}$ consists of grid functions vanishing on every boundary node.

Proof

1.1givenF1algebra

Fix an interior row $j$ and write $q_{i} = q_{i + 1 / 2, j}^{x}$ . Telescoping the horizontal contribution gives $h_{x} h_{y} \sum_{i = 1}^{N_{x} - 1} - (q_{i} - q_{i - 1}) w_{i j} / h_{x} = h_{y} \sum_{i = 0}^{N_{x} - 1} q_{i} (w_{i + 1, j} - w_{i j}) - h_{y} (q_{N_{x} - 1 / 2, j}^{x} w_{N_{x}, j} - q_{1 / 2, j}^{x} w_{0, j})$ . Summing this identity over $j$ gives the horizontal energy and its two boundary terms.

1.2givenF1algebra

Let $v \in X_{h, 0}$ . For each interior row, $v_{i j} = \sum_{k = 0}^{i - 1} h_{x} D_{x} v_{k + 1 / 2, j}$ . Cauchy–Schwarz gives $∣ v_{i j} ∣^{2} \leq (i h_{x}) \sum_{k = 0}^{i - 1} h_{x} ∣ D_{x} v_{k + 1 / 2, j} ∣^{2} \leq L_{x} \sum_{k = 0}^{N_{x} - 1} h_{x} ∣ D_{x} v_{k + 1 / 2, j} ∣^{2}$ . Summing with weights $h_{x} h_{y}$ and using $\sum_{i = 1}^{N_{x} - 1} h_{x} < L_{x}$ proves the displayed discrete Poincaré inequality.

2.1F1step 1.1algebra

Applying the same telescoping sum in each column to the vertical flux gives the vertical energy minus the top and bottom boundary terms. Adding it to step 1.1 proves the displayed two-dimensional identity, with all four boundary contributions present.

3.1step 2.1givenalgebra

If $w$ vanishes at every boundary node, both boundary sums in step 2.1 are zero, so $⟨ A_{h}^{a} v, w ⟩_{h} = E_{h}^{a} (v, w)$ .

4.1F1step 3.1step 1.2algebra

Apply step 3.1 with $w = v$ . The face lower bound gives $E_{h}^{a} (v, v) \geq a_{0} h_{x} h_{y} \sum_{j, i} ∣ D_{x} v_{i + 1 / 2, j} ∣^{2} \geq (a_{0} / L_{x}^{2}) ∥ v ∥_{h}^{2}$ by step 1.2.

5.1step 4.1algebra

If $A_{h}^{a} v = 0$ for $v \in X_{h, 0}$ , step 4.1 forces $∥ v ∥_{h} = 0$ , hence every interior value is zero; the boundary values already vanish, so $v = 0$ . Thus the square finite-dimensional matrix is injective and therefore invertible.

6.1step 3.1step 4.1step 5.1algebra∎

For $A_{h}^{a} v = f_{h}$ , steps 3.1 and 4.1 imply $(a_{0} / L_{x}^{2}) ∥ v ∥_{h}^{2} \leq ⟨ f_{h}, v ⟩_{h} \leq ∥ f_{h} ∥_{h} ∥ v ∥_{h}$ . If $v = 0$ the claimed estimate is immediate; otherwise divide by $∥ v ∥_{h}$ to obtain $∥ v ∥_{h} \leq (L_{x}^{2} / a_{0}) ∥ f_{h} ∥_{h}$ , which is the asserted inverse-operator bound.

Remarks

No choice axiom is used: the proof uses finite sums, Cauchy–Schwarz, and finite-dimensional injectivity implying surjectivity.

LemmaStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

Second-order consistency of the variable-coefficient flux stencil

Statement

Let $Ω = (0, L_{x}) \times (0, L_{y})$ , $a \in C^{3} (\overline{Ω})$ with $a (x, y) \geq a_{0} > 0$ , and $u \in C^{4} (\overline{Ω})$ . Set $f = - \partial_{x} (a \partial_{x} u) - \partial_{y} (a \partial_{y} u)$ . For $r = 0, 1, 2, 3$ and $s = 1, 2, 3, 4$ , define $A_{r}^{x} = ∥ \partial_{x}^{r} a ∥_{L^{\infty} (Ω)}$ and $U_{s}^{x} = ∥ \partial_{x}^{s} u ∥_{L^{\infty} (Ω)}$ , where $\partial_{x}^{0} a = a$ . Define

C_{x} = \frac{A_{0}^{x} U_{4}^{x}}{24} + \frac{A_{1}^{x} U_{3}^{x}}{12} + \frac{A_{2}^{x} U_{2}^{x}}{16} + \frac{A_{3}^{x} U_{1}^{x}}{48} + L_{x} (\frac{A_{1}^{x} U_{4}^{x}}{48} + \frac{A_{2}^{x} U_{3}^{x}}{48} + \frac{A_{3}^{x} U_{2}^{x}}{96}) + L_{x}^{2} (\frac{A_{2}^{x} U_{4}^{x}}{192} + \frac{A_{3}^{x} U_{3}^{x}}{288}) + L_{x}^{3} \frac{A_{3}^{x} U_{4}^{x}}{1152} .

For $r = 0, 1, 2, 3$ and $s = 1, 2, 3, 4$ , also set $A_{r}^{y} = ∥ \partial_{y}^{r} a ∥_{L^{\infty} (Ω)}$ and $U_{s}^{y} = ∥ \partial_{y}^{s} u ∥_{L^{\infty} (Ω)}$ ; define $C_{y}$ by the same displayed expression with $x, L_{x}, A_{r}^{x}, U_{s}^{x}$ replaced by $y, L_{y}, A_{r}^{y}, U_{s}^{y}$ . If $u_{i j}^{*} = u (x_{i}, y_{j})$ and $f_{h, i j} = f (x_{i}, y_{j})$ , then for every interior node,

∣ (A_{h}^{a} u^{*})_{i j} - f_{h, i j} ∣ \leq 2 C_{x} h_{x}^{2} + 2 C_{y} h_{y}^{2},

where $A_{h}^{a}$ is the exact-midpoint flux stencil of Rectangular grid and Dirichlet flux stencil. The estimate includes every interior row next to the boundary; the Dirichlet boundary samples themselves are imposed exactly.

Facts & Assumptions

Given: The rectangle $Ω$ , $a \in C^{3} (\overline{Ω})$ with $a \geq a_{0} > 0$ , $u \in C^{4} (\overline{Ω})$ , the pointwise equation $f = - \partial_{x} (a \partial_{x} u) - \partial_{y} (a \partial_{y} u)$ , and the rectangular grids of Rectangular grid and Dirichlet flux stencil.

[F1]

Rectangular grid and Dirichlet flux stencil: $A_{h}^{a}$ is the negative difference of adjacent midpoint face fluxes in each coordinate direction, divided by that coordinate's mesh spacing; its face values are sampled at the exact face midpoints.

[A1]

The coordinate derivatives $\partial_{x}^{r} a$ for $0 \leq r \leq 3$ and $\partial_{x}^{s} u$ for $1 \leq s \leq 4$ are continuous and bounded on $\overline{Ω}$ ; the analogous $y$ derivatives are also continuous and bounded.

Proof

1.1givenA1F1algebra

Fix an interior node $(x_{i}, y_{j})$ and write $x = x_{i}$ , $h = h_{x}$ , $A_{r} = A_{r}^{x}$ , and $U_{s} = U_{s}^{x}$ . Taylor's theorem with bounded third derivative for $a$ and bounded fourth derivative for $u$ gives $a (x \pm h / 2, y_{j}) = a \pm h a_{x} / 2 + h^{2} a_{x x} / 8 + R_{a}^{\pm}$ with $∣ R_{a}^{\pm} ∣ \leq A_{3} h^{3} / 48$ , and $D_{+} u = u_{x} + h u_{x x} / 2 + h^{2} u_{x x x} / 6 + R_{u}^{+}$ , $D_{-} u = u_{x} - h u_{x x} / 2 + h^{2} u_{x x x} / 6 + R_{u}^{-}$ with $∣ R_{u}^{\pm} ∣ \leq U_{4} h^{3} / 24$ , where $D_{+} u = (u (x + h, y_{j}) - u (x, y_{j})) / h$ and $D_{-} u = (u (x, y_{j}) - u (x - h, y_{j})) / h$ .

2.1givenA1step 1.1algebra

Multiplying the coefficient and difference expansions yields, with $F_{\pm} = a (x \pm h / 2, y_{j}) D_{\pm} u$ , $F_{\pm} = a u_{x} \pm h (a u_{x x} + a_{x} u_{x}) / 2 + h^{2} (a u_{x x x} / 6 + a_{x} u_{x x} / 4 + a_{x x} u_{x} / 8) + R_{F}^{\pm}$ . The absolute values of the discarded products are bounded by $h^{3} (A_{0} U_{4} / 24 + A_{1} U_{3} / 12 + A_{2} U_{2} / 16 + A_{3} U_{1} / 48) + h^{4} (A_{1} U_{4} / 48 + A_{2} U_{3} / 48 + A_{3} U_{2} / 96) + h^{5} (A_{2} U_{4} / 192 + A_{3} U_{3} / 288) + h^{6} A_{3} U_{4} / 1152$ . Since $h \leq L_{x}$ , this is at most $C_{x} h^{3}$ for the stated $C_{x}$ .

3.1givenstep 2.1algebra

The coefficient of $h^{2}$ in step 2.1 is the same for $F_{+}$ and $F_{-}$ , so it cancels on subtraction. Thus $∣ (F_{+} - F_{-}) / h - \partial_{x} (a \partial_{x} u) (x_{i}, y_{j}) ∣ \leq (∣ R_{F}^{+} ∣ + ∣ R_{F}^{-} ∣) / h \leq 2 C_{x} h_{x}^{2}$ , because $\partial_{x} (a \partial_{x} u) = a_{x} u_{x} + a u_{x x}$ . Interchanging $x$ and $y$ proves the corresponding vertical-flux bound $2 C_{y} h_{y}^{2}$ .

4.1F1givenstep 3.1algebra∎

By [F1], $A_{h}^{a} u^{*}$ is the negative sum of the two discrete flux divergences. The continuous right-hand side $f$ is the negative sum of the matching derivatives. Subtracting these expressions and applying the horizontal and vertical bounds from step 3.1 gives $∣ (A_{h}^{a} u^{*})_{i j} - f_{h, i j} ∣ \leq 2 C_{x} h_{x}^{2} + 2 C_{y} h_{y}^{2}$ at every interior node, including nodes whose stencil touches a boundary value.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passOpen item page →

Second-order grid L2 error for rectangular Dirichlet flux differences

Statement

Let $Ω = (0, L_{x}) \times (0, L_{y})$ , let $a \in C^{3} (\overline{Ω})$ satisfy $a \geq a_{0} > 0$ , and let $u \in C^{4} (\overline{Ω})$ solve $- \partial_{x} (a \partial_{x} u) - \partial_{y} (a \partial_{y} u) = f$ . On each grid from Rectangular grid and Dirichlet flux stencil, impose the exact sampled boundary values $u_{i j}^{*} = u (x_{i}, y_{j})$ and solve $(A_{h}^{a} U_{h})_{i j} = f (x_{i}, y_{j})$ at every interior node. Let $C_{x}, C_{y}$ be the derivative constants of Second-order consistency of the variable-coefficient flux stencil. Then the discrete solution exists uniquely and, with $e_{h} = U_{h} - u^{*}$ ,

∥ e_{h} ∥_{h} \leq \frac{L_{x}^{2}}{a_{0}} \sqrt{L_{x} L_{y}} (2 C_{x} h_{x}^{2} + 2 C_{y} h_{y}^{2}) .

Thus the weighted grid $L^{2}$ error is $O (h_{x}^{2} + h_{y}^{2})$ as both mesh widths tend to zero. This is a pointwise-smooth-solution result; it asserts no error rate for a nonsmooth weak solution.

Facts & Assumptions

Given: $L_{x}, L_{y} > 0$ , $a \in C^{3} (\overline{Ω})$ with $a \geq a_{0} > 0$ , $u \in C^{4} (\overline{Ω})$ satisfying $- \partial_{x} (a \partial_{x} u) - \partial_{y} (a \partial_{y} u) = f$ , and the exact sampled Dirichlet boundary values on every rectangular grid.

[F1]

Rectangular grid and Dirichlet flux stencil: $A_{h}^{a}$ is the negative-divergence operator formed from exact midpoint face coefficients and acts on the interior nodes; $∥ \cdot ∥_{h}$ is the weighted interior grid $L^{2}$ norm.

[F2]

Discrete summation by parts, Poincaré inequality and inverse bound: if every face value is at least $a_{0} > 0$ , the homogeneous Dirichlet matrix is invertible and its inverse has weighted grid $L^{2}$ norm at most $L_{x}^{2} / a_{0}$ .

[F3]

Second-order consistency of the variable-coefficient flux stencil: the sampled exact solution has interior residual bounded pointwise by $2 C_{x} h_{x}^{2} + 2 C_{y} h_{y}^{2}$ .

Proof

1.1givenF1F2algebra

Write $u_{h}^{*} = (u (x_{i}, y_{j}))$ and seek $U_{h} = u_{h}^{*} + e_{h}$ with $e_{h} \in X_{h, 0}$ . The discrete equations are equivalent to $A_{h}^{a} e_{h} = f_{h} - A_{h}^{a} u_{h}^{*}$ on the finite-dimensional zero-boundary space. By [F2], $A_{h}^{a}$ is invertible, so this equation has exactly one solution; hence the Dirichlet scheme has exactly one solution $U_{h}$ .

2.1F1F3step 1.1algebra

Define $τ_{h} = A_{h}^{a} u_{h}^{*} - f_{h}$ . Then the equation for $e_{h}$ is $A_{h}^{a} e_{h} = - τ_{h}$ , and $e_{h} = 0$ at every boundary node because the scheme uses the exact sampled Dirichlet data. By [F3], each interior entry satisfies $∣ τ_{h, i j} ∣ \leq 2 C_{x} h_{x}^{2} + 2 C_{y} h_{y}^{2}$ .

3.1givenF3step 2.1algebra

The weighted sum defining $∥ τ_{h} ∥_{h}^{2}$ has $(N_{x} - 1) (N_{y} - 1)$ terms, so $h_{x} h_{y} (N_{x} - 1) (N_{y} - 1) \leq L_{x} L_{y}$ . Therefore $∥ τ_{h} ∥_{h} \leq \sqrt{L_{x} L_{y}} (2 C_{x} h_{x}^{2} + 2 C_{y} h_{y}^{2})$ .

4.1F2step 2.1step 3.1algebra∎

Apply the inverse estimate [F2] to $A_{h}^{a} e_{h} = - τ_{h}$ and then use step 3.1. This gives the displayed error bound; the derivative constants do not depend on $N_{x}$ or $N_{y}$ , so the error is $O (h_{x}^{2} + h_{y}^{2})$ .

Remarks

No choice axiom is used. The estimates use finite-dimensional coercivity, finite sums, and pointwise Taylor remainders. The published Lax–Milgram and Sobolev–Poincaré pages are continuous-theory context; no continuous weak-solvability theorem is used as a discrete stability result.

5 · Examples, counterexamples and false statements

None yet.

Elliptic finite-difference methods

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

Rectangular grid and Dirichlet flux stencil

Definition

Discrete summation by parts, Poincaré inequality and inverse bound

Statement

Facts & Assumptions

Proof

Remarks

Second-order consistency of the variable-coefficient flux stencil

Statement

Facts & Assumptions

Proof

Second-order grid L2 error for rectangular Dirichlet flux differences

Statement

Facts & Assumptions

Proof

Remarks

5 · Examples, counterexamples and false statements

Sources