G_ratio_mono
plain-language theorem explainer
The theorem shows that for fixed r > 0 the gravitational enhancement factor G_ratio(r, R) increases with the reference scale R. Modelers of nanoscale gravity strengthening cite it to guarantee consistent growth of the effective constant as the reference lengthens. The proof unfolds the definition, invokes the sign and positivity lemmas on the running exponent, reduces to a base comparison, and applies the real-power monotonicity rule for negative exponents.
Claim. Let $r > 0$ and $0 < R_1 ≤ R_2$. Let $β < 0$ be the running exponent. Then $1 + |β| (r / R_1)^β ≤ 1 + |β| (r / R_2)^β$.
background
The module formalizes gravitational running at nanometer scales under the hypothesis that Newton's constant strengthens below macroscopic distances. The effective ratio is defined by G_ratio(r, r_ref) := 1 + |β| (r / r_ref)^β, where β = -(φ - 1)/φ^5 is the running exponent taken from the φ-ladder. Upstream lemmas establish that β is strictly negative and |β| is positive, which are the only properties required for the monotonicity argument.
proof idea
Unfold the definition of G_ratio. Obtain 0 < |β| from abs_beta_running_pos and β < 0 from beta_running_neg. Reduce the target inequality to (r/R1)^β ≤ (r/R2)^β by multiplying through by the positive factor |β| and applying linarith. Conclude by invoking Real.rpow_le_rpow_of_exponent_le on the positive bases r/R1 ≥ r/R2 and the negative exponent.
why it matters
The result is used by G_ratio_eventually_large to show that the enhancement factor can be driven arbitrarily large by increasing the reference scale. It supports the H_GravitationalRunning hypothesis inside the Recognition framework, where the exponent β originates from the φ-ladder fixed point and the eight-tick octave structure. The monotonicity is a direct algebraic consequence of the negative exponent and is required for the unbounded-growth claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.