TheoremStatement: 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.

Inward reaction fields preserve rectangles and stoichiometric mass

Statement

Let $R = \prod_{i = 1}^{m} [a_{i}, b_{i}]$ be the reaction-inward rectangle of Inward reaction rectangles. Assume $F$ from Reaction vector fields and quasi-positivity is continuously differentiable on an open neighborhood of $R$ , and its derivative is bounded on some closed neighborhood of $R$ . For any $z_{0} \in R$ , the IVP $z^{'} = F (z)$ has a unique solution for every $t \geq 0$ , and $z (t) \in R$ . If $c$ is a conservation vector on $R$ , then $c^{T} z (t) = c^{T} z_{0}$ ; if it is a dissipation vector, then $c^{T} z (t)$ is nonincreasing. When every $a_{i} = 0$ , quasi-positivity implies the lower-face condition on $R$ ; upper-face inwardness remains a separate hypothesis.

Facts & Assumptions

Given: A compact rectangle $R$ , a $C^{1}$ reaction field on a neighborhood with bounded derivative there, inward signs on every lower and upper face, and a stoichiometric vector $c$ on $R$ .

[F1]

Inward reaction rectangles: the rectangle is reaction-inward exactly when the lower-face signs are $F_{i} \geq 0$ and upper-face signs are $F_{i} \leq 0$ .

[F2]

Stoichiometric conservation and dissipation functionals: $c^{T} F = 0$ on $R$ for conservation, or $c^{T} F \leq 0$ on $R$ for dissipation.

[F3]

Picard-Lindelöf local existence and uniqueness for first-order systems: a continuous field locally Lipschitz in the state variable has a unique local solution through each point of its open domain.

[F4]

Every Picard–Lindelöf initial value problem has one maximal solution on an open interval: a Picard–Lindelöf IVP has a unique maximal solution, and any other solution through the same data is its restriction.

[F5]

Gronwall's integral inequality with variable and constant coefficients: if a continuous nonnegative $V$ satisfies $V (t) \leq C \int_{0}^{t} V (s) d s$ , then $V (t) = 0$ .

[F6]

The second fundamental theorem: if $G$ is differentiable on $[a, b]$ with $G^{'} = f$ and $f$ is integrable, then $\int_{a}^{b} f = G (b) - G (a)$ : the integral of a continuous derivative on a compact interval is the endpoint difference.

[A1]

Because $R$ is compact and $U$ is open, and $D F$ is bounded on some closed neighborhood of $R$ , choose $δ > 0$ small enough that the closed convex neighborhood $R_{δ} = R + {\overline{B}}_{δ}$ is contained both in $U$ and in that bounded neighborhood. Then $D F$ is bounded on $R_{δ}$ , so $F$ is Lipschitz there with a constant $L$ , and compactness gives $M_{F} = \sup_{R_{δ}} ∥ F ∥ < \infty$ .

Proof

1.1A1F1F3givenalgebra

Let $z (t)$ be the unique local solution from [F3] and let $p (t)$ be the coordinatewise projection of $z (t)$ onto $R$ . While $z (t) \in R_{δ}$ , define $V (t) = \sum_{i} ((a_{i} - z_{i} (t))_{+}^{2} + (z_{i} (t) - b_{i})_{+}^{2})$ , where $x_{+} = \max (x, 0)$ . The squared positive-part function is continuously differentiable. If $z_{i} < a_{i}$ , then $p_{i} = a_{i}$ and [F1], [A1] give $F_{i} (z) \geq F_{i} (p) - L ∥ z - p ∥ \geq - L ∥ z - p ∥$ ; if $z_{i} > b_{i}$ , then $p_{i} = b_{i}$ and $F_{i} (z) \leq F_{i} (p) + L ∥ z - p ∥ \leq L ∥ z - p ∥$ . Differentiating the active terms of $V$ therefore yields $V^{'} (t) \leq C_{m} L V (t)$ for a finite constant $C_{m}$ depending only on $m$ .

2.1step 1.1F5given

Since $V (0) = 0$ , integrating $V^{'} (t) \leq C_{m} L V (t)$ gives $0 \leq V (t) \leq C_{m} L \int_{0}^{t} V (s) d s$ on any initial interval where $z$ remains in $R_{δ}$ . Apply Gronwall's inequality [F5] to obtain $V (t) = 0$ . Thus $z (t)$ cannot leave $R$ on its local interval of existence.

3.1A1F3F4F6step 2.1algebra

The field is bounded by $M_{F}$ on $R$ by [A1]. If a maximal solution interval had a finite right endpoint $T_{*}$ , then $∥ z (t) - z (s) ∥ \leq M_{F} ∣ t - s ∣$ for $s, t < T_{*}$ , so $z (t)$ has a limit $z_{*} \in R$ as $t ↑ T_{*}$ . The open domain contains $z_{*}$ , so [F3] gives a solution starting at $(T_{*}, z_{*})$ ; local uniqueness in [F3] joins it to the original solution, contradicting maximality [F4]. Hence the solution exists for every $t \geq 0$ , and step 2.1 keeps it in $R$ .

4.1F2F6givenalgebra∎

Along the solution, $\frac{d}{d t} (c^{T} z (t)) = c^{T} F (z (t))$ . By [F2] this derivative is zero in the conservation case and nonpositive in the dissipation case. Integrating over $[0, t]$ proves the corresponding mass conclusion.

Depends on

Used by

Dependency tree · two levels

36 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

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