ExampleConstruction: AI-generatedVerification: 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.

A periodic manufactured compressible viscous state

Example

On the one-dimensional periodic domain $T_{2 π}$ , fix $R > 0$ , $γ > 1$ , $μ > 0$ , $ζ \geq 0$ , and $κ > 0$ . Let $ρ (x) = 1$ , $u (x) = 0$ , $T (x) = 2 + \sin x$ , and $E (x) = c_{v} T (x)$ . With forcing $S (x) = (0, R \cos x, κ \sin x)$ in the conservative balance $\partial_{t} U + \partial_{x} F_{1} = \partial_{x} F_{1}^{v i s c} + S$ , these fields form a smooth positive stationary solution. Its pointwise physical entropy production is $κ \cos^{2} x / T (x)^{2}$ , and the forcing contribution closes the periodic mathematical-entropy balance exactly.

Verification

Given: The one-dimensional ideal-gas model, the displayed periodic state, and the forcing $S$ in the balance law.

[F1] Ideal-gas compressible Navier–Stokes–Fourier model: $p = (γ - 1) (E - m^{2} / (2 ρ))$ , $T = p / (R ρ)$ , $F_{1} = (ρ u, ρ u^{2} + p, (E + p) u)$ , and $F_{1}^{v i s c} = (0, τ, u τ + κ \partial_{x} T)$ .

[F2] Smooth ideal-gas Navier–Stokes–Fourier entropy identity: for an unforced smooth positive field, $η_{t} + \partial_{x} (η u + κ T_{x} / T) = - τ u_{x} / T - κ T_{x}^{2} / T^{2}$ .

1.1F1givenalgebra

Since $T (x) \geq 1$ , $ρ = 1$ , $u = 0$ , $m = 0$ , and $E = c_{v} T > 0$ , the state lies in $G$ . The equation of state gives $p = (γ - 1) c_{v} T = R T$ . The stress is zero because $u_{x} = 0$ , so $F_{1} = (0, R T, 0)$ and $F_{1}^{v i s c} = (0, 0, κ \cos x)$ .

2.1F1step 1.1algebra

The state is stationary, so $\partial_{t} U = 0$ . Direct differentiation gives $\partial_{x} F_{1} = (0, R \cos x, 0)$ and $\partial_{x} F_{1}^{v i s c} = (0, 0, - κ \sin x)$ . Therefore $\partial_{x} F_{1}^{v i s c} + S = \partial_{x} F_{1}$ , proving the forced balance componentwise.

3.1F1F2step 1.1step 2.1algebra∎

The physical production is $τ u_{x} / T + κ T_{x}^{2} / T^{2} = κ \cos^{2} x / T^{2}$ . For a source $S$ , multiplying the conservative equation by $v$ adds $v^{T} S$ to the right side of the mathematical-entropy identity [F2]; here $v^{T} S = - κ \sin x / T$ . The left-side entropy flux derivative is $\partial_{x} (κ \cos x / T) = - κ \sin x / T - κ \cos^{2} x / T^{2}$ , which equals minus the production plus $v^{T} S$ . Periodicity removes endpoint contributions.

Depends on

Used by

Nothing in the library uses this result yet.

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)