beta_running_neg
plain-language theorem explainer
The running exponent β for gravitational strengthening at nanometer scales is strictly negative. Researchers modeling scale-dependent Newton's constant G would cite this to fix the sign of the correction term in the effective G formula. The proof is a one-line wrapper that applies the numerical bounds theorem via linarith on its second component.
Claim. $β < 0$, where $β = -(φ - 1)/φ^5$ and $φ$ denotes the golden ratio.
background
The module formalizes the prediction that Newton's gravitational constant G runs with scale, strengthening at nanometer distances according to the φ-ladder. The running exponent is defined as β = -(φ - 1)/φ^5 ≈ -0.056, with the effective form G_eff(r) = G_∞ * (1 + |β| * (r / r_ref)^β). Upstream, beta_running_bounds supplies the interval -0.06 < β < -0.05 obtained from φ ∈ (1.61, 1.62) and the identity φ^5 = 5φ + 3.
proof idea
The proof applies beta_running_bounds, which yields the pair of inequalities -0.06 < beta_running ∧ beta_running < -0.05, then invokes linarith on the second conjunct to conclude beta_running < 0.
why it matters
This sign result is required by the four immediate downstream theorems: abs_beta_running_pos (which extracts 0 < |β|), G_ratio_at_self_lt_two, G_ratio_mono (which relies on β < 0 for monotonicity in r_ref), and r_ref_exact_gt_r. It fills the sign step in the C51 prediction that G strengthens at small r, consistent with the φ-ladder exponent derived from the Recognition forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.