pith. machine review for the scientific record. sign in
theorem proved tactic proof

r_ref_exact_gt_r

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 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

proof body

Tactic-mode proof.

 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:
 238  r_ref = 20e-9 * (31/|beta|)^(1/beta)
 239  |beta| ~ 0.0557, 1/beta ~ -17.95
 240  31/0.0557 ~ 556.6
 241  556.6^(-17.95) ~ 1.83e49
 242  r_ref ~ 20e-9 * 1.83e49 ~ 3.66e41 m
 243
 244In Planck units (ell_P ~ 1.6e-35 m):
 245  r_ref / ell_P ~ 2.3e76
 246  log_phi(2.3e76) ~ 76 * ln(10) / ln(phi) ~ 76 * 2.303 / 0.481 ~ 364
 247
 248So r_ref sits near phi-rung N ~ 364.
 249
 250Significance: 364 = 4 * 91 = 4 * 7 * 13.
 251Also: 364 = F_14 - 13 (where F_14 = 377).
 252And: 364 = 8 * 45 + 4 = 8 * 45.5 (close to 8 * gap_45 = 360).
 253
 254The nearest "clean" RS number is 360 = lcm(8, 45) = sync_period from
 255Foundation.DimensionForcing. So r_ref ~ ell_P * phi^360 is suggestive. -/
 256
 257/-- The approximate phi-rung of r_ref for the 20nm/32x prediction. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (31)

Lean names referenced from this declaration's body.

… and 1 more