G_ratio_at_self_lt_31
plain-language theorem explainer
The declaration proves that the gravitational running ratio G_ratio(r, r) is strictly less than 31 for every positive real scale r. Researchers formalizing nanoscale gravity enhancements cite this bound to support an intermediate-value argument targeting a factor of 32. The proof is a one-line wrapper that invokes the stricter bound less than 2 and applies linear arithmetic.
Claim. For every real number $r > 0$, the effective gravitational ratio satisfies $G(r, r) < 31$, where $G(r, r_0) := 1 + |β| · (r / r_0)^β$ and $β$ is the running exponent from the φ-ladder.
background
The module formalizes the running of Newton's gravitational constant at nanometer scales. The effective ratio is defined by G_ratio(r, r_ref) = 1 + |beta_running| * (r / r_ref)^beta_running, with beta_running the exponent β ≈ -0.056 derived from the φ-ladder. The local theoretical setting is the prediction that G strengthens to approximately 32 times G_∞ at 20 nm scales, as stated in the module hypothesis H_GravitationalRunning. This theorem depends on the upstream result G_ratio_at_self_lt_two, whose doc-comment states: 'G_ratio at r_ref = r is less than 2 (and hence far below 31). Since |β| < 0.06 < 1, we have 1 + |β| < 2.'
proof idea
The proof is a one-line wrapper that applies the theorem G_ratio_at_self_lt_two r hr to obtain G_ratio r r < 2, then invokes linarith to conclude the weaker inequality G_ratio r r < 31.
why it matters
This bound is invoked inside the existence theorem H_GravitationalRunning_certificate, whose doc-comment states: 'EXISTENCE THEOREM: The 20nm gravity prediction is satisfiable. There exists r_ref > 0 with |G_ratio(20nm, r_ref) - 32| < 1.' It supplies the upper estimate required for the intermediate-value step that discharges the gravitational-running hypothesis at nanometer scales, consistent with the φ-ladder and eight-tick structure of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.