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

The HLL flux follows from the conservative two-wave model

Statement

When SL<0<SR, the HLL intermediate state u∗=SRuR−SLuL−(fR−fL)SR−SL together with the assigned model flux f∗=fL+SL(u∗−uL) satisfies the two model balances f∗−fL=SL(u∗−uL),fR−f∗=SR(uR−u∗). This f∗ is the middle formula in HLL two-wave approximate flux. In general f∗≠f(u∗), even when u∗∈G; the model is not asserted to be a weak solution of the original conservation law. For equal states the HLL flux is consistent. A finite-volume update using the same HLL flux at each periodic interface is conservative: for any finite periodic array with adjacent pairs in the flux domain, define Ujnew=Uj−ν(f^HLL(Uj,Uj+1)−f^HLL(Uj−1,Uj)). Here n≥1. The result holds for any scalar ν and assumes the supplied speeds; it does not prove that they enclose a nonlinear Riemann fan.

Facts & Assumptions

Given: SL<SR, the two states and fluxes, and the HLL two-wave definition.

[F1]

HLL two-wave approximate flux: the speeds and three-branch HLL flux are explicit inputs; the middle formula applies when SL<0<SR.

[F2]

Rankine–Hugoniot jumps and Lax shocks: a physical jump at speed S requires f(uR)−f(uL)=S(uR−uL), using the physical flux at each state.

Proof

1.1givenF1F2algebra

Put D=SR−SL>0. Direct subtraction gives u∗−uL=(SR(uR−uL)−(fR−fL))/D and uR−u∗=(−SL(uR−uL)+(fR−fL))/D. Define f∗=fL+SL(u∗−uL); substitution gives f∗=(SRfL−SLfR+SLSR(uR−uL))/D. Then f∗−fL=SL(u∗−uL) and fR−f∗=SR(uR−u∗), which are the two model balances. They have the algebraic form of [F2], but use the assigned f∗ rather than f(u∗).

2.1step 1.1F1algebra∎

If uL=uR=u, the middle numerator is (SR−SL)f(u), so the middle flux is f(u); the outer branches also equal f(u) when applicable. In a periodic finite-volume sum, each shared interface flux cancels with the opposite sign from the neighboring cell. This proves consistency and conservation without claiming any bound on SL,SR.

Depends on

Used by

Dependency tree · two levels

3 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