TheoremStatement: AI-adaptedProof: AI-generatedPipeline-generated

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 sectional dynamics have a unique global positive solution

Statement

For every nonnegative finite-grid initial state $(n^{0}, L^{0})$ , with grid indices $0 \leq i \leq J$ , mesh width $Δ = \max_{i < J} (x_{i + 1} - x_{i}) \leq 1$ , maximum aggregation rate $K_{*} : = \max_{i, j} K_{i j}$ , fragmentation rate bound $β_{*} : = \max_{i} β_{i}$ , and daughter count bound $D : = \max_{i} B_{x_{i}} (E)$ , the ODE of Finite sectional coagulation-fragmentation balance with reported overflow has a unique solution for all $t \geq 0$ , and the solution remains nonnegative. Here $x_{i} \geq a > 0$ and each daughter measure has first moment $x_{i}$ . If its initial augmented mass is $M = \sum_{i = 0}^{J} x_{i} n_{i}^{0} + L^{0}$ , then

$0 \leq n_{i} (t) \leq M / x_{i}, 0 \leq L (t) \leq M, M_{2} (t) \leq M_{2, 0} + t [K_{*} M^{2} + Δ^{2} (\frac{K_{*} M^{2}}{8 a^{2}} + \frac{β_{*} D M}{4 a})],$

where $M_{2} (t) = \sum_{i} x_{i}^{2} n_{i} (t)$ and $M_{2, 0} = M_{2} (0)$ .

Facts & Assumptions

Given: A finite-dimensional autonomous event ODE, a nonnegative initial state, and the mass and positivity conclusions of the cited items.

[F1]

The finite sectional reaction vector field is locally Lipschitz: the finite-dimensional right-hand side is locally Lipschitz.

[F2]

Finite sectional event dynamics preserve positivity and retained-plus-reservoir mass: solutions remain nonnegative and $\sum_{i} x_{i} n_{i} (t) + L (t) = M$ on their intervals of existence.

[F3]

Every Picard–Lindelöf initial value problem has one maximal solution on an open interval: every locally Lipschitz finite-dimensional initial-value problem has a unique maximal solution.

[F4]

Picard-Lindelöf local existence and uniqueness for first-order systems: every locally Lipschitz finite-dimensional initial-value problem has a unique solution on a neighborhood of its initial time.

[F5]

Fixed-pivot weights are nonnegative and reproduce number and mass: redistributing a product or daughter of size $z$ adds at most $Δ^{2} / 4$ to its second moment.

Proof

1.1givenF1F2F3

By [F1] and [F3], the event ODE has a unique maximal solution on an open time interval containing $0$ . While it exists, [F2] puts every coordinate in the closed set $0 \leq n_{i} \leq M / x_{i}$ and $0 \leq L \leq M$ , which is compact because the grid is finite and $x_{i} > 0$ .

1.2givenF1F2F5algebra

Along each in-range coagulation event at parent masses $x_{i}, x_{j}$ , the second-moment increment is at most $2 x_{i} x_{j} + Δ^{2} / 4$ by [F5]; an overflow event only removes retained second moment. Summing the event rates $K_{i j} n_{i} n_{j} / 2$ bounds the coagulation contribution by $K_{*} M_{1}^{2} + K_{*} Δ^{2} M_{0}^{2} / 8$ . For fragmentation, $\int z^{2} B_{x_{i}} (d z) \leq x_{i}^{2}$ because $z \leq x_{i}$ and $\int z B_{x_{i}} = x_{i}$ ; pivot redistribution adds at most $D Δ^{2} / 4$ per parent event. Thus its second-moment contribution is at most $β_{*} D Δ^{2} M_{0} / 4$ .

2.1step 1.1step 1.2algebra

Since $x_{i} \geq a$ , the mass bound in step 1.1 gives $M_{0} \leq M / a$ and $M_{1} \leq M$ . Integrating the derivative bound in step 1.2 yields the displayed $M_{2}$ estimate.

3.1step 1.1F3F4algebra∎

If the maximal right endpoint $T_{*}$ were finite, step 1.1 puts the solution in a compact set. Continuity of $F$ there gives a bound $B$ on $∥ F ∥_{2}$ , so $∥ y (t) - y (s) ∥_{2} \leq B ∣ t - s ∣$ and $y (t)$ has a limit in that set as $t ↑ T_{*}$ . By [F4], restarting at the limit gives a local solution; uniqueness in [F3] glues it to the existing solution and extends past $T_{*}$ , a contradiction. The same argument applies at every finite endpoint.

Depends on

Used by

Dependency tree · two levels

18 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

Philippe Laurençot and Stéphane Mischler, From the discrete to the continuous coagulation-fragmentation equations, §1 (standard reference, not scraped)
Jitendra Kumar, Numerical approximations of population balance equations in particulate systems, Chapter 2 (standard reference, not scraped)