abs_beta_running_pos
The absolute value of the gravitational running exponent β is strictly positive. Modelers of scale-dependent gravity cite this to guarantee that the correction factor in G_eff(r) remains positive for all r. The proof is a one-line wrapper applying the absolute-value positivity lemma to the already-proved negativity of β.
claim$0 < |β|$ where $β = -(φ-1)/φ^5$ is the running exponent for gravitational strengthening.
background
The module formalizes gravitational running at nanometer scales: G_eff(r) = G_∞ ⋅ (1 + |β| ⋅ (r/r_ref)^β) with β derived from the φ-ladder. beta_running is defined as -(phi - 1) / (phi ^ 5) and beta_running_neg establishes β < 0 using the numerical bounds on phi. G_ratio then folds in abs beta_running to produce the effective ratio relative to G_∞. The local setting is the hypothesis that gravity strengthens at r ≈ 20 nm to roughly 32 times its macroscopic value.
proof idea
One-line wrapper that applies abs_pos.mpr to the strict inequality beta_running_neg.
why it matters in Recognition Science
This sign fact is required for all downstream positivity and monotonicity statements on G_ratio. It is invoked directly by G_ratio_at_self_pos, G_ratio_mono, r_ref_exact_gt_r and r_ref_exact_pos. In the Recognition framework it supplies the positivity half of the β correction that produces the predicted nanoscale enhancement; without it the running model would not guarantee G(r) > G_∞.
scope and limits
- Does not compute the numerical magnitude of β.
- Does not derive β from the φ-ladder axioms.
- Does not prove the running law itself, only the sign of |β|.
- Does not address convergence or validity at r = 0.
Lean usage
theorem G_ratio_at_self_pos (r : ℝ) (hr : 0 < r) : 0 < G_ratio r r := by rw [G_ratio_at_self r hr]; linarith [abs_beta_running_pos]formal statement (Lean)
72theorem abs_beta_running_pos : 0 < abs beta_running := by
proof body
Term-mode proof.
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 β. -/