TheoremStatement: 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.

MUSCL/minmod face states are second order on smooth monotone data

Statement

Let $u \in C^{2}$ on a neighborhood of a cell and its two neighbors, and suppose $∣ u^{'} (x) ∣ \geq c > 0$ there. Let $U_{j}$ be the averages of $u$ over uniform cells of width $h$ , centered at $x_{j} = x_{0} + j h$ . For sufficiently small $h$ , the MUSCL/minmod face states of Finite-volume MUSCL, nodal ENO2 and WENO5 reconstruction conventions satisfy $∣ U_{i} + h s_{i} / 2 - u (x_{i} + h / 2) ∣ \leq C h^{2}, ∣ U_{i} - h s_{i} / 2 - u (x_{i} - h / 2) ∣ \leq C h^{2},$ where $C$ depends only on $c$ and a bound for $∣ u^{''} ∣$ on the stated neighborhood.

Facts & Assumptions

Given: The stated smoothness and nonvanishing derivative, uniform cell averages, and minmod MUSCL slopes.

[F1]

Finite-volume MUSCL, nodal ENO2 and WENO5 reconstruction conventions: $h s_{i} = minmod (U_{i} - U_{i - 1}, U_{i + 1} - U_{i})$ and the two face states are $U_{i} \pm h s_{i} / 2$ .

[F2]

A uniform derivative bound gives a uniform Taylor remainder bound: with $∣ u^{''} ∣ \leq M_{2}$ , the degree-one Taylor remainder at distance $r$ is bounded by $M_{2} ∣ r ∣^{2} / 2$ .

Proof

1.1givenF2algebra

Let $M_{2} = \sup ∣ u^{''} ∣$ on the cell and its neighbors. Applying [F2] about $x_{i}$ and averaging over the symmetric central cell cancels the linear term, giving $∣ U_{i} - u (x_{i}) ∣ \leq M_{2} h^{2} / 24$ . Applying [F2] at $x_{i}$ to the neighboring centers and using the same cell-average estimate gives $U_{i} - U_{i - 1} = h u^{'} (x_{i}) + O (M_{2} h^{2})$ and $U_{i + 1} - U_{i} = h u^{'} (x_{i}) + O (M_{2} h^{2})$ .

2.1F1step 1.1algebra

Because $∣ u^{'} (x_{i}) ∣ \geq c$ , both increments in step 1.1 have the same nonzero sign for all sufficiently small $h$ . Minmod selects one of them, and either equals $h u^{'} (x_{i}) + O (M_{2} h^{2})$ ; hence $h s_{i} = h u^{'} (x_{i}) + O (M_{2} h^{2})$ .

3.1F2step 1.1step 2.1algebra∎

By step 1.1 and step 2.1, $U_{i} + h s_{i} / 2 = u (x_{i}) + h u^{'} (x_{i}) / 2 + O (M_{2} h^{2})$ . Applying [F2] at distance $h / 2$ gives $u (x_{i} + h / 2) = u (x_{i}) + h u^{'} (x_{i}) / 2 + O (M_{2} h^{2})$ , so subtraction proves the right-face estimate. The same calculation with $- h / 2$ proves the left-face estimate.

Depends on

Used by

MUSCL and WENO reconstruct a translating affine profile exactly Example

Dependency tree · two levels

7 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

Jérôme Droniou, A Beginner’s Course in Finite Volume Approximation of Scalar Conservation Laws, complete lecture notes (standard reference, not scraped)