r_ref_exact_pos
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|.
claimIf $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 in Recognition Science
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.
scope and limits
- Does not compute a numerical value for r_ref_exact.
- Does not prove that target exceeds 1 + |beta_running|.
- Does not derive beta_running from the phi-ladder.
- Does not address physical units or dimensions of r and target.
Lean usage
example (r target : ℝ) (hr : 0 < r) (ht : 1 < target) : 0 < r_ref_exact r target := r_ref_exact_pos r target hr htformal statement (Lean)
211theorem r_ref_exact_pos (r target : ℝ) (hr : 0 < r) (ht : 1 < target) :
212 0 < r_ref_exact r target := by
proof body
Term-mode proof.
213 unfold r_ref_exact
214 apply mul_pos hr
215 apply Real.rpow_pos_of_pos
216 exact div_pos (by linarith) abs_beta_running_pos
217
218/-- For target > 1 + |beta| (i.e., target above the G_ratio at self),
219 r_ref_exact > r. The reference scale is LARGER than the measurement scale. -/