releaseRate_zero
plain-language theorem explainer
The release rate at rung zero equals the initial rate r_0. Mars terraforming models cite this base case to anchor the geometric phi progression for CO2 release. The proof is a one-line wrapper that unfolds the release rate definition and simplifies.
Claim. Let $r(n)$ denote the release rate at rung $n$ and $r_0$ the initial rate. Then $r(0) = r_0$.
background
The module derives a J-cost optimal CO2 release schedule for Mars terraforming with rate scaling as $r_0$ times phi to the power of the rung index. r_0 is the initial release rate fixed at year zero. releaseRate encodes the geometric progression $r_0 * phi^n$ on the phi-ladder.
proof idea
One-line wrapper that unfolds releaseRate and applies simp.
why it matters
Supplies the rate_zero field inside marsAtmosphereJCostScheduleCert, which collects the zero, positivity, monotonicity and cumulative properties of the schedule. It completes the base case for the geometric sum identity in the module documentation. Connects to the phi self-similar fixed point in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.