G_ratio_continuous_snd
plain-language theorem explainer
G_ratio_continuous_snd asserts that for any fixed positive scale r the map r_ref to the gravitational ratio correction 1 + |β|(r/r_ref)^β is continuous on the positive reals. Researchers modeling nanoscale running of Newton's G cite it to justify limits and approximations in the 20 nm enhancement prediction. The term proof unfolds the explicit formula and chains library lemmas for continuity of addition, constant multiplication, and real exponentiation.
Claim. For fixed $r > 0$, the map $r_ref ↦ 1 + |β| (r / r_ref)^β$ is continuous on $(0, ∞)$, where $β$ is the running exponent from the φ-ladder.
background
The RunningG module formalizes the hypothesis that Newton's G strengthens at nanometer scales via G_eff(r) = G_∞ (1 + |β| (r / r_ref)^β) with β ≈ -0.056. G_ratio(r, r_ref) is the explicit multiplicative correction factor 1 + |β| (r / r_ref)^β. Continuity in the reference scale r_ref is needed so that the function attains values near 32 at r = 20 nm for some positive r_ref.
proof idea
Unfold G_ratio to expose the sum of a constant and a constant multiple of a power. Apply ContinuousOn.add with continuousOn_const, then ContinuousOn.mul with continuousOn_const, followed by ContinuousOn.rpow_const. The base division r/x is continuous on positive reals by ContinuousOn.div, with the positivity hypothesis hr ensuring the denominator is never zero.
why it matters
This lemma supports the downstream existence certificate H_GravitationalRunning_certificate that constructs an r_ref making |G_ratio(20 nm, r_ref) - 32| < 1. It supplies the required analytic regularity for the C51 nanoscale gravity prediction inside Recognition Science, where the exponent β originates from the φ-ladder fixed point. No open scaffolding remains in this declaration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.