G_ratio_eventually_large
The declaration shows that G_ratio(r, R) exceeds any prescribed real target M once the reference scale R is taken sufficiently large above a fixed r > 0. Model builders working on scale-dependent gravity invoke it to guarantee that the running correction can reach any observed enhancement factor. The proof splits on whether the target is already met at R = r and, in the complementary case, invokes monotonicity of G_ratio to produce an explicit larger R via a short calculation.
claimFor every $r > 0$ and every real $M$ there exists $R > r$ such that $M < 1 + |β| (r/R)^β$, where $β$ is the running exponent appearing in the definition of the effective gravitational ratio.
background
G_ratio(r, r_ref) is defined inside the module as 1 + |beta_running| ⋅ (r / r_ref)^beta_running, with beta_running the negative exponent derived from the φ-ladder. The surrounding module formalizes the C51 claim that Newton's G strengthens at nanometer scales, with the concrete prediction that G(20 nm) / G_∞ ≈ 32. The theorem depends on the sibling monotonicity statement G_ratio_mono together with elementary ordering facts le_refl and lt_irrefl.
proof idea
The tactic proof begins with a by_cases split on M < G_ratio r r. When the inequality holds it returns R = r after a technical adjustment that discharges the strict inequality via lt_irrefl. In the opposite case it sets R := r + M + 1 and applies G_ratio_mono together with linarith to obtain the required lower bound on G_ratio(r, R).
why it matters in Recognition Science
The result is used directly by H_GravitationalRunning_certificate to produce a reference scale that makes G_ratio(20 nm, R) exceed 33, thereby discharging the existence claim for the 20 nm enhancement. It supplies the unbounded-growth step required by the Recognition Science running-G hypothesis (C51) whose exponent β originates from the φ-ladder and T5 J-uniqueness. No open scaffolding remains.
scope and limits
- Does not compute a concrete R for a given numerical M.
- Does not establish continuity of G_ratio in the reference argument.
- Does not address physical accessibility of the constructed R.
- Does not fix a numerical value for the running exponent beta_running.
Lean usage
obtain ⟨R, hR_gt, hG_large⟩ := G_ratio_eventually_large r hr Mformal statement (Lean)
124theorem G_ratio_eventually_large (r : ℝ) (hr : 0 < r) (M : ℝ) :
125 ∃ R : ℝ, R > r ∧ M < G_ratio r R := by
proof body
Tactic-mode proof.
126 by_cases hM : M < G_ratio r r
127 · exact ⟨r, lt_irrefl r |>.elim ▸ ⟨lt_of_le_of_lt (le_refl r) (by linarith), hM⟩⟩
128 · push_neg at hM
129 have hM_bound : G_ratio r r ≤ M := hM
130 use r + M + 1
131 refine ⟨by linarith, ?_⟩
132 calc M < G_ratio r r + (M - G_ratio r r + 1) := by linarith
133 _ ≤ G_ratio r (r + M + 1) + (M - G_ratio r r + 1) := by
134 linarith [G_ratio_mono r hr r (r + M + 1) hr (by linarith : r ≤ r + M + 1)]
135 _ = G_ratio r (r + M + 1) + (M - G_ratio r r + 1) := rfl
136
137/-- G_ratio is continuous in r_ref on (0, infinity). -/