beta_running
plain-language theorem explainer
beta_running supplies the running exponent β for the scale dependence of Newton's gravitational constant as -(φ-1)/φ^5. Researchers modeling nanometer-scale gravitational strengthening would cite this constant when evaluating effective G(r). The declaration is introduced as a direct algebraic assignment using the golden ratio from the self-similar forcing chain.
Claim. The gravitational running exponent is defined by $β = -(φ - 1)/φ^5 ≈ -0.056$, where $φ$ is the golden ratio fixed point of the forcing chain.
background
In the Recognition Science setting, the golden ratio φ is the self-similar fixed point (T6) forced by J-uniqueness (T5), with J(x) = (x + x^{-1})/2 - 1. This module formalizes the claim that Newton's constant is not fixed but runs with distance: G(r) approaches G_∞ at large r while strengthening at nanometer scales according to the exponent β derived from the φ-ladder. The module doc states the effective form G_eff(r) = G_∞ * (1 + |β| * (r / r_ref)^β) and the target prediction G(20 nm)/G_∞ ≈ 32. The upstream structure for records the meta-realization properties required by the self-reference axioms.
proof idea
This is a direct definition that assigns the closed-form expression -(phi - 1) / (phi ^ 5) to the identifier. No lemmas or tactics are applied; the body is a single noncomputable real constant.
why it matters
The definition supplies the exponent that feeds every downstream result on gravitational running, including G_ratio, G_ratio_at_self, beta_running_bounds, and the hypothesis H_GravitationalRunning. It realizes the module-level prediction of nanoscale strengthening and connects the φ-ladder (T5-T6) to the eight-tick octave and D = 3 (T7-T8). The value also anchors the alpha band and mass-ladder constants imported from Constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.