`referenceSpeed`

definition

show as: view math explainer →

module: IndisputableMonolith.Combustion.FlameSpeedFromPhiLadder
domain: Combustion
line: 31 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Combustion.FlameSpeedFromPhiLadder on GitHub at line 31.

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

  28noncomputable section
  29
  30/-- Reference flame speed (RS-native dimensionless 1). -/
  31def referenceSpeed : ℝ := 1
  32
  33/-- Flame speed at φ-ladder rung `k`. -/
  34def flameSpeed (k : ℕ) : ℝ := referenceSpeed * phi ^ k
  35
  36/-- Flame speed is positive at every rung. -/
  37theorem flameSpeed_pos (k : ℕ) : 0 < flameSpeed k := by
  38  unfold flameSpeed referenceSpeed
  39  have : 0 < phi ^ k := pow_pos Constants.phi_pos k
  40  linarith [this]
  41
  42/-- Adjacent-rung flame speeds ratio by exactly φ. -/
  43theorem flameSpeed_succ_ratio (k : ℕ) :
  44    flameSpeed (k + 1) = flameSpeed k * phi := by
  45  unfold flameSpeed
  46  rw [pow_succ]
  47  ring
  48
  49/-- Flame speed is strictly monotone-increasing in rung. -/
  50theorem flameSpeed_strictly_increasing (k : ℕ) :
  51    flameSpeed k < flameSpeed (k + 1) := by
  52  rw [flameSpeed_succ_ratio]
  53  have hk : 0 < flameSpeed k := flameSpeed_pos k
  54  have hphi_gt_one : (1 : ℝ) < phi := by
  55    have := Constants.phi_gt_onePointFive; linarith
  56  have : flameSpeed k * 1 < flameSpeed k * phi := by
  57    apply mul_lt_mul_of_pos_left hphi_gt_one hk
  58  simpa using this
  59
  60/-- Adjacent-rung flame-speed ratio equals φ. -/
  61theorem flameSpeed_adjacent_ratio (k : ℕ) :

papers checked against this theorem

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