G_ratio

formal source

  52    linarith
  53
  54/-- Effective G at scale r relative to G_infinity. -/
  55noncomputable def G_ratio (r r_ref : ℝ) : ℝ :=
  56    1 + abs beta_running * (r / r_ref) ^ beta_running
  57
  58/-- **HYPOTHESIS H_GravitationalRunning**: Gravity strengthens at nm scales.
  59    Prediction: G(20nm) / G_inf ≈ 32. -/
  60def H_GravitationalRunning : Prop :=
  61  ∃ r_ref : ℝ, r_ref > 0 ∧
  62    abs (G_ratio 20e-9 r_ref - 32) < 1.0
  63
  64/-! ## Structural Properties of G_ratio -/
  65
  66/-- beta_running is strictly negative. -/
  67theorem beta_running_neg : beta_running < 0 := by
  68  have := beta_running_bounds
  69  linarith [this.2]
  70
  71/-- |beta_running| is strictly positive. -/
  72theorem abs_beta_running_pos : 0 < abs beta_running := by
  73  exact abs_pos.mpr (ne_of_lt beta_running_neg)
  74
  75/-- At r_ref = r, G_ratio(r, r) = 1 + |β|.
  76    The base (r/r) = 1, and 1^β = 1 for any β. -/
  77theorem G_ratio_at_self (r : ℝ) (hr : 0 < r) :
  78    G_ratio r r = 1 + abs beta_running := by
  79  unfold G_ratio
  80  rw [div_self (ne_of_gt hr), Real.one_rpow]
  81  ring
  82
  83/-- G_ratio at r_ref = r is less than 2 (and hence far below 31).
  84    Since |β| < 0.06 < 1, we have 1 + |β| < 2. -/
  85theorem G_ratio_at_self_lt_two (r : ℝ) (hr : 0 < r) :