releaseRate_pos
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not establish the 45-year time interval per rung.
- Does not prove the rate is strictly increasing.
- Does not derive the closed-form cumulative sum.
- Does not connect to specific physical CO2 mass values.
Lean usage
exact le_of_lt (releaseRate_pos k)formal statement (Lean)
46theorem releaseRate_pos (n : ℕ) : 0 < releaseRate n := by
proof body
Term-mode proof.
47 unfold releaseRate r_0
48 exact mul_pos one_pos (pow_pos phi_pos _)
49