beta_running_bounds
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 in Recognition Science
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.
scope and limits
- Does not derive the functional form of the running law from the Recognition Composition Law.
- Does not compute the exact numerical value of beta_running.
- Does not address higher-order corrections beyond the leading exponent.
- Does not connect to the J-cost functional or defect distance.
formal statement (Lean)
36theorem beta_running_bounds :
37 -0.06 < beta_running ∧ beta_running < -0.05 := by
proof body
Tactic-mode proof.
38 unfold beta_running
39 -- Use phi_fifth_eq: φ^5 = 5φ + 3
40 rw [phi_fifth_eq]
41 -- We want to prove: -0.06 < -(φ - 1) / (5φ + 3) < -0.05
42 have h_phi_pos : 0 < phi := phi_pos
43 have h_denom_pos : 0 < 5 * phi + 3 := by linarith
44 constructor
45 · -- -0.06 < -(φ - 1) / (5φ + 3)
46 rw [lt_div_iff₀ h_denom_pos]
47 have h_phi_lt : phi < 1.62 := phi_lt_onePointSixTwo
48 linarith
49 · -- -(φ - 1) / (5φ + 3) < -0.05
50 rw [div_lt_iff₀ h_denom_pos]
51 have h_phi_gt : 1.61 < phi := phi_gt_onePointSixOne
52 linarith
53
54/-- Effective G at scale r relative to G_infinity. -/