`r_0`

definition

show as: view math explainer →

module: IndisputableMonolith.Engineering.MarsAtmosphereJCostSchedule
domain: Engineering
line: 38 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Engineering.MarsAtmosphereJCostSchedule on GitHub at line 38.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  35/-! ## §1. Release rate ladder -/
  36
  37/-- Initial release rate (year 0). -/
  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

papers checked against this theorem

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