cumulativeRelease_zero
plain-language theorem explainer
cumulativeRelease_zero establishes that the total CO2 released after zero rungs equals zero, anchoring the base case of the geometric partial sum for the Mars terraforming J-cost schedule. Engineers modeling phi-scaled release timelines cite this to initialize the sum identity before applying the closed form for positive rungs. The proof is a one-line wrapper that unfolds the sum definition and simplifies the empty range.
Claim. Let $S(n) := (Finset.range n).sum (fun k => r(k))$ where $r(k)$ is the release rate at rung $k$. Then $S(0) = 0$.
background
The module derives a J-cost-optimal CO2 release schedule for Mars terraforming. Release rates follow a geometric progression $r(k) = r_0 · φ^k$ (gap-45 yr per rung) to minimize the Recognition Science J-cost. cumulativeRelease n is defined as the partial sum of the first n rates, giving total CO2 released over n rungs. The upstream definition states: Cumulative CO2 released over n rungs (geometric partial sum). This zero case supplies the base for the geometric-sum identity used in the engineering derivation.
proof idea
The proof is a one-line wrapper. It unfolds the definition of cumulativeRelease (the sum over Finset.range 0) and applies simp to reduce the empty sum to zero.
why it matters
This base case populates the cumulative_zero field inside marsAtmosphereJCostScheduleCert, which certifies the full schedule invariants including rate positivity, strict monotonicity, and the geometric sum. It closes the n=0 instance of the total-release formula r_0 · 45 · (φ^n - 1)/(φ - 1) described in the module documentation. The result sits inside the phi-ladder and J-cost framework of Recognition Science; the module falsifier is any schedule diverging from the φ scaling by a factor of 2.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.