TheoremStatement: AI-adaptedProof: 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 upwind ALE step conserves mass and preserves constants

Statement

For every input satisfying Conservative upwind ALE finite-volume step, the procedure completes after finitely many operations and returns exactly one of mesh_crossing (with no updated state, if some $J_{i}^{n + 1} \leq 0$ ) or success (with a unique updated array, if all $J_{i}^{n + 1} > 0$ ). Whenever it returns success, it preserves total periodic mass, $\sum_{i} J_{i}^{n + 1} {\overset{ˉ}{u}}_{i}^{n + 1} = \sum_{i} J_{i}^{n} {\overset{ˉ}{u}}_{i}^{n}$ . It also preserves every constant state: if ${\overset{ˉ}{u}}_{i}^{n} = U$ for every cell, then ${\overset{ˉ}{u}}_{i}^{n + 1} = U$ for every cell. The mass and constant-state properties require no CFL condition.

Facts & Assumptions

Given: An admissible periodic moving grid, a constant physical speed, cell averages, and the inputs of Conservative upwind ALE finite-volume step.

[F1]

Periodic one-dimensional moving grid: indices are periodic, $J_{i}^{n} = (x_{i + 1 / 2}^{n} - x_{i - 1 / 2}^{n}) / Δ ξ$ , and $c_{i + 1 / 2} = a - w_{i + 1 / 2}$ .

[F2]

Conservative upwind ALE finite-volume step: after computing the finite trial face table it returns mesh_crossing with no state update if any new $J_{i}^{n + 1} \leq 0$ ; otherwise it accepts the trial mesh and returns success with the cell averages defined by $J_{i}^{n + 1} {\overset{ˉ}{u}}_{i}^{n + 1} = J_{i}^{n} {\overset{ˉ}{u}}_{i}^{n} - (Δ t / Δ ξ) ({\hat{F}}_{i + 1 / 2} - {\hat{F}}_{i - 1 / 2})$ , where ${\hat{F}}_{i + 1 / 2} = c_{i + 1 / 2}^{+} {\overset{ˉ}{u}}_{i}^{n} + c_{i + 1 / 2}^{-} {\overset{ˉ}{u}}_{i + 1}^{n}$ .

[F3]

Moving faces satisfy the one-dimensional discrete GCL: $J_{i}^{n + 1} = J_{i}^{n} + (Δ t / Δ ξ) (w_{i + 1 / 2} - w_{i - 1 / 2})$ .

Proof

1.1givenF1F2algebra

By [F1], the input has a finite number $N$ of cells and faces. The algorithm performs a fixed finite number of arithmetic operations and comparisons per cell or face, so its trial face calculation and Jacobian check terminate. If some $J_{i}^{n + 1} \leq 0$ , its specified branch returns mesh_crossing before any state update.

1.2givenF1F2algebra

Sum the update in [F2] over one period. Each face flux occurs once with a plus sign and once with a minus sign, so the periodic flux sum is zero. The remaining identity is $\sum_{i} J_{i}^{n + 1} {\overset{ˉ}{u}}_{i}^{n + 1} = \sum_{i} J_{i}^{n} {\overset{ˉ}{u}}_{i}^{n}$ .

1.3F1F2F3algebra

If every input average equals $U$ , then $c^{+} + c^{-} = c$ gives ${\hat{F}}_{i + 1 / 2} = (a - w_{i + 1 / 2}) U$ . Thus ${\hat{F}}_{i + 1 / 2} - {\hat{F}}_{i - 1 / 2} = - U (w_{i + 1 / 2} - w_{i - 1 / 2})$ . Substituting this in [F2] and using [F3] gives $J_{i}^{n + 1} {\overset{ˉ}{u}}_{i}^{n + 1} = J_{i}^{n + 1} U$ .

2.1F1F2step 1.1algebra

If all checked Jacobians are positive, each update equation in [F2] has the unique solution obtained by dividing its specified right-hand side by $J_{i}^{n + 1} > 0$ . There are finitely many such formulas, and no further failure branch, so the algorithm returns success with exactly this array.

3.1step 2.1step 1.3algebra∎

In the success branch of step 2.1, divide the equality in step 1.3 by $J_{i}^{n + 1} > 0$ to obtain ${\overset{ˉ}{u}}_{i}^{n + 1} = U$ .

Depends on

Used by

Cited to discharge well-definedness by Conservative upwind ALE finite-volume step.

Dependency tree · one level

3 results within one dependency step 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

J. Donea, A. Huerta, J.-Ph. Ponthot, and A. Rodríguez-Ferran, Arbitrary Lagrangian–Eulerian Methods, Encyclopedia of Computational Mechanics, Vol. 1, Chapter 14 (2004) (standard reference, not scraped)