LemmaStatement: AI-adaptedProof: AI-generatedPipeline-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.

Centered-difference residual bound with exact Dirichlet closure

Statement

Let $u : [0, 1] \to R$ have four continuous derivatives, with $u (0) = u (1) = 0$ , let $g = - u^{''}$ , and suppose $∣ u^{(4)} (x) ∣ \leq M$ on $[0, 1]$ for a constant $M \geq 0$ . For the grid and matrix of Centered finite differences for the zero-Dirichlet boundary-value problem, put $u_{j} = u (x_{j})$ , $g_{j} = g (x_{j})$ , and $τ_{j} = (A_{h} u_{g r i d})_{j} - g_{j}$ for $1 \leq j \leq N$ . Then

\max_{1 \leq j \leq N} ∣ τ_{j} ∣ \leq \frac{M h^{2}}{12} .

The endpoint closure residuals are exactly zero: $u (0) - 0 = 0$ and $u (1) - 0 = 0$ . If $τ_{0} = τ_{N + 1} : = 0$ records those boundary residuals, then $\max_{0 \leq j \leq N + 1} ∣ τ_{j} ∣ \leq M h^{2} / 12$ as well.

Facts & Assumptions

Given: The regularity, boundary values, differential equation and fourth-derivative bound in the statement; $N \geq 1$ and $h = 1 / (N + 1)$ .

[F1]

Centered finite differences for the zero-Dirichlet boundary-value problem fixes $x_{j} = j h$ , sets $U_{0} = U_{N + 1} = 0$ , and uses $(A_{h} U)_{j} = (- U_{j - 1} + 2 U_{j} - U_{j + 1}) / h^{2}$ for $1 \leq j \leq N$ .

[F2]

A uniform derivative bound gives a uniform Taylor remainder bound: on a closed interval, if $f$ has four derivatives and $∣ f^{(4)} ∣ \leq M$ , its degree-three Taylor remainder satisfies $∣ R_{3, a} f (x) ∣ \leq M ∣ x - a ∣^{4} / 24$ .

[F3]

The triangle inequality: for real $x, y$ , $∣ x + y ∣ \leq ∣ x ∣ + ∣ y ∣$ ; here apply it to the two Taylor remainders.

Proof

1.1givenF1F2choose

The endpoint values of the exact function agree with the algorithm's prescribed endpoint values, so both boundary closure residuals are $0$ . Fix an interior index $j$ . Applying [F2] with center $x_{j}$ and targets $x_{j} - h$ and $x_{j} + h$ gives $u (x_{j} \pm h) = u_{j} \pm h u^{'} (x_{j}) + \frac{h^{2}}{2} u^{''} (x_{j}) \pm \frac{h^{3}}{6} u^{'''} (x_{j}) + R_{\pm}$ , with $∣ R_{\pm} ∣ \leq M h^{4} / 24$ . Both closed intervals lie in $[0, 1]$ , including when $j = 1$ or $j = N$ .

2.1givenF1step 1.1algebra

Substituting these expansions into [F1] cancels the odd derivative terms and gives $(A_{h} u_{g r i d})_{j} = - u^{''} (x_{j}) - (R_{-} + R_{+}) / h^{2}$ . Since $g = - u^{''}$ , it follows that $τ_{j} = - (R_{-} + R_{+}) / h^{2}$ .

3.1F2F3step 1.1step 2.1algebra∎

By [F3] and step 1.1, $∣ τ_{j} ∣ \leq (∣ R_{-} ∣ + ∣ R_{+} ∣) / h^{2} \leq (M h^{4} / 24 + M h^{4} / 24) / h^{2} = M h^{2} / 12$ . This holds for every interior index, and the endpoint residuals from step 1.1 are zero, proving both bounds.

Depends on

Used by

Second-order max-norm error for the centered Dirichlet scheme Theorem

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

Tobin A. Driscoll and Richard J. Braun, Fundamentals of Numerical Computation, author-source revision 2025.01.27, Chapter 10, linear.md (standard reference, not scraped)
Benjamin Seibold, MIT OpenCourseWare 18.336, Lecture 5: Finite Difference Approximation, Spring 2009 (standard reference, not scraped)
Benjamin Seibold, MIT OpenCourseWare 18.336, Lecture 6: General Linear Second Order Equation, Spring 2009 (standard reference, not scraped)