r_ref_exact_gt_r
plain-language theorem explainer
r_ref_exact_gt_r asserts that the exact reference scale exceeds the input scale r whenever the target ratio lies above 1 + |beta_running|. Nanoscale gravity modelers cite the result to guarantee r_ref sits above the probed distance for large enhancement factors. The proof unfolds the definition of r_ref_exact then chains positivity, one_lt_rpow, and mul_lt_mul_of_pos_left on the real power term.
Claim. Let $r > 0$ and let $t > 1 + |beta|$ where $beta$ is the running exponent. Then $r < r_ref(r, t)$ with $r_ref(r, t) := r · ((t-1)/|beta|)^{1/beta}$.
background
The module formalizes the C51 claim that Newton's G runs at nanometer scales: G_eff(r) = G_∞ · (1 + |beta| · (r/r_ref)^beta) with beta = -(phi-1)/phi^5. G_ratio(r, r_ref) is the explicit enhancement factor 1 + |beta| · (r/r_ref)^beta. Upstream results supply the phi-ladder rung structure (NucleosynthesisTiers.of) and the Planck length ell_P for unit conversion; the local setting is the prediction that the enhancement reaches 32 at r ≈ 20 nm.
proof idea
The tactic proof unfolds r_ref_exact. It proves (target-1)/|beta| > 1 by one_lt_div and linarith, shows the exponent 1/beta < 0 by div_neg_of_pos_of_neg, verifies the rpow term is positive, then applies mul_lt_mul_of_pos_left together with one_lt_rpow to obtain the strict inequality after rewriting r = r · 1.
why it matters
The result is invoked inside running_g_r4_cert as the field r_ref_above_r, completing the certificate that assembles r_ref_explicit, rung_near_360 and the H_GravitationalRunning hypothesis. It fills the nanoscale gravity step of the Recognition Science chain (T5 J-uniqueness and T6 phi fixed point determine beta), confirming that the reference scale lies above the measurement scale when the target exceeds the self-ratio.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.