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.

Smooth ideal-gas Navier–Stokes–Fourier entropy identity

Statement

Let $U$ be a smooth solution with values in $G$ of the unforced balance law in Ideal-gas compressible Navier–Stokes–Fourier model. Then

$\partial_{t} η (U) + \sum_{j = 1}^{d} \partial_{j} (η (U) u_{j} + κ \frac{\partial_{j} T}{T}) = - \sum_{j, k = 1}^{d} (\partial_{j} v)^{T} K_{j k} (U) (\partial_{k} v) = - (\frac{τ : \nabla u}{T} + \frac{κ ∣ \nabla T ∣^{2}}{T^{2}}) \leq 0.$

This is a local smooth identity; it makes no boundary discretization claim.

Facts & Assumptions

Given: A smooth positive state field $U (t, x) \in G$ satisfying the conservative equation, with $η$ , $v$ , $T$ , $q_{j} = η u_{j}$ , and $F_{j}^{v i s c}$ as defined by the preceding items.

[F1]

Ideal-gas compressible Navier–Stokes–Fourier model: $\partial_{t} U + \sum_{j} \partial_{j} F_{j} = \sum_{j} \partial_{j} F_{j}^{v i s c}$ and $F_{j}^{v i s c} = (0, τ_{j \cdot}, u \cdot τ_{j \cdot} + κ \partial_{j} T)$ .

[F2]

Strict convexity and entropy variables for the ideal-gas Euler flux: $\partial_{t} η + \sum_{j} \partial_{j} q_{j} = v^{T} (\partial_{t} U + \sum_{j} \partial_{j} F_{j})$ for smooth fields.

[F3]

Positive-semidefinite entropy-variable factorization of viscous flux: $F_{j}^{v i s c} = \sum_{k} K_{j k} \partial_{k} v$ and the corresponding quadratic sum is $τ : \nabla u / T + κ ∣ \nabla T ∣^{2} / T^{2} \geq 0$ .

Proof

1.1F1F2givenalgebra

By [F2] and the balance law [F1], $\partial_{t} η + \sum_{j} \partial_{j} q_{j} = v^{T} \sum_{j} \partial_{j} F_{j}^{v i s c} = \sum_{j} \partial_{j} (v^{T} F_{j}^{v i s c}) - \sum_{j} (\partial_{j} v)^{T} F_{j}^{v i s c}$ . The second equality is the product rule applied componentwise to each finite-dimensional flux vector.

2.1F1F2F3step 1.1algebra∎

From the explicit entropy variables in [F2] and viscous flux in [F1], the momentum and stress-work terms cancel pointwise: $v^{T} F_{j}^{v i s c} = (T^{- 1} u) \cdot τ_{j \cdot} - T^{- 1} (u \cdot τ_{j \cdot} + κ \partial_{j} T) = - κ \frac{\partial_{j} T}{T}$ . Substitution into step 1.1 and the factorization identity [F3] gives the displayed local balance and its nonpositive right-hand side.

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

Pablo Fernandez, Ngoc-Cuong Nguyen, and Jaime Peraire, Entropy-stable hybridized discontinuous Galerkin methods for the compressible Euler and Navier-Stokes equations, complete author preprint (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)