referenceRate

formal source

  34noncomputable section
  35
  36/-- Reference core-vocabulary replacement rate (RS-native). -/
  37def referenceRate : ℝ := 1
  38
  39/-- Replacement rate at φ-ladder rung `k` (higher rung = faster). -/
  40def rateAtRung (k : ℕ) : ℝ := referenceRate * phi ^ k
  41
  42theorem rateAtRung_pos (k : ℕ) : 0 < rateAtRung k := by
  43  unfold rateAtRung referenceRate
  44  have : 0 < phi ^ k := pow_pos Constants.phi_pos k
  45  linarith [this]
  46
  47theorem rateAtRung_succ_ratio (k : ℕ) :
  48    rateAtRung (k + 1) = rateAtRung k * phi := by
  49  unfold rateAtRung; rw [pow_succ]; ring
  50
  51theorem rateAtRung_strictly_increasing (k : ℕ) :
  52    rateAtRung k < rateAtRung (k + 1) := by
  53  rw [rateAtRung_succ_ratio]
  54  have hk : 0 < rateAtRung k := rateAtRung_pos k
  55  have hphi_gt_one : (1 : ℝ) < phi := by
  56    have := Constants.phi_gt_onePointFive; linarith
  57  have : rateAtRung k * 1 < rateAtRung k * phi :=
  58    mul_lt_mul_of_pos_left hphi_gt_one hk
  59  simpa using this
  60
  61theorem rate_adjacent_ratio (k : ℕ) :
  62    rateAtRung (k + 1) / rateAtRung k = phi := by
  63  rw [rateAtRung_succ_ratio]
  64  field_simp [(rateAtRung_pos k).ne']
  65
  66structure SwadeshDecayCert where
  67  rate_pos : ∀ k, 0 < rateAtRung k