beta_running_bounds
plain-language theorem explainer
The theorem proves that the gravitational running exponent satisfies -0.06 < beta_running < -0.05. Cosmologists modeling nanoscale corrections to Newton's constant cite the bound to control the size of the leading correction term. The proof is a short tactic script that substitutes the exact phi-fifth identity, confirms the denominator is positive, and discharges both sides of the conjunction by linear arithmetic on the known interval 1.61 < phi < 1.62.
Claim. $-0.06 < - (phi - 1) / phi^5 < -0.05$, where $phi$ is the golden ratio.
background
The module formalizes the prediction that Newton's gravitational constant runs at nanometer scales. The effective form is G_eff(r) = G_∞ (1 + |β| (r/r_ref)^β) with β = -(phi - 1)/phi^5. Upstream, phi_fifth_eq records the identity phi^5 = 5 phi + 3 obtained from the Fibonacci recurrence of the golden ratio. The constants module also supplies the tight numerical bounds 1.61 < phi < 1.62 that anchor the interval arithmetic.
proof idea
The proof unfolds beta_running, rewrites the denominator via phi_fifth_eq, proves the denominator positive by linarith, then splits the conjunction. The left inequality is rewritten with lt_div_iff₀ and discharged by linarith using the upper bound on phi; the right inequality uses div_lt_iff₀ together with the lower bound on phi and linarith.
why it matters
The bound is invoked directly by beta_running_neg to establish strict negativity and by G_ratio_at_self_lt_two to show the ratio at the reference scale remains below 2. It supplies the numerical anchor required for the C51 prediction of G enhancement at 20 nm scales. Within the Recognition framework it closes the interval estimate on the phi-ladder exponent before monotonicity and large-scale limits are derived.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.