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.

The selected nodal ENO2 quadratic reconstructs the face to third order

Statement

Let $h > 0$ , let $y_{j} = j h$ , and let $u \in C^{3} ([y_{i - 1}, y_{i + 2}])$ with $M : = \sup ∣ u^{'''} ∣ < \infty$ . Form the nodal ENO2 value at $y_{i + 1 / 2}$ by the rule in Finite-volume MUSCL, nodal ENO2 and WENO5 reconstruction conventions. Then $∣ U_{i + 1 / 2}^{E N O 2} - u (y_{i + 1 / 2}) ∣ \leq M h^{3} / 16.$ The conclusion holds for either selected triple, so it includes the left-tie case.

Facts & Assumptions

Given: Uniform distinct nodes $y_{j} = j h$ , nodal values $U_{j} = u (y_{j})$ from a C3 function, and the ENO2 selector and Newton quadratic.

[F1]

Finite-volume MUSCL, nodal ENO2 and WENO5 reconstruction conventions: ENO2 compares the absolute divided differences on $(y_{i - 1}, y_{i}, y_{i + 1})$ and $(y_{i}, y_{i + 1}, y_{i + 2})$ , chooses the smaller (ties left), and evaluates the corresponding Newton quadratic at $y_{i + 1 / 2}$ .

[F2]

Existence and uniqueness of the cardinal-polynomial interpolant: for distinct real nodes, the data have a unique interpolating polynomial of degree at most the number of nodes minus one.

[F3]

Pointwise Lagrange interpolation remainder: for three distinct nodes and $u \in C^{3}$ , the quadratic interpolant error at a non-node $x$ is $u^{'''} (ξ) (x - y_{a}) (x - y_{b}) (x - y_{c}) / 3!$ for some $ξ$ between the nodes and $x$ .

Proof

1.1givenF1F2algebra

For either candidate triple $y_{a} < y_{b} < y_{c}$ , let $D_{a b} = (U_{b} - U_{a}) / (y_{b} - y_{a})$ and $D_{b c} = (U_{c} - U_{b}) / (y_{c} - y_{b})$ . The Newton polynomial in [F1] takes values $U_{a}$ and $U_{b}$ at the first two nodes. At $y_{c}$ , its value is $U_{a} + D_{a b} (y_{c} - y_{a}) + (D_{b c} - D_{a b}) (y_{c} - y_{b}) = U_{b} + D_{b c} (y_{c} - y_{b}) = U_{c}$ , using the divided-difference definition. By [F2] it is the unique quadratic interpolant to that triple.

1.2givenF3algebra

Apply [F3] to the left triple. The offsets from $y_{i + 1 / 2}$ are $- 3 h / 2, - h / 2, h / 2$ , whose product has magnitude $3 h^{3} / 8$ ; hence the error is at most $M (3 h^{3} / 8) / 6 = M h^{3} / 16$ . For the right triple the offsets are $- h / 2, h / 2, 3 h / 2$ , with the same product magnitude, so it has the same bound.

2.1F1step 1.2∎

The selector in [F1] returns one of those two quadratics, including the left one at a tie. Since both candidates satisfy the bound from step 1.2, whichever is selected satisfies it.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

17 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

Chi-Wang Shu, Essentially Non-Oscillatory and Weighted Essentially Non-Oscillatory Schemes for Hyperbolic Conservation Laws, complete lecture notes (standard reference, not scraped)