r_ref_exact

formal source

 204
 205/-- The explicit r_ref that gives G_ratio(r, r_ref) = target.
 206    Derived by inverting the G_ratio formula. -/
 207noncomputable def r_ref_exact (r target : ℝ) : ℝ :=
 208  r * ((target - 1) / abs beta_running) ^ (1 / beta_running)
 209
 210/-- r_ref_exact is positive when r > 0 and target > 1. -/
 211theorem r_ref_exact_pos (r target : ℝ) (hr : 0 < r) (ht : 1 < target) :
 212    0 < r_ref_exact r target := by
 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. -/
 220theorem r_ref_exact_gt_r (r target : ℝ) (hr : 0 < r)
 221    (ht : 1 + abs beta_running < target) :
 222    r < r_ref_exact r target := by
 223  unfold r_ref_exact
 224  have h_base_gt_one : 1 < (target - 1) / abs beta_running := by
 225    rw [one_lt_div abs_beta_running_pos]; linarith
 226  have h_exp_neg : 1 / beta_running < 0 := by
 227    apply div_neg_of_pos_of_neg one_pos beta_running_neg
 228  have h_rpow_pos : 0 < ((target - 1) / abs beta_running) ^ (1 / beta_running) :=
 229    Real.rpow_pos_of_pos (lt_trans one_pos h_base_gt_one) _
 230  calc r = r * 1 := by ring
 231    _ < r * ((target - 1) / abs beta_running) ^ (1 / beta_running) := by
 232        apply mul_lt_mul_of_pos_left _ hr
 233        exact Real.one_lt_rpow h_base_gt_one.le h_exp_neg
 234
 235/-! ## Phi-Ladder Rung Analysis (Path 1b)
 236
 237For target = 32, r = 20 nm: