G_ratio_eventually_large
plain-language theorem explainer
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.
Claim. For 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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.