r_ref_exact
plain-language theorem explainer
The definition supplies the explicit reference scale r_ref that makes the gravitational running ratio exactly equal to a chosen target value. Physicists modeling nanoscale gravity enhancements would cite it when solving for the scale at which G_eff reaches a specific multiple of G_infinity. It is obtained by algebraic inversion of the G_ratio expression involving the running exponent beta.
Claim. The reference scale $r_{ref}$ satisfying $G_{ratio}(r, r_{ref}) = t$ is given by $r ((t-1)/|β|)^{1/β}$, where $β = -(φ-1)/φ^5$ is the running exponent from the φ-ladder.
background
The module formalizes the prediction that Newton's G runs with scale and strengthens at nanometer distances. G_ratio(r, r_ref) is defined as 1 + |beta_running| * (r / r_ref)^beta_running, with beta_running := -(phi - 1)/phi^5. The explicit r_ref_exact inverts this relation to produce a prescribed target ratio, as required for quantitative predictions such as G(20 nm)/G_∞ ≈ 32.
proof idea
One-line definition obtained by solving the G_ratio equation for r_ref using the explicit form of beta_running.
why it matters
It supplies the explicit r_ref needed for the RunningGR4Cert structure that certifies gravitational running predictions, including the positivity and ordering properties proved in r_ref_exact_pos and r_ref_exact_gt_r. This supports the H_GravitationalRunning hypothesis that G strengthens at nm scales, with the exponent drawn from the φ-ladder. It closes the inversion step required for the module's quantitative nanoscale predictions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.