Alphabeta Math
TheoremStatement: Literature-sourcedProof: 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.

Semidiscrete cell entropy inequality for Tadmor-dissipative fluxes

Statement

Let (η,q) be a convex entropy pair on an open set A, with entropy variable v and potential ψ as in Convex entropy pairs, entropy variables, and entropy potentials for systems. On a periodic mesh of N≥2 cells of width Δx>0, let differentiable states Ui(t)∈A satisfy U˙i=−Fi+1/2es−Fi−1/2esΔx, where every face flux is the entropy-stable dissipative flux of Entropy-stable flux from positive-semidefinite entropy-variable dissipation. Define q^i+1/2:=(vi+vi+12)TFi+1/2es−ψi+ψi+12. Then each cell satisfies ddtη(Ui)+q^i+1/2−q^i−1/2Δx≤0. Summing over the periodic mesh gives nonincrease of total discrete entropy. This is a semidiscrete result; it asserts no entropy inequality for a chosen fully discrete time integrator.

Facts & Assumptions

Given: A periodic semidiscrete finite-volume system, states in A, a convex entropy pair, and the dissipative flux definition. Prove the local cell entropy inequality.

[F2]

Tadmor entropy-conservative two-point flux: [v]TFec=[ψ] at every face.

[F3]

Entropy-stable flux from positive-semidefinite entropy-variable dissipation: Fes=Fec−12D[v] with D=DT and zTDz≥0.

Proof

1.1givenF2F3algebra

At a face, [F2]–[F3] give [v]TFes=[ψ]−12[v]TD[v]≤[ψ], since [v]TD[v]≥0. This uses only positive semidefiniteness, including the case where the jump or dissipation vanishes.

2.1givenF1F2F3step 1.1algebra

Write [v]i+1/2=vi+1−vi and [ψ]i+1/2=ψi+1−ψi, and use the arithmetic means in the definition of q^. Then −viTFi+1/2es+q^i+1/2=12[v]i+1/2TFi+1/2es−12(ψi+ψi+1) and viTFi−1/2es−q^i−1/2=12[v]i−1/2TFi−1/2es+12(ψi−1+ψi). At equal states the same formula gives q^=q by [F1] and the consistency in [F2], so this is a consistent numerical entropy flux. The right and left interface terms now combine with the entropy-jump defects from step 1.1.

3.1givenF1step 1.1step 2.1algebra∎

By the chain rule and the semidiscrete update, Δxη˙(Ui)=−viTFi+1/2es+viTFi−1/2es. Add q^i+1/2−q^i−1/2 and use step 2.1. The potential terms combine as −12(ψi+ψi+1)+12(ψi−1+ψi)=−12([ψ]i+1/2+[ψ]i−1/2). Hence Δx times the cell residual equals 12([v]i+1/2TFi+1/2es−[ψ]i+1/2)+12([v]i−1/2TFi−1/2es−[ψ]i−1/2), which is nonpositive by step 1.1. This proves the local cell inequality; summing it on the periodic mesh cancels all numerical entropy fluxes. No time discretization was used.

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