releaseRate
plain-language theorem explainer
The release rate at rung n is defined as the initial rate multiplied by phi to the power n. Engineers deriving the Mars CO2 release schedule under J-cost optimality would cite this geometric scaling. The definition is a direct one-line multiplication of the pre-set initial rate by the phi factor at each rung.
Claim. $r(n) = r_0 phi^n$ for $n$ a natural number, where $r_0$ is the initial release rate at rung zero.
background
This module derives a J-cost optimal schedule for Mars terraforming via CO2 release. The release follows a geometric progression on the phi-ladder, with the continuous approximation given as r(t) = r_0 phi^(t/45) and a 45-year gap per rung. The upstream definition fixes r_0 as the initial release rate (year 0) and sets it to 1 in native units.
proof idea
This is a direct definition that multiplies the initial release rate by phi raised to the rung index. No lemmas are applied beyond the definition of r_0 and the real exponentiation operation.
why it matters
This definition supplies the base rate function used to construct the cumulative release sum and to certify the monotonicity properties in MarsAtmosphereJCostScheduleCert. It realizes the geometric scaling required for the Mars terraforming plan, which is summarized in the one-statement theorem asserting rate ladder properties, positivity, and strict increase. The module falsifier is any deployed schedule diverging from this phi scaling by a factor of two at any rung.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.