r_ref_exact_pos
plain-language theorem explainer
The theorem establishes that the exact reference scale r_ref_exact(r, target) is strictly positive whenever the measurement scale r exceeds zero and the target ratio exceeds one. Modelers of scale-dependent gravity at nanometer distances cite this to guarantee a positive reference length in running-G formulas. The proof is a short term-mode script that unfolds the definition then chains mul_pos, Real.rpow_pos_of_pos, and div_pos using the already-proved positivity of |beta_running|.
Claim. If $r > 0$ and $target > 1$, then the exact reference scale $r_ {rm ref}(r, target)$ solving $G_ {rm ratio}(r, r_ {rm ref}) = target$ satisfies $r_ {rm ref}(r, target) > 0$.
background
Module Gravity.RunningG formalizes the hypothesis that Newton's constant strengthens at nanometer scales: $G_ {rm eff}(r) = G_ {infty} (1 + |beta| (r / r_ {rm ref})^beta)$ with $beta = -(phi-1)/phi^5 approx -0.056$. The reference scale $r_ {rm ref}$ is defined so the correction term reaches order unity at that length. G_ratio is the explicit function $1 + |beta_running| (r / r_ {rm ref})^beta_running$ and abs_beta_running_pos records that this absolute value is positive. Upstream, scale from LargeScaleStructureFromRS supplies the phi-powered lengths on the ladder, while the module doc states the macroscopic limit $G(r) to G_infty$ as $r to infty$ and the nanoscale prediction $G(20 nm) approx 32 G_infty$.
proof idea
The proof is a term-mode script. It unfolds r_ref_exact, applies mul_pos to the hypothesis 0 < r, then Real.rpow_pos_of_pos to the base of the power. The remaining positivity of the exponent is discharged by div_pos on a linear inequality together with the upstream theorem abs_beta_running_pos.
why it matters
This supplies the explicit positivity witness r_ref_explicit inside the certificate running_g_r4_cert, which also records r_ref_above_r and the H_GravitationalRunning hypothesis. It closes one link from the phi-ladder (T5 J-uniqueness through T8 D=3) and the Recognition Composition Law to the concrete prediction of 32-fold gravitational enhancement at 20 nm. The result touches the open question whether beta acquires scale-dependent corrections beyond the leading phi-ladder term.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.