releaseRate_strict_mono
The theorem shows that the CO₂ release rate r(n) = φ^n (with r_0 = 1) increases strictly with rung index n. Mars terraforming engineers would cite it to validate the exponential schedule in the J-cost model. The short proof unfolds the definition, cancels the unit multiplier, and invokes the strict monotonicity of exponentiation for base phi > 1.
claimLet $r(n) := r_0 φ^n$ with $r_0 = 1$. For natural numbers $n < m$ it holds that $r(n) < r(m)$.
background
The module derives an optimal CO₂ release schedule for Mars terraforming under the J-cost metric. The initial rate r_0 is defined as 1 in RS-native units. The release rate at rung n is then r_0 multiplied by phi raised to n, where phi is the golden ratio satisfying the self-similar fixed point from the forcing chain. Upstream, one_lt_phi establishes that phi exceeds 1, which is required for the exponential growth to be increasing. This sits inside the Engineering track of the Recognition Science framework, where J-cost schedules are built from the Recognition Composition Law and the phi-ladder.
proof idea
The proof is a one-line term-mode wrapper. It unfolds the definitions of releaseRate and r_0, simplifies the multiplication by one using the arithmetic lemma one_mul, and applies the power strict increase lemma pow_lt_pow_right₀ instantiated with one_lt_phi and the hypothesis n < m.
why it matters in Recognition Science
This result is used to certify the full Mars atmosphere J-cost schedule and to assemble the one-statement summary of the terraforming ladder. It directly supports the claim in the module documentation that release rates are strictly increasing, closing the monotonicity part of the geometric schedule. In the broader framework it instantiates the phi > 1 property (T5-T6) for an engineering application, confirming that the eight-tick octave structure yields monotonic growth in the D=3 spatial setting.
scope and limits
- Does not specify the physical units or gap size of 45 years.
- Does not prove positivity or the cumulative sum identities.
- Does not address whether the schedule satisfies planetary boundary conditions.
- Does not derive the value of r_0 from first principles.
Lean usage
theorem example_use {n m : ℕ} (h : n < m) : releaseRate n < releaseRate m := releaseRate_strict_mono hformal statement (Lean)
50theorem releaseRate_strict_mono {n m : ℕ} (h : n < m) :
51 releaseRate n < releaseRate m := by
proof body
Term-mode proof.
52 unfold releaseRate r_0
53 simp only [one_mul]
54 exact pow_lt_pow_right₀ one_lt_phi h
55