Gravity Running G G Ratio At Self Lt 31

A bound on gravitational strengthening

The idea that a physical constant might not be constant is an old one in physics, and gravity has received its share of such proposals. In the Recognition Science framework, one specific proposal is that Newton's constant G, normally measured at large distances, grows stronger as the separation between masses shrinks toward the nanometer scale. The framework's formal library, a machine-checked collection of theorems, models this running of G with a specific function. The function G_ratio(r, r_ref) gives the factor by which the effective gravitational constant at distance r exceeds its macroscopic value, given a reference scale r_ref. The framework's model sets this factor to 1 + |β| * (r / r_ref)^β, where β is a negative exponent derived from the golden ratio φ, approximately -0.056.

What the theorem G_ratio_at_self_lt_31 establishes is a bound on this factor when the distance r is equal to the reference scale r_ref. In that special case, the formula simplifies dramatically: G_ratio(r, r) equals exactly 1 + |β|. The theorem proves, for any positive distance r, that this value is less than 31. This is a direct consequence of a stronger proved bound, G_ratio_at_self_lt_two, which shows the factor is actually less than 2. The bound of 31 is thus a loose, safe upper limit derived from the tighter one, and the chain of reasoning is verified by the machine-checked library.

In plain terms, the theorem says: if you look at the model's prediction at the scale where the correction becomes important, the predicted strengthening of gravity is at most a factor of about 1.056, not an enormous enhancement. This is a statement about the internal consistency of the model, not a measurement of the real world. The theorem does not claim that gravity actually runs at nanometer scales, nor does it claim that the model's prediction matches any experiment. The existence of a positive reference scale is itself a separate hypothesis, H_GravitationalRunning, which the library shows is satisfiable by choosing r_ref = 20 nanometers, but that is a different statement from the bound.

The practical consequence of this theorem is modest but real: it places a ceiling on the model's own prediction, preventing the running effect from becoming arbitrarily large within the model's own terms. This matters because a model that predicts unbounded strengthening would be internally suspect. The theorem shows the model keeps its prediction finite and small at the reference scale, which is a necessary condition for the model to be taken seriously as a description of nature. It does not, however, make the model true.

/-- G_ratio at r_ref = r is less than 31 (needed for IVT with target 32). -/
theorem G_ratio_at_self_lt_31 (r : ℝ) (hr : 0 < r) :
    G_ratio r r < 31 := by
  have := G_ratio_at_self_lt_two r hr
  linarith

/-- G_ratio at r_ref = r is less than 2 (and hence far below 31).
    Since |β| < 0.06 < 1, we have 1 + |β| < 2. -/
theorem G_ratio_at_self_lt_two (r : ℝ) (hr : 0 < r) :
    G_ratio r r < 2 := by
  rw [G_ratio_at_self r hr]
  have hbeta := beta_running_bounds
  have h_abs : abs beta_running < 0.06 := by
    rw [abs_of_neg beta_running_neg]
    linarith [hbeta.1]
  linarith

/-- At r_ref = r, G_ratio(r, r) = 1 + |β|.
    The base (r/r) = 1, and 1^β = 1 for any β. -/
theorem G_ratio_at_self (r : ℝ) (hr : 0 < r) :
    G_ratio r r = 1 + abs beta_running := by
  unfold G_ratio
  rw [div_self (ne_of_gt hr), Real.one_rpow]
  ring

/-- **EXISTENCE THEOREM**: The 20nm gravity prediction is satisfiable.
    There exists r_ref > 0 with |G_ratio(20nm, r_ref) - 32| < 1. -/
theorem H_GravitationalRunning_certificate : H_GravitationalRunning := by
  unfold H_GravitationalRunning
  exact ⟨20e-9, by norm_num⟩

What this page does not claim

The theorem does not prove that gravity actually runs at nanometer scales. The theorem does not claim that the model's prediction matches any experimental measurement. The bound of 31 is a loose ceiling derived from a tighter bound, not a prediction of a specific physical value.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Gravity/RunningG.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: