ExampleConstruction: Literature-sourcedVerification: 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.

Lax–Friedrichs flux under the invariant-interval CFL bound

Example

Assume ${A C}_{ω}$ , and additionally assume Dependent Choice $D C$ when $u_{0} \in L^{1} (R)$ .

Let $I = [a_{-}, a_{+}]$ be a compact invariant interval, let $f \in C^{1} (R)$ , and choose finite $L, α$ with $∣ f^{'} (s) ∣ \leq L$ on $I$ and $α \geq L$ . The Lax–Friedrichs flux $F_{L F} (a, b) : = \frac{f (a) + f (b)}{2} - \frac{α}{2} (b - a)$ is consistent, nondecreasing in $a$ , nonincreasing in $b$ , and has coordinate Lipschitz bounds $L_{1} = L_{2} = (L + α) / 2$ . Thus any bounded BV datum in $I$ and mesh family satisfying $\frac{τ_{m}}{h_{m}} (L + α) \leq 1, \frac{τ_{m}}{h_{m}} \geq c_{*} > 0, h_{m}, τ_{m} \to 0$ falls under Strong entropy convergence of monotone finite-volume schemes.

Facts & Assumptions

Given: Countable Choice ${A C}_{ω}$ , the compact interval $I$ , $f \in C^{1}$ , constants $L, α$ with $∣ f^{'} ∣ \leq L \leq α$ on $I$ , bounded BV data $u_{0}$ in $I$ , and the displayed numerical flux; additionally assume Dependent Choice $D C$ when $u_{0} \in L^{1} (R)$ .

[F1]

A continuous real-valued function on a compact interval is bounded, so a finite $L$ exists for $∣ f^{'} ∣$ on $I$ (A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value).

[F2]

If $f$ is continuous on $[a, b]$ and differentiable on $(a, b)$ , then $f (b) - f (a) = f^{'} (c) (b - a)$ for some $c \in (a, b)$ (The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

[F3]

The full invariant-interval CFL condition uses the sum of coordinate Lipschitz bounds, and under ${A C}_{ω}$ —with DC additionally on the $L^{1}$ branch—the convergence theorem requires a positive lower bound for $τ / h$ (Monotone finite-volume scheme and invariant-interval CFL, The Axiom of Countable Choice ( ${A C}_{ω}$ ), The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain, Strong entropy convergence of monotone finite-volume schemes).

[F4]

$u_{0} \in {B V}_{b} (R)$ is bounded and has finite translation variation (Bounded BV data on the real line).

Verification

1.1F1F2givenalgebra

On the diagonal, $F_{L F} (s, s) = f (s)$ , so the flux is consistent. If $a_{2} = a_{1}$ , the first-coordinate difference is zero; if $a_{2} > a_{1}$ , the mean-value theorem gives $F_{L F} (a_{2}, b) - F_{L F} (a_{1}, b) = \frac{f (a_{2}) - f (a_{1}) + α (a_{2} - a_{1})}{2} \geq \frac{α - L}{2} (a_{2} - a_{1}) \geq 0.$ Thus it is nondecreasing in its first coordinate.

1.2F1F2givenalgebra

If $b_{2} = b_{1}$ , the second-coordinate difference is zero; if $b_{2} > b_{1}$ , the mean-value theorem gives $F_{L F} (a, b_{2}) - F_{L F} (a, b_{1}) = \frac{f (b_{2}) - f (b_{1}) - α (b_{2} - b_{1})}{2} \leq - \frac{α - L}{2} (b_{2} - b_{1}) \leq 0,$ so it is nonincreasing in its second coordinate. The mean-value bounds on each variable also give $L_{1} = L_{2} = (L + α) / 2$ .

2.1F1F2F3F4step 1.1step 1.2algebra∎

Since $f$ is locally Lipschitz and the flux adds a linear term, $F_{L F}$ is locally Lipschitz. The displayed flux is consistent by its diagonal formula, and steps 1.1 and 1.2 prove monotonicity with coordinate bounds whose sum is $L + α$ . Hence the displayed upper ratio gives the full CFL condition, while the lower ratio and bounded BV data satisfy the remaining hypotheses of [F3]. The convergence theorem applies.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

58 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 note (standard reference, not scraped)
Siddhartha Mishra, Ulrik S. Fjordholm and Rémi Abgrall, Numerical Methods for Conservation Laws, ETH lecture notes (standard reference, not scraped)