TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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 factorized zero-state step is well-defined, nonnegative, conservative, and locally first order

Statement

Let a finite conservative PDS have a source-factored representation on an open neighborhood $U \subseteq Ω$ of a compact set $K \subseteq [0, \infty)^{m}$ , with factors that are multivariable $C^{2}$ on $U$ and nonnegative on $U \cap [0, \infty)^{m}$ , as in Source-factored transfer rates for zero compartments. For every $y^{n} \in K$ and $h > 0$ , Zero-compatible modified Patankar Euler in rate-factor form has a unique output $y^{n + 1} \geq 0$ and conserves $\sum_{i} y_{i}$ . For the accuracy clause, fix a compact set $K_{*} \subset U$ containing $K$ and all exact solution segments under consideration, and define the $C^{2}$ extension ${\tilde{F}}_{i} (y) : = \sum_{j \neq i} (y_{j} a_{i j} (y) - y_{i} a_{j i} (y))$ on $U$ . If those exact segments remain in $K_{*} \cap [0, \infty)^{m}$ , then the exact-start local defect is uniformly $O (h^{2})$ as $h ↓ 0$ , including when some coordinates of $y^{n}$ are zero. The claim is local; no global error bound at the boundary is asserted.

Facts & Assumptions

Given: A finite conservative PDS, a source-factored representation on a neighborhood of $K$ , $y^{n} \in K \subseteq [0, \infty)^{m}$ , $h > 0$ , and the fixed compact tube $K_{*} \subset U$ from the defect clause when local accuracy is asserted.

[F1]

Finite conservative production destruction systems: $F_{i} (y) = \sum_{j \neq i} (p_{i j} (y) - d_{i j} (y))$ and the pair rates satisfy $p_{i j} = d_{j i}$ .

[F2]

Source-factored transfer rates for zero compartments: $p_{i j} (y) = y_{j} a_{i j} (y)$ and $d_{i j} (y) = y_{i} a_{j i} (y)$ with $C^{2}$ factors that are nonnegative on admissible nonnegative states, including at zero coordinates.

[F3]

Zero-compatible modified Patankar Euler in rate-factor form: the output solves $(I - h B (y^{n})) y^{n + 1} = y^{n}$ , where $B_{i j} = a_{i j}$ for $i \neq j$ and $B_{j j} = - \sum_{i \neq j} a_{i j}$ .

[F4]

Strict column dominance gives an entrywise nonnegative inverse: a strict column-diagonally-dominant matrix with positive diagonal and nonpositive off-diagonal entries has an entrywise nonnegative inverse.

[F5]

First-order systems, initial value problems, and solutions on intervals: an exact trajectory satisfies $y^{'} = F (y)$ on its interval.

[F6]

$C^{k}$ maps and multi-index derivative notation in Euclidean space and If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative: continuous first partials give a total derivative, and the $C^{2}$ factors give continuous first derivatives.

[F7]

Chain sum product and composition rules for Banach derivatives and The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : products of differentiable coordinate maps obey the bounded-bilinear product rule, and composition obeys the total chain rule.

[F8]

Multivariable Taylor formula with a Lagrange remainder along a line segment: a $C^{2}$ solution curve on a time interval has a first-order Taylor expansion with remainder bounded by its second derivative on that interval.

[F9]

One-step ODE methods, local defect, uniform order, and step stability: the exact-start local defect is the method output minus the exact next state.

Proof

1.1givenF2F3F4algebra

For each column $j$ , $B_{j j} = - \sum_{i \neq j} a_{i j} \leq 0$ , $B_{i j} = a_{i j} \geq 0$ off the diagonal, and $\sum_{i} B_{i j} = 0$ . Therefore $M : = I - h B (y^{n})$ has $M_{j j} = 1 + h \sum_{i \neq j} a_{i j} (y^{n}) > 0$ , $M_{i j} = - h a_{i j} (y^{n}) \leq 0$ for $i \neq j$ , and $M_{j j} - \sum_{i \neq j} ∣ M_{i j} ∣ = 1$ . By [F4], $M^{- 1} \geq 0$ ; hence the unique solution $y^{n + 1} = M^{- 1} y^{n}$ exists and is nonnegative, including for zero coordinates in $y^{n}$ .

2.1F3step 1.1algebra

The column sums of $M$ equal one, so $\sum_{i} y_{i}^{n} = \sum_{i} (M y^{n + 1})_{i} = \sum_{j} (\sum_{i} M_{i j}) y_{j}^{n + 1} = \sum_{j} y_{j}^{n + 1}$ .

2.2F1F2F3algebra

The factorization [F2] gives $B (y) y = F (y)$ for every $y \in K$ : its $i$ -th component is $\sum_{j \neq i} a_{i j} (y) y_{j} - y_{i} \sum_{j \neq i} a_{j i} (y) = \sum_{j \neq i} (p_{i j} (y) - d_{i j} (y))$ . The matrix identity used in step 1.1 also gives $(I - h B (y))^{- 1} = I + h B (y) + h^{2} B (y)^{2} (I - h B (y))^{- 1}$ .

3.1givenF2F5F6F7F8F9step 2.2algebra∎

The factors are $C^{2}$ on $U$ , so the coordinate products $y_{j} a_{i j} (y)$ and $y_{i} a_{j i} (y)$ have continuous partial derivatives through order two by applying the bounded-bilinear product rule [F7] twice. Applying the continuous-partials theorem [F6] to these components and their first partials shows that $\tilde{F}$ is $C^{2}$ and has continuous first total derivative on $U$ . On the compact set $[0, h_{0}] \times K$ of admissible nonnegative starting states, $B$ is bounded and $I - h B (y^{n})$ is invertible by step 1.1 for $h > 0$ and equals $I$ at $h = 0$ . Its inverse is continuous there, hence uniformly bounded for sufficiently small $h$ . The matrix identity from step 2.2 then yields $y^{n + 1} = y^{n} + h F (y^{n}) + O (h^{2})$ uniformly, without dividing by any coordinate of $y^{n}$ . On the nonnegative exact path, the PDS field equals the $C^{2}$ extension $\tilde{F}$ defined in the Statement, so [F5]–[F7] give $y^{'} = \tilde{F} (y)$ and bounded $y^{''} = D \tilde{F} (y) \tilde{F} (y)$ on $K_{*}$ . Applying [F8] to the time curve gives the same expansion uniformly. Their difference is therefore $O (h^{2})$ uniformly, which is the local-defect bound specified by [F9].

Depends on

Used by

Dependency tree · two levels

41 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

Stefan Kopecz and Andreas Meister, On order conditions for modified Patankar-Runge-Kutta schemes, §2 (standard reference, not scraped)
Sergio Blanes, Arieh Iserles, and Shev Macnamara, Positivity-preserving methods for ordinary differential equations, §3.4 (standard reference, not scraped)