cumulativeRelease_succ
plain-language theorem explainer
The partial sum of release rates satisfies the successor identity: total CO2 after n+1 rungs equals the total after n rungs plus the rate at rung n. Mars terraforming schedule certifiers cite this when closing inductive arguments for monotonic growth of cumulative release. The proof is a one-line wrapper that unfolds the Finset sum definition and invokes the standard successor rule for sums over initial segments of the naturals.
Claim. Let $S(n) = (r_0 / (phi - 1)) (phi^n - 1)$ denote the cumulative CO2 released over the first $n$ rungs, where the per-rung rate is $r(k) = r_0 phi^k$. Then $S(n+1) = S(n) + r(n)$.
background
The module treats Mars CO2 release as a J-cost-optimal schedule on the phi-ladder with 45-year gaps per rung. releaseRate n is defined as r_0 * phi^n. cumulativeRelease n is the partial sum of releaseRate k for k ranging from 0 to n-1. These two definitions are the only upstream results required; the successor identity follows immediately from the general property of finite sums.
proof idea
Unfold cumulativeRelease to expose the Finset.range sum, then rewrite with the library lemma Finset.sum_range_succ that equates the sum over range (n+1) to the sum over range n plus the nth term.
why it matters
The identity is invoked in the base case of the induction for cumulativeRelease_strict_mono and appears inside the MarsAtmosphereJCostScheduleCert structure that certifies the full schedule. It supplies the geometric-sum step required by the module documentation for the J-cost release schedule. The result sits inside the engineering track that derives concrete release timelines from the phi-ladder and the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.