Alphabeta Math
ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck pass
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.

Exact Tadmor entropy residual for a dissipative Burgers flux

Example

For Burgers' flux f(u)=u2/2 and entropy η(u)=u2/2, the entropy flux is q(u)=u3/3 and the entropy potential is ψ(u)=u3/6. The symmetric two-point flux fec(uL,uR)=uL2+uLuR+uR26 is entropy-conservative. Adding unit dissipation in entropy variables gives fes=fec−(uR−uL)/2; at the jump 1→0 its Tadmor entropy residual is exactly −1/2.

Facts & Assumptions

Given: Burgers' flux, the quadratic entropy pair, and the two-point flux formula. Verify compatibility, the entropy-conservative identity, and the dissipative residual at (uL,uR)=(1,0).

[F1]

Convex entropy pairs, entropy variables, and entropy potentials for systems: an entropy pair satisfies q′=η′f′, with v=η′ and ψ=vf−q.

[F2]

Tadmor entropy-conservative two-point flux: a continuous, consistent, symmetric two-point flux is entropy-conservative when [v]fec=[ψ] for every pair of states, with right-minus-left jumps.

[F3]

Entropy-stable flux from positive-semidefinite entropy-variable dissipation: fes=fec−D[v]/2 for symmetric positive-semidefinite D.

Verification

1.1givenF1algebra

Here η′′(u)=1, η′(u)=u, and q′(u)=u2=η′(u)f′(u), so this is a convex entropy pair. Thus v=u and ψ=uf−q=u3/6 by [F1].

2.1givenF1F2step 1.1algebra

The displayed fec is polynomial, hence continuous, is symmetric, and satisfies fec(u,u)=u2/2=f(u). Moreover, (uR−uL)fec(uL,uR)=uR3−uL36=ψ(uR)−ψ(uL), so [F2] applies using ψ=u3/6 from step 1.1.

3.1givenF2F3step 2.1algebra∎

Taking D=1 in [F3], at (1,0) we have fec=1/6, [v]=−1, and [ψ]=−1/6. Therefore [v]fes−[ψ]=(−1)(1/6+1/2)−(−1/6)=−1/2. In general the same substitution gives residual −12(uR−uL)2≤0, using the formula in step 2.1.

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