N_galactic

formal source

  24def phi_rung_time (N : ℝ) : ℝ := tau0_SI * phi ^ N
  25
  26/-- The log-base-φ of the timescale ratio: N = log_φ(τ★/τ₀) -/
  27def N_galactic : ℝ := Real.log (tau_star_s / tau0_SI) / Real.log phi
  28
  29/-- **THEOREM: N_galactic Approximation** -/
  30theorem N_galactic_approx : 140 < N_galactic ∧ N_galactic < 145 := by
  31  have h_ratio_val : tau_star_s / tau0_SI = (galactic_ratio_rational : ℝ) := by
  32    unfold tau_star_s tau0_SI galactic_ratio_rational
  33    norm_num
  34  have hlog_phi : 0 < Real.log phi := Real.log_pos Constants.one_lt_phi
  35
  36  constructor
  37  · unfold N_galactic
  38    rw [h_ratio_val]
  39    apply (lt_div_iff₀ hlog_phi).mpr
  40    rw [← Real.log_rpow Constants.phi_pos]
  41    apply Real.log_lt_log (Real.rpow_pos_of_pos Constants.phi_pos 140)
  42    exact phi_pow_140_lt_ratio
  43  · unfold N_galactic
  44    rw [h_ratio_val]
  45    apply (div_lt_iff₀ hlog_phi).mpr
  46    rw [← Real.log_rpow Constants.phi_pos]
  47    apply Real.log_lt_log
  48    · have h_pos : (0 : ℝ) < (galactic_ratio_rational : ℝ) := by norm_num [galactic_ratio_rational]
  49      exact h_pos
  50    · exact ratio_lt_phi_pow_145
  51
  52/-- **THEOREM: τ★ Lies on the φ-Ladder** -/
  53theorem tau_star_is_phi_rung :
  54   ∃ N : ℤ, |tau_star_s - phi_rung_time N| < 0.1 * tau_star_s := by
  55  use 142
  56  unfold phi_rung_time
  57  let ratio := tau_star_s / tau0_SI