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.

CFL monotonicity and weighted L1 contraction for the ALE step

Statement

Suppose the step of Conservative upwind ALE finite-volume step succeeds and, for every cell,

$\frac{Δ t}{Δ ξ} ((c_{i + 1 / 2}^{n})^{+} - (c_{i - 1 / 2}^{n})^{-}) \leq J_{i}^{n} .$

Then the update is monotone, maps nonnegative cell averages to nonnegative cell averages, and for any two input arrays $U, V$ with outputs $U^{'}, V^{'}$ it satisfies

$\sum_{i} J_{i}^{n + 1} ∣ U_{i}^{'} - V_{i}^{'} ∣ \leq \sum_{i} J_{i}^{n} ∣ U_{i} - V_{i} ∣ .$

Facts & Assumptions

Given: A periodic moving grid, the successful upwind ALE step, and the stated cellwise CFL inequalities.

[F1]

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

[F2]

Conservative upwind ALE finite-volume step: the update is linear in the input averages and uses the relative-speed upwind flux, provided every $J_{i}^{n + 1} > 0$ .

[F3]

The upwind ALE step conserves mass and preserves constants: every successful step conserves weighted mass for arbitrary inputs and preserves constant input arrays.

Proof

1.1givenF1F2algebra

Put $μ = Δ t / Δ ξ$ . Expanding the flux difference in [F2] gives $J_{i}^{n + 1} U_{i}^{'} = μ (c_{i - 1 / 2}^{n})^{+} U_{i - 1} + [J_{i}^{n} - μ ((c_{i + 1 / 2}^{n})^{+} - (c_{i - 1 / 2}^{n})^{-})] U_{i} - μ (c_{i + 1 / 2}^{n})^{-} U_{i + 1}$ . The first and third coefficients are nonnegative by the sign definitions of positive and negative parts; the middle coefficient is nonnegative by the CFL condition.

2.1F2F3step 1.1algebra

Divide by the positive $J_{i}^{n + 1}$ from success. The resulting matrix $P$ has nonnegative entries, so $U \leq V$ componentwise implies $P U \leq P V$ , and $U \geq 0$ implies $P U \geq 0$ . By [F3], the update preserves constants, hence every row of $P$ sums to $1$ .

3.1F3step 2.1algebra∎

For each coordinate vector $e_{j}$ , mass conservation in [F3] gives $\sum_{i} J_{i}^{n + 1} P_{i j} = J_{j}^{n}$ . Linearity and nonnegativity now imply $\sum_{i} J_{i}^{n + 1} ∣ U_{i}^{'} - V_{i}^{'} ∣ = \sum_{i} J_{i}^{n + 1} ∣ (P (U - V))_{i} ∣ \leq \sum_{j} (\sum_{i} J_{i}^{n + 1} P_{i j}) ∣ U_{j} - V_{j} ∣ = \sum_{j} J_{j}^{n} ∣ U_{j} - V_{j} ∣$ . This is the asserted weighted $L^{1}$ contraction.

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

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)