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.

Properties of the explicit entropy-conservative flux

Statement

The flux in Explicit entropy-conservative two-point Euler flux is well-defined for every pair in $G \times G$ , symmetric in its two states, and consistent in the sense that $F_{j}^{e c} (U, U) = F_{j} (U)$ . It satisfies

$(v (U_{R}) - v (U_{L}))^{T} F_{j}^{e c} (U_{L}, U_{R}) = ψ_{j} (U_{R}) - ψ_{j} (U_{L}) .$

The flux is locally Lipschitz on $G \times G$ .

Facts & Assumptions

Given: $d \geq 1$ and two states $U_{L}, U_{R} \in G$ .

[F1]

Explicit entropy-conservative two-point Euler flux: with $\overset{ˉ}{U} = (U_{L} + U_{R}) / 2$ , $Δ v = v (U_{R}) - v (U_{L})$ , and $Δ ψ_{j} = ψ_{j} (U_{R}) - ψ_{j} (U_{L})$ , use $F_{j} (U_{L})$ when $Δ v = 0$ and otherwise use $F_{j} (\overset{ˉ}{U}) + (Δ ψ_{j} - Δ v^{T} F_{j} (\overset{ˉ}{U})) Δ v / ∥ Δ v ∥^{2}$ .

[F2]

Strict convexity and entropy variables for the ideal-gas Euler flux: $D_{U} v = D_{U}^{2} η$ is positive definite on $G$ , $\nabla_{U} ψ_{j} = (D_{U} v)^{T} F_{j}$ , and $ψ_{j} = v^{T} F_{j} - q_{j}$ .

[F3]

The ideal-gas admissible state set is open and convex: $G$ is open and convex.

Proof

1.1F1F2F3algebra

If $U_{L} = U_{R}$ , then $Δ v = 0$ and [F1] gives $F_{j}^{e c} (U_{L}, U_{R}) = F_{j} (U_{L})$ . If $U_{L} \neq U_{R}$ , convexity [F3] keeps the segment $U (t) = U_{L} + t (U_{R} - U_{L})$ in $G$ , and $Δ v^{T} (U_{R} - U_{L}) = \int_{0}^{1} (U_{R} - U_{L})^{T} D_{U}^{2} η (U (t)) (U_{R} - U_{L}) d t > 0$ by [F2]. Hence $Δ v \neq 0$ , so the denominator in [F1] is nonzero; also $\overset{ˉ}{U} \in G$ . This proves well-definedness and consistency.

1.2F1algebra

Exchanging $U_{L}$ and $U_{R}$ leaves $\overset{ˉ}{U}$ fixed and changes the signs of both $Δ v$ and $Δ ψ_{j}$ . Thus the scalar correction coefficient in [F1] changes sign while its vector factor changes sign, leaving the flux unchanged. The diagonal branch is also symmetric.

1.3F2algebra

Fix a state $X \in G$ and write $U_{R} = X + h / 2$ , $U_{L} = X - h / 2$ for small $h$ . The entropy compatibility in [F2] implies $D_{U} ψ_{j} (X) = F_{j} (X)^{T} D_{U} v (X)$ . Symmetric Taylor expansions therefore give $Δ v = D_{U} v (X) h + O (∣ h ∣^{3})$ and $Δ ψ_{j} = F_{j} (X)^{T} D_{U} v (X) h + O (∣ h ∣^{3})$ , so $N : = Δ ψ_{j} - Δ v^{T} F_{j} (X) = O (∣ h ∣^{3})$ . Positive definiteness of $D_{U} v (X)$ implies $∣ Δ v ∣ \geq c ∣ h ∣$ in a sufficiently small neighborhood of $h = 0$ .

2.1F1step 1.1algebra

When $Δ v \neq 0$ , dotting [F1] with $Δ v$ cancels its denominator and gives $Δ v^{T} F_{j} (\overset{ˉ}{U}) + Δ ψ_{j} - Δ v^{T} F_{j} (\overset{ˉ}{U}) = Δ ψ_{j}$ . When $Δ v = 0$ , step 1.1 gives $U_{L} = U_{R}$ , so both sides are zero.

3.1F1F2step 1.1step 1.3algebra∎

On that neighborhood, the correction $N Δ v / ∣ Δ v ∣^{2}$ is $O (∣ h ∣^{2})$ and tends to zero on the diagonal. Differentiating the symmetric Taylor remainders gives $\partial_{h} N = O (∣ h ∣^{2})$ , $\partial_{X} N = O (∣ h ∣^{3})$ , $\partial_{h} Δ v = O (1)$ , and $\partial_{X} Δ v = O (∣ h ∣)$ . The quotient rule then shows that the correction derivatives are bounded and tend to zero as $h \to 0$ ; its diagonal extension is $C^{1}$ . Away from the diagonal the denominator is nonzero by step 1.1 and the formula is smooth. Thus the flux is locally Lipschitz everywhere on $G \times G$ .

Depends on

Used by

Dependency tree · two levels

4 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

Eitan Tadmor, Entropy Stable Schemes, Chapter 18, Handbook of Numerical Methods for Hyperbolic Problems: Basic and Fundamental Issues, 2016, complete chapter (standard reference, not scraped)
F. Ismail and P. L. Roe, Affordable, entropy-consistent Euler flux functions II: Entropy production at shocks, Journal of Computational Physics 228 (2009), 5410–5436, complete paper (standard reference, not scraped)