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.

Certified residuals bound mass drift and the exact-solve positivity margin

Statement

Let $M \in R^{m \times m}$ be the exact real matrix represented by the stored coefficients of a successfully completed Modified Patankar Euler for conservative transfer systems step with admissible positive denominators, or of a completed stage/final solve of The positive-interior MPRK22(1) step, for a finite conservative PDS. Let $b \geq 0$ be its stored right-hand side, interpreted exactly as a real vector. For either scheme, the PDS transfer identity gives $1^{T} M = 1^{T}$ and strict column diagonal dominance, so $M^{- 1} \geq 0$ . Let $\hat{y} \in R^{m}$ be a stored candidate. Assume all entries of $M$ , $\hat{y}$ , and $b$ are stored in a common operationwise format $F$ with unit roundoff $u$ , and compute $\hat{v} = fl (M \hat{y})$ and $\hat{w} = fl (\hat{v} - b)$ in the model of Operationwise real and complex floating point arithmetic with rounded square roots and fused multiply-add, with $0 < u < 1$ , $(m - 1) u < 1$ , every nonzero exact intermediate normal, zero operations exact, and successful sequential dot products and subtraction. Let $W$ be the certified allowance from Rounded matrix products give certified linear and normal-equation residual allowances, with its norm inputs exact or certified upper bounds. Let $η_{w}$ be the exact value of $∥ \hat{w} ∥_{2}$ or a certified upper bound for it, and set $ρ : = η_{w} + W$ .

$∥ M \hat{y} - b ∥_{2} \leq ρ, ∣ 1^{T} \hat{y} - 1^{T} b ∣ \leq \sqrt{m} ρ .$

If $y^{*} : = M^{- 1} b$ is the exact solution of the stored linear system, then

$∥ \hat{y} - y^{*} ∥_{1} \leq \sqrt{m} ρ .$

Consequently, the componentwise margin condition ${\hat{y}}_{i} \geq \sqrt{m} ρ$ for every $i$ certifies $y^{*} \geq 0$ . A residual bound alone does not certify that the computed candidate $\hat{y}$ is nonnegative. This certificate is relative to the stated stored matrix and right-hand side; any coefficient-assembly or right-hand-side data error relative to the intended real system must be separately bounded and added to the residual allowance.

Facts & Assumptions

Given: A finite conservative PDS matrix $M$ from the stated Patankar systems, its stored real right-hand side $b \geq 0$ , a stored candidate $\hat{y}$ , and their common operationwise format with $0 < u < 1$ and $(m - 1) u < 1$ . Assume normal nonzero exact intermediates, exact zero operations, successful residual calculations, exact or certified upper bounds for the norm inputs used in $W$ , and an exact or certified upper bound $η_{w} \geq ∥ \hat{w} ∥_{2}$ .

[F1]

Finite conservative production destruction systems: paired transfers satisfy $p_{i j} = d_{j i}$ .

[F2]

Modified Patankar Euler for conservative transfer systems and The positive-interior MPRK22(1) step: every completed solve evaluates PDS rates only at states in $Ω_{+}$ ; with positive declared denominators, its matrix has nonpositive off-diagonal entries, positive diagonal, and column sums equal to one by $p_{i j} = d_{j i}$ .

[F3]

Strict column dominance gives an entrywise nonnegative inverse: each such solve matrix has an entrywise nonnegative inverse.

[F4]

Operationwise real and complex floating point arithmetic with rounded square roots and fused multiply-add: successful real additions, subtractions and products follow the stated no-underflow, round-to-nearest operation model.

[F5]

Rounded matrix products give certified linear and normal-equation residual allowances: for stored $M, \hat{y}, b$ and the stated successful evaluation order, $∥ \hat{w} - (M \hat{y} - b) ∥_{2} \leq W$ when its unit-roundoff and normal-intermediate hypotheses hold; the norms used in $W$ are exact or certified upper bounds.

[F6]

Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation: $∣ ⟨ u, v ⟩ ∣ \leq ∥ u ∥_{2} ∥ v ∥_{2}$ , in particular $∥ r ∥_{1} \leq \sqrt{m} ∥ r ∥_{2}$ and $∣ 1^{T} r ∣ \leq \sqrt{m} ∥ r ∥_{2}$ .

Proof

1.1F1F2F3algebra

For modified Patankar Euler, column $j$ of $M$ has off-diagonal entries $- h p_{i j} (y^{n}) / σ_{j}$ and diagonal $1 + h \sum_{k \neq j} d_{j k} (y^{n}) / σ_{j}$ ; for an MPRK final matrix the same form uses averaged rates and denominators $z_{j}$ , and its stage is the first form with $σ_{j} = y_{j}^{n} > 0$ . By [F1]–[F2], each such matrix has column sum one and strict column-dominance margin one, so [F3] gives $M^{- 1} \geq 0$ .

1.2F4F5algebra

Put $r : = M \hat{y} - b$ . By [F5] and the triangle inequality, $∥ r ∥_{2} \leq ∥ \hat{w} ∥_{2} + ∥ r - \hat{w} ∥_{2} \leq ∥ \hat{w} ∥_{2} + W \leq η_{w} + W = ρ$ .

1.3F2F3algebra

Multiplying $1^{T} M = 1^{T}$ on the right by $M^{- 1}$ gives $1^{T} M^{- 1} = 1^{T}$ .

2.1F2F6step 1.2algebra

Since $1^{T} M = 1^{T}$ , $1^{T} \hat{y} - 1^{T} b = 1^{T} (M \hat{y} - b) = 1^{T} r$ ; [F6] and step 1.2 give $∣ 1^{T} \hat{y} - 1^{T} b ∣ \leq \sqrt{m} ρ$ .

2.2F3F6step 1.2step 1.3algebra

With $y^{*} = M^{- 1} b$ , we have $\hat{y} - y^{*} = M^{- 1} r$ and, since $M^{- 1} \geq 0$ and its columns sum to one, $∥ M^{- 1} r ∥_{1} = \sum_{i} ∣ \sum_{j} (M^{- 1})_{i j} r_{j} ∣ \leq \sum_{j} (\sum_{i} (M^{- 1})_{i j}) ∣ r_{j} ∣ = ∥ r ∥_{1} \leq \sqrt{m} ρ$ by [F6] and step 1.2.

3.1step 2.2algebra∎

For each coordinate, $y_{i}^{*} \geq {\hat{y}}_{i} - ∣ {\hat{y}}_{i} - y_{i}^{*} ∣ \geq {\hat{y}}_{i} - ∥ \hat{y} - y^{*} ∥_{1}$ ; step 2.2 therefore gives $y_{i}^{*} \geq 0$ whenever ${\hat{y}}_{i} \geq \sqrt{m} ρ$ . A residual bound alone places no sign condition on $\hat{y}$ , so it does not certify that the computed candidate is nonnegative.

Depends on

Used by

An arbitrarily small residual does not certify the candidate's nonnegativity Counterexample

Dependency tree · two levels

22 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, Lemmas 2.6–2.7 (standard reference, not scraped)