IndisputableMonolith.Constants.ILG

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4namespace IndisputableMonolith
   5namespace Constants
   6
   7@[simp] noncomputable def alpha_locked : ℝ := (1 - 1 / phi) / 2
   8
   9@[simp] noncomputable def Clag : ℝ := 1 / (phi ^ (5 : Nat))
  10
  11lemma alpha_locked_pos : 0 < alpha_locked := by
  12  dsimp [alpha_locked]
  13  have hφ : 0 < phi := phi_pos
  14  have hφ_gt_1 : 1 < phi := one_lt_phi
  15  -- 1/φ < 1 because φ > 1
  16  have hinv_lt_one : 1 / phi < 1 := by
  17    rw [div_lt_one hφ]
  18    exact hφ_gt_1
  19  have hsub : 0 < 1 - 1 / phi := by
  20    linarith
  21  have hdiv : 0 < (1 - 1 / phi) / 2 := by
  22    apply div_pos hsub
  23    exact zero_lt_two
  24  exact hdiv
  25
  26lemma alpha_locked_lt_one : alpha_locked < 1 := by
  27  dsimp [alpha_locked]
  28  have hφ_pos : 0 < phi := phi_pos
  29  have hφ : 1 < phi := one_lt_phi
  30  -- We need to show: (1 - 1/φ) / 2 < 1
  31  -- Since φ > 1, we have 0 < 1/φ < 1, so 0 < 1 - 1/φ < 1, so (1 - 1/φ)/2 < 1/2 < 1
  32  have hinv_pos : 0 < 1 / phi := div_pos one_pos hφ_pos
  33  have hinv_lt_one : 1 / phi < 1 := by
  34    rw [div_lt_one hφ_pos]
  35    exact hφ
  36  have hsub_lt : 1 - 1 / phi < 1 := by
  37    have : 0 < 1 / phi := hinv_pos
  38    linarith
  39  have hdiv_lt : (1 - 1 / phi) / 2 < 1 / 2 := by
  40    apply div_lt_div_of_pos_right hsub_lt
  41    exact zero_lt_two
  42  have half_lt_one : (1 : ℝ) / 2 < 1 := by norm_num
  43  linarith
  44
  45lemma Clag_pos : 0 < Clag := by
  46  have hφ : 0 < phi := phi_pos
  47  have hpow : 0 < phi ^ (5 : Nat) := pow_pos hφ 5
  48  simpa [Clag, one_div] using inv_pos.mpr hpow
  49
  50end Constants
  51end IndisputableMonolith
  52