pith. machine review for the scientific record. sign in
theorem proved tactic proof

N_galactic_approx

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  30theorem N_galactic_approx : 140 < N_galactic ∧ N_galactic < 145 := by

proof body

Tactic-mode proof.

  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** -/

depends on (11)

Lean names referenced from this declaration's body.