theorem
proved
hbar_bounds
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants on GitHub at line 354.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
-
of -
hbar -
hbar_eq_phi_inv_fifth -
phi_gt_onePointSixOne -
phi_lt_onePointSixTwo -
tick -
hbar -
tick -
voxel -
of -
of -
of -
hbar -
of -
and -
hbar
used by
formal source
351/-- **THEOREM C-004.5**: Bounds on ℏ from φ bounds.
352
353 With φ ∈ (1.61, 1.62), we get ℏ ∈ (0.088, 0.093). -/
354theorem hbar_bounds : (0.088 : ℝ) < hbar ∧ hbar < (0.093 : ℝ) := by
355 rw [hbar_eq_phi_inv_fifth]
356 have h1 : (1.61 : ℝ) < phi := phi_gt_onePointSixOne
357 have h2 : phi < (1.62 : ℝ) := phi_lt_onePointSixTwo
358 -- We want 0.088 < φ^(-5) < 0.093
359 -- Since hbar = 1/φ^5, we need bounds on φ^5
360 -- Lower bound: φ < 1.62, so φ^5 < 1.62^5, so 1/φ^5 > 1/1.62^5
361 -- Upper bound: φ > 1.61, so φ^5 > 1.61^5, so 1/φ^5 < 1/1.61^5
362 have h_phi5_lower : phi ^ (5 : ℝ) > (1.61 : ℝ) ^ (5 : ℝ) := by
363 apply Real.rpow_lt_rpow
364 · linarith
365 · linarith
366 · norm_num
367 have h_phi5_upper : phi ^ (5 : ℝ) < (1.62 : ℝ) ^ (5 : ℝ) := by
368 apply Real.rpow_lt_rpow
369 · linarith
370 · linarith
371 · norm_num
372 -- Convert to hbar = φ^(-5) bounds
373 have hbar_lower : phi ^ (-(5 : ℝ)) > (0.088 : ℝ) := by
374 have h_inv : phi ^ (-(5 : ℝ)) = 1 / (phi ^ (5 : ℝ)) := by
375 rw [show (-(5 : ℝ)) = - (5 : ℝ) by norm_num]
376 rw [Real.rpow_neg]
377 · ring
378 · exact le_of_lt phi_pos
379 rw [h_inv]
380 -- Since φ^5 < 1.62^5, we have 1/φ^5 > 1/1.62^5
381 -- Compute 1.62^5 = 11.158... and 1/11.158 ≈ 0.0896 > 0.088
382 have h_div : 1 / (phi ^ (5 : ℝ)) > 1 / ((1.62 : ℝ) ^ (5 : ℝ)) := by
383 apply (one_div_lt_one_div (by positivity) (by positivity)).mpr
384 linarith [h_phi5_upper]