cumulativeRelease
plain-language theorem explainer
The cumulativeRelease definition computes the total carbon dioxide released after n rungs by summing the per-rung rates in the Mars terraforming model. Researchers working on planetary engineering schedules would cite this partial sum when verifying total atmospheric loading. It is realized as a finite sum over the release rate sequence.
Claim. Let $r(k)$ denote the release rate at rung $k$. The cumulative release after $n$ rungs equals $sum_{k=0}^{n-1} r(k)$.
background
The module documents a J-cost schedule for Mars terraforming in which the release rate grows geometrically with the golden ratio phi. The upstream release rate definition sets the rate at rung n to the base rate times phi to the power n. This cumulative definition aggregates those rates to obtain the total carbon dioxide released, as required for the geometric partial sum identity stated in the module documentation.
proof idea
The definition is a direct one-line wrapper that applies the Finset range sum to the release rate function.
why it matters
It provides the total release quantity required by the certification structure MarsAtmosphereJCostScheduleCert and the one-statement theorem for the terraforming schedule. The construction follows the phi-ladder geometry in the Recognition Science engineering track, where self-similar scaling governs the release increments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.