releaseRate_pos
plain-language theorem explainer
Release rate positivity at each φ-rung n guarantees non-negative cumulative CO2 totals in the Mars schedule. J-cost modelers reference it when verifying the geometric series for total release. The term proof applies mul_pos and pow_pos after unfolding the product definition.
Claim. For every natural number $n$, $0 < r_0 · ϕ^n$ where $r_0 = 1$ is the initial release rate and $ϕ$ is the golden ratio.
background
The Mars Atmosphere J-Cost Schedule module defines the CO2 release schedule as a geometric sequence on the phi-ladder for J-cost optimality. The constant r_0 is defined as the initial release rate (year 0) with value 1. The function releaseRate n is defined as r_0 multiplied by phi raised to n, matching the module statement that release rate follows r(t) = r_0 · φ^(t/45) with rung indexing n.
proof idea
The proof is a term-mode one-liner. It unfolds releaseRate and r_0 to expose the product 1 · phi^n, then applies mul_pos one_pos (pow_pos phi_pos _) to conclude strict positivity.
why it matters
This result supplies the positivity fact used by cumulativeRelease_nonneg to prove the total release sum is non-negative and by the certification record marsAtmosphereJCostScheduleCert that bundles all schedule properties. It anchors the geometric-sum identity for total CO2 in the engineering derivation, consistent with the phi fixed point from the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.