  38def r_0 : ℝ := 1
  39
  40/-- Release rate at φ-rung `n`. -/
  41def releaseRate (n : ℕ) : ℝ := r_0 * phi ^ n
  42
  43theorem releaseRate_zero : releaseRate 0 = r_0 := by
  44  unfold releaseRate; simp
  45
  46theorem releaseRate_pos (n : ℕ) : 0 < releaseRate n := by
  47  unfold releaseRate r_0
  48  exact mul_pos one_pos (pow_pos phi_pos _)
  49
  50theorem releaseRate_strict_mono {n m : ℕ} (h : n < m) :
  51    releaseRate n < releaseRate m := by
  52  unfold releaseRate r_0
  53  simp only [one_mul]
  54  exact pow_lt_pow_right₀ one_lt_phi h
  55
  56theorem releaseRate_succ (n : ℕ) :
  57    releaseRate (n + 1) = releaseRate n * phi := by
  58  unfold releaseRate
  59  rw [pow_succ]; ring
  60
  61/-! ## §2. Cumulative release -/
  62
  63/-- Cumulative CO₂ released over `n` rungs (geometric partial sum). -/
  64def cumulativeRelease (n : ℕ) : ℝ :=
  65  (Finset.range n).sum (fun k => releaseRate k)
  66
  67theorem cumulativeRelease_zero : cumulativeRelease 0 = 0 := by
  68  unfold cumulativeRelease; simp
  69
  70theorem cumulativeRelease_succ (n : ℕ) :
  71    cumulativeRelease (n + 1) = cumulativeRelease n + releaseRate n := by

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.