releaseRate_strict_mono
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.