cumulativeRelease_nonneg
plain-language theorem explainer
cumulativeRelease_nonneg establishes that the partial sum of release rates over any number of rungs stays nonnegative in the Mars J-cost schedule. Terraforming modelers cite it when confirming that total CO2 addition cannot turn negative under the geometric progression. The term proof unfolds the sum definition and applies the finite-sum nonnegativity lemma to each strictly positive term supplied by releaseRate_pos.
Claim. For every natural number $n$, $0$ $leq$ $sum_{k=0}^{n-1} r(k)$, where $r(k)$ is the release rate at rung $k$.
background
The module treats Mars terraforming as a J-cost-optimal schedule in which release rate grows as $r(t) = r_0 phi^{t/45}$. cumulativeRelease is defined as the finite sum of these rates over the first $n$ rungs. releaseRate_pos supplies the key fact that each summand is strictly positive, obtained by unfolding to $r_0$ times a positive power of phi.
proof idea
The proof unfolds cumulativeRelease to a Finset.range sum, applies Finset.sum_nonneg, then for each index $k$ replaces the summand by le_of_lt applied to releaseRate_pos k.
why it matters
The result is invoked inside marsAtmosphereJCostScheduleCert to complete the certificate for the full schedule. It supplies the nonnegativity clause required by the engineering derivation that rests on the phi-ladder and eight-tick structure of Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.