cumulativeRelease_strict_mono
plain-language theorem explainer
Cumulative CO2 release over n rungs in the Mars terraforming J-cost schedule is strictly monotonic. Engineers modeling planetary engineering schedules cite this to ensure that extending the release ladder always increases total delivered CO2. The proof uses induction on the difference m-n, invoking the successor identity for the cumulative sum together with positivity of each release rate term.
Claim. Let $r(k)$ denote the release rate at rung $k$. For natural numbers $n < m$, the partial sum satisfies $S(m) > S(n)$ where $S(n) = (Finset.range n).sum (fun k => r(k))$.
background
cumulativeRelease(n) is defined as the sum of releaseRate(k) for k from 0 to n-1, where releaseRate itself follows the geometric ladder r_0 · phi^k. The module derives an optimal CO2 release schedule r(t) = r_0 · φ^(t/45) for Mars terraforming under J-cost optimality. Upstream, cumulativeRelease_succ states that the sum up to n+1 equals the sum up to n plus the nth rate, while releaseRate_pos asserts that every rate is positive; both rest on the arithmetic successor and positivity of phi.
proof idea
The proof applies Nat.le_induction on m with hypothesis h : n < m. In the base case it rewrites using cumulativeRelease_succ and applies releaseRate_pos with linarith to obtain the strict inequality. The successor step repeats the same rewrite and positivity argument.
why it matters
This monotonicity result is invoked directly in the one-statement summary of the Mars terraform schedule and in the master certificate that bundles all schedule properties. It closes the engineering derivation that total CO2 release grows without bound as the number of phi-rungs increases, consistent with the self-similar fixed point phi in the Recognition Science forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.