cumulativeRelease_zero
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not compute releaseRate at any positive rung.
- Does not derive the closed-form geometric sum for n > 0.
- Does not incorporate physical constants or units.
- Does not address continuous-time limits or non-integer rungs.
Lean usage
example : cumulativeRelease 0 = 0 := cumulativeRelease_zeroformal statement (Lean)
67theorem cumulativeRelease_zero : cumulativeRelease 0 = 0 := by
proof body
One-line wrapper that applies unfold.
68 unfold cumulativeRelease; simp
69