TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-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.

The local Godunov flux is consistent and conservative

Statement

For all equal states $u$ in the local solver neighborhood, $G (u, u) = f (u)$ . For any finite periodic array of length $n \geq 1$ whose adjacent pairs lie in the local flux domain, define the update (indices modulo $n$ ) $U_{j}^{n e w} = U_{j} - ν (G (U_{j}, U_{j + 1}) - G (U_{j - 1}, U_{j})) .$ For any scalar $ν$ , this update using one two-state flux at each interface preserves the sum of cell states.

Facts & Assumptions

Given: The local Riemann solver and Godunov flux definition on a neighborhood of states.

[F1]

Godunov flux from the local Riemann solution: $G (u_{L}, u_{R})$ is the physical flux at $ξ = 0$ of the local self-similar profile, defined by its common one-sided flux if the profile jumps there.

[F2]

Local small-data Riemann solver near a strictly hyperbolic state: equal left/right data have the constant profile $u (ξ) = u$ .

Proof

1.1F1F2algebra

With equal data, uniqueness of the local strength vector gives $σ = 0$ , so [F2] makes the profile constant. Evaluating it at $ξ = 0$ in [F1] gives $G (u, u) = f (u)$ .

2.1givenF1algebra∎

The periodic update in the statement sums to $\sum_{j} U_{j} - ν \sum_{j} (G (U_{j}, U_{j + 1}) - G (U_{j - 1}, U_{j}))$ ; each shared interface flux appears once with coefficient $- ν$ and once with $+ ν$ , so the second sum is zero. This uses the same oriented two-state flux at each interface and asserts no stability or CFL condition.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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

Randall J. LeVeque, Numerical Methods for Conservation Laws (standard reference, not scraped)