LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-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.

A bounded forward-Euler reaction step preserves an inward rectangle

Statement

Let $R = \prod_{i = 1}^{m} [a_{i}, b_{i}]$ be reaction-inward for $F$ from Reaction vector fields and quasi-positivity. Assume for each $i$ there is a coordinate Lipschitz constant $L_{i} \geq 0$ such that $∣ F_{i} (z) - F_{i} (w) ∣ \leq L_{i} ∣ z_{i} - w_{i} ∣$ whenever $z, w \in R$ differ only in coordinate $i$ . Define

τ_{R} = \min_{i : L_{i} > 0} L_{i}^{- 1},

with $τ_{R} = + \infty$ if every $L_{i} = 0$ . For $z \in R$ and $0 \leq τ \leq τ_{R}$ , the forward-Euler reaction step $z^{+} = z + τ F (z)$ lies in $R$ . For every conservation vector $c$ on $R$ , $c^{T} z^{+} = c^{T} z$ ; for every dissipation vector, $c^{T} z^{+} \leq c^{T} z$ .

Facts & Assumptions

Given: An inward rectangle $R$ , coordinate Lipschitz constants $L_{i}$ , a state $z \in R$ , a step $0 \leq τ \leq τ_{R}$ , and a stoichiometric vector $c$ .

[F1]

Inward reaction rectangles: $F_{i} \geq 0$ on the lower face and $F_{i} \leq 0$ on the upper face of $R$ .

[F2]

Stoichiometric conservation and dissipation functionals: $c^{T} F (z) = 0$ or $c^{T} F (z) \leq 0$ throughout $R$ .

[A1]

The coordinate Lipschitz inequalities with constants $L_{i}$ in the Statement hold on $R$ .

Proof

1.1A1F1givenconstruct

Fix coordinate $i$ and keep the other coordinates of $z$ fixed. Let $z^{-}$ replace $z_{i}$ by $a_{i}$ . By [F1], $F_{i} (z^{-}) \geq 0$ ; hence [A1] gives $F_{i} (z) \geq - L_{i} (z_{i} - a_{i})$ . Similarly, let $z^{+}$ replace $z_{i}$ by $b_{i}$ . Then [F1] and [A1] give $F_{i} (z) \leq L_{i} (b_{i} - z_{i})$ .

2.1A1F1step 1.1algebra

If $L_{i} > 0$ , the lower estimate yields $z_{i} + τ F_{i} (z) - a_{i} \geq (1 - τ L_{i}) (z_{i} - a_{i}) \geq 0$ , and the upper estimate yields $b_{i} - z_{i} - τ F_{i} (z) \geq (1 - τ L_{i}) (b_{i} - z_{i}) \geq 0$ . If $L_{i} = 0$ , [A1] makes $F_{i}$ independent of $z_{i}$ on the coordinate interval; its lower and upper face signs force $F_{i} (z) = 0$ . Thus every coordinate of $z^{+}$ lies in its interval.

3.1F2givenalgebra∎

The Euler formula gives $c^{T} z^{+} = c^{T} z + τ c^{T} F (z)$ . Apply [F2] to get equality for a conservation vector and the claimed inequality for a dissipation vector.

Depends on

Used by

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

Willem Hundsdorfer, Numerical Solution of Advection-Diffusion-Reaction Equations, lecture notes for Ph.D. course, 1996 (standard reference, not scraped)