cumulativeRelease
Cumulative CO2 release after n rungs equals the partial sum of the geometric sequence r(k) = r_0 phi^k. Mars terraforming engineers would cite this sum to obtain total atmospheric mass added under the J-cost schedule. The definition is a direct Finset summation over the releaseRate sequence.
claimLet $r(k) = r_0 phi^k$ be the release rate at rung $k$. The cumulative release after $n$ rungs is $C(n) := sum_{k=0}^{n-1} r(k)$.
background
The Mars Terraforming J-Cost Schedule module implements a geometric release schedule r(t) = r_0 phi^(t/45) that follows the phi-ladder from the Recognition forcing chain. The upstream releaseRate definition supplies the per-rung term r(n) = r_0 phi^n. The cumulative sum then aggregates these terms to give total CO2 mass, matching the geometric partial sum identity stated in the module documentation.
proof idea
One-line definition that applies Finset.range sum to the releaseRate function.
why it matters in Recognition Science
This definition supplies the total mass term required by MarsAtmosphereJCostScheduleCert and mars_terraform_one_statement. It closes the geometric-sum step in the engineering derivation of the J-cost schedule, linking the phi-ladder release rates to the overall terraforming certification.
scope and limits
- Does not embed the 45-year gap scaling factor into the sum.
- Does not prove non-negativity or monotonicity of the cumulative release.
- Does not reference the J-cost functional equation or forcing chain steps T0-T8.
- Does not evaluate the sum in physical units or connect to alpha or G constants.
formal statement (Lean)
64def cumulativeRelease (n : ℕ) : ℝ :=
proof body
Definition body.
65 (Finset.range n).sum (fun k => releaseRate k)
66