Gravity Running G G Ratio Continuous Snd

A smooth ratio

Newton's gravitational constant G is usually treated as a fixed number. In Recognition Science, the framework models it as a quantity that changes with the distance between masses, a behavior called running. The central object is a ratio, G_ratio(r, R), which compares the effective strength at distance r against a reference scale R. The declaration G_ratio_continuous_snd proves that for any fixed positive r, this ratio is a continuous function of the reference scale R on the entire positive real line. Continuity here means small changes in the reference distance produce small changes in the ratio, with no sudden jumps or breaks. This is a purely mathematical statement about the defined formula, not yet a physical measurement.

The formula itself is G_ratio(r, R) = 1 + |β| * (r / R)^β, where β is a negative exponent, approximately -0.056. The theorem establishes that this expression is well-behaved: it does not blow up or oscillate erratically as R varies. This continuity is a prerequisite for the framework's more ambitious claims, such as the prediction that G strengthens by a factor of about 32 at a scale near 20 nanometers. Without continuity, that prediction could not be stated as a smooth trend. The proof is carried out in the framework's machine-checked library of formal theorems, meaning every step is verified by a computer.

What this declaration does not claim is just as important. It does not assert that G actually runs in nature; that is a separate hypothesis, tagged as a prediction with a named falsifier. It does not give the physical value of the running exponent or the reference scale; those are defined constants, not derived results. And it does not prove that the ratio is continuous at r = 0 or for negative distances, which are outside its scope. The theorem is a technical foundation, a guarantee that the mathematical machinery is smooth, not a verdict on the physics itself.

/-- G_ratio is continuous in r_ref on (0, infinity). -/
theorem G_ratio_continuous_snd (r : ℝ) (hr : 0 < r) :
    ContinuousOn (G_ratio r) (Set.Ioi 0) := by
  unfold G_ratio
  apply ContinuousOn.add continuousOn_const
  apply ContinuousOn.mul continuousOn_const
  apply ContinuousOn.rpow_const
  · exact ContinuousOn.div continuousOn_const continuousOn_id (fun x hx => ne_of_gt hx)
  · exact fun x hx => Or.inl (ne_of_gt (div_pos hr hx))

What this page does not claim

The theorem does not prove that G actually runs in physical reality. The theorem does not provide the numerical value of the running exponent or the reference scale. The theorem does not apply to zero or negative distances.

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: