`rs_params_positive`

proved

show as: view math explainer →

module: IndisputableMonolith.Relativity.GRLimit.Parameters
domain: Relativity
line: 32 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Relativity.GRLimit.Parameters on GitHub at line 32.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  29  Constants.phi ^ (-5 : ℝ)
  30
  31/-- PROVEN: Both parameters are positive. -/
  32theorem rs_params_positive :
  33  0 < alpha_from_phi ∧ 0 < cLag_from_phi := by
  34  constructor
  35  · unfold alpha_from_phi
  36    have hφ_pos : 0 < Constants.phi := Constants.phi_pos
  37    have hφ_gt_one : 1 < Constants.phi := Constants.one_lt_phi
  38    have : 0 < 1 - 1 / Constants.phi := by
  39      have : 1 / Constants.phi < 1 := (div_lt_one hφ_pos).mpr hφ_gt_one
  40      linarith
  41    linarith
  42  · unfold cLag_from_phi
  43    exact Real.rpow_pos_of_pos Constants.phi_pos _
  44
  45/-- PROVEN: α < 1 (straightforward from φ > 1). -/
  46theorem alpha_lt_one : alpha_from_phi < 1 := by
  47  unfold alpha_from_phi
  48  have hφ_pos : 0 < Constants.phi := Constants.phi_pos
  49  have : 1 - 1 / Constants.phi < 1 := by
  50    have : 0 < 1 / Constants.phi := div_pos (by norm_num) hφ_pos
  51    linarith
  52  have : (1 - 1 / Constants.phi) / 2 < 1 / 2 := by
  53    exact div_lt_div_of_pos_right this (by norm_num)
  54  linarith
  55
  56/- PROVEN: α < 1/2 (since 1 − 1/φ < 1). -/
  57theorem alpha_lt_half : alpha_from_phi < 1 / 2 := by
  58  unfold alpha_from_phi
  59  have hφ_pos : 0 < Constants.phi := Constants.phi_pos
  60  have : 1 - 1 / Constants.phi < 1 := by
  61    have : 0 < 1 / Constants.phi := div_pos (by norm_num) hφ_pos
  62    linarith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.