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.

Finite-volume and periodic diffusion preserve intervals and weighted mass

Statement

Consider either the no-flux TPFA cell system of No-flux TPFA diffusion generator or the periodic grid system of Periodic rectangular reaction-diffusion grid. Write its finite index set as $I$ , its positive diagonal mass matrix as $M = diag (m_{i})$ , and its stiffness matrix as $L$ . In both cases $L = L^{T}$ , $L 1 = 0$ , and $L_{i j} = - c_{i j}$ for $i \neq j$ , where $c_{i j} = c_{j i} \geq 0$ . For each species $r$ , let $d_{r} \geq 0$ and solve $M u_{r}^{'} + d_{r} L u_{r} = 0$ . Assume $a_{r} \leq b_{r}$ for every species. If initially $u_{i, r} \in [a_{r}, b_{r}]$ for all $i, r$ , then the solution exists for all $t \geq 0$ and remains in those intervals. More precisely, each species evolution matrix has nonnegative entries and row sums one, so it is a contraction in the maximum norm. The flow also preserves each weighted species sum $\sum_{i} m_{i} u_{i, r}$ and therefore every finite linear combination of species sums, including $M_{c, h}$ of Stoichiometric conservation and dissipation functionals.

Facts & Assumptions

Given: Either stated finite diffusion discretization, a finite index set $I$ , positive masses, symmetric stiffness with nonpositive off-diagonal entries and zero row sums, species diffusivities $d_{r} \geq 0$ , and initial component values in the stated intervals.

[F1]

No-flux TPFA diffusion generator: its mass matrix has entries $m_{K} = ∣ K ∣ > 0$ ; its stiffness has symmetric off-diagonal entries $- c_{K L} \leq 0$ and zero row sums.

[F2]

Periodic rectangular reaction-diffusion grid: its mass matrix is $m_{h} I$ and its stiffness $m_{h} A_{h}^{p e r}$ is symmetric, has nonpositive off-diagonal entries, and annihilates constants.

[F3]

Finite matrix exponential series and its identities: for a finite matrix $A$ , $e^{t A}$ is defined by a convergent power series, is differentiable with derivative $A e^{t A}$ , and exponentials of commuting matrices multiply to the exponential of their sum.

[F4]

The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ : $e^{x} > 0$ for every real $x$ .

[F5]

Stoichiometric conservation and dissipation functionals: $M_{c, h} (U) = \sum_{i} m_{i} c^{T} U_{i}$ .

[F6]

Picard-Lindelöf local existence and uniqueness for first-order systems: a locally Lipschitz finite-dimensional vector field has a unique local solution through each initial state.

Proof

1.1F1F2givenchooseconstructinduction

Fix a species $r$ and put $A_{r} = - d_{r} M^{- 1} L$ . If $d_{r} = 0$ , the solution is constant. If $d_{r} > 0$ , then $(A_{r})_{i j} = d_{r} c_{i j} / m_{i} \geq 0$ for $i \neq j$ , every row sums to zero, and $(A_{r})_{i i} = - d_{r} \sum_{j \neq i} c_{i j} / m_{i}$ . Choose $α > 0$ at least as large as every exit rate $d_{r} \sum_{j \neq i} c_{i j} / m_{i}$ , and set $P = I + A_{r} / α$ . Then $P$ is entrywise nonnegative with row sums one. Matrix multiplication shows inductively that every $P^{k}$ has these same properties.

1.2F1F2F3algebra

Symmetry of $L$ and $L 1 = 0$ give $1^{T} L = 0$ . Hence $1^{T} M A_{r} = - d_{r} 1^{T} L = 0$ , and multiplication by every power of $A_{r}$ gives $1^{T} M A_{r}^{k} = 0$ for $k \geq 1$ . The exponential series therefore yields $1^{T} M e^{t A_{r}} = 1^{T} M$ , so the weighted sum of species $r$ is conserved.

2.1F3F4F6step 1.1algebra

If $d_{r} = 0$ , $e^{t A_{r}} = I$ has nonnegative entries and row sums one. Otherwise use the $α$ and $P$ of step 1.1. Since $A_{r} = α (P - I)$ , [F3] gives $e^{t A_{r}} = e^{α t P} e^{- α t I}$ . The power series shows $e^{- α t I} = e^{- α t} I$ , whose scalar coefficient is positive by [F4]. Every term in the series for $e^{α t P}$ is entrywise nonnegative by step 1.1. Thus $e^{t A_{r}}$ is entrywise nonnegative. Since $A_{r} 1 = 0$ , its power series also gives $e^{t A_{r}} 1 = 1$ . By [F3], this exponential has derivative $A_{r} e^{t A_{r}}$ and initial value $I$ , so it solves the finite ODE; [F6] gives uniqueness.

3.1F3F5step 2.1step 1.2algebra∎

The initial inequalities are $u_{r} (0) - a_{r} 1 \geq 0$ and $b_{r} 1 - u_{r} (0) \geq 0$ . Applying the nonnegative matrix $e^{t A_{r}}$ and using $e^{t A_{r}} 1 = 1$ from step 2.1 proves $a_{r} 1 \leq e^{t A_{r}} u_{r} (0) \leq b_{r} 1$ . The explicit exponential is defined for every finite $t \geq 0$ ; step 1.2 preserves its weighted sum. Taking the finite linear combination in [F5] proves the stated mass assertion.

Depends on

Used by

Dependency tree · two levels

32 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

R. Eymard, T. Gallouët, and R. Herbin, Finite Volume Methods, updated author text, 2019 (standard reference, not scraped)
Willem Hundsdorfer, Numerical Solution of Advection-Diffusion-Reaction Equations, lecture notes for Ph.D. course, 1996 (standard reference, not scraped)