halfLife

formal source

  24namespace IndisputableMonolith.Linguistics.LexicalDecayFromPhiLadder
  25open Constants
  26
  27noncomputable def halfLife (k : ℕ) : ℝ := phi ^ k
  28
  29theorem halfLifeRatio (k : ℕ) :
  30    halfLife (k + 1) / halfLife k = phi := by
  31  unfold halfLife
  32  have hpos := pow_pos phi_pos k
  33  rw [pow_succ, div_eq_iff hpos.ne']
  34  ring
  35
  36/-- phi^5 > 10. -/
  37theorem phi5_gt_10 : phi ^ 5 > 10 := by
  38  have h2 := phi_sq_eq  -- phi^2 = phi + 1
  39  have h3 : phi ^ 3 = 2 * phi + 1 := by nlinarith
  40  have h4 : phi ^ 4 = 3 * phi + 2 := by nlinarith
  41  have h5 : phi ^ 5 = 5 * phi + 3 := by nlinarith
  42  linarith [phi_gt_onePointFive]
  43
  44/-- phi^5 < 12. -/
  45theorem phi5_lt_12 : phi ^ 5 < 12 := by
  46  have h2 := phi_sq_eq
  47  have h3 : phi ^ 3 = 2 * phi + 1 := by nlinarith
  48  have h4 : phi ^ 4 = 3 * phi + 2 := by nlinarith
  49  have h5 : phi ^ 5 = 5 * phi + 3 := by nlinarith
  50  linarith [phi_lt_onePointSixTwo]
  51
  52structure LexicalDecayCert where
  53  phi_ratio : ∀ k, halfLife (k + 1) / halfLife k = phi
  54  phi5_lower : phi ^ 5 > 10
  55  phi5_upper : phi ^ 5 < 12
  56
  57noncomputable def lexicalDecayCert : LexicalDecayCert where