abs_beta_running_pos
plain-language theorem explainer
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
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_∞.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.