hbar_bounds
Bounds on the reduced Planck constant ħ in RS-native units are proved to lie strictly between 0.088 and 0.093 once the golden ratio φ is confined to (1.61, 1.62). Workers on mass predictions and numerical certificates in Recognition Science reference this interval to fix ħ = φ^{-5}. The argument rewrites ħ via its defining identity and propagates the φ bounds through power and reciprocal inequalities with explicit numerical checks.
claimWith $1.61 < phi < 1.62$, the reduced Planck constant satisfies $0.088 < hbar < 0.093$ in RS-native units, where $hbar := phi^{-5}$.
background
The module sets the fundamental time quantum as the tick τ₀ = 1. The golden ratio φ satisfies the self-similar fixed-point equation and receives tight bounds from the lemmas phi_gt_onePointSixOne and phi_lt_onePointSixTwo. The reduced Planck constant is introduced as hbar = cLagLock · τ₀ and satisfies the identity hbar = phi^{-5} from the upstream lemma hbar_eq_phi_inv_fifth, quoted as: THEOREM C-004.1: ℏ = φ⁻⁵ in RS-native units. This places the result in the setting where physical constants are expressed in voxel/tick units with c = 1.
proof idea
After rewriting with hbar_eq_phi_inv_fifth, the proof invokes phi_gt_onePointSixOne and phi_lt_onePointSixTwo. It lifts these to strict inequalities on phi^5 using Real.rpow_lt_rpow. Reciprocal bounds are obtained via one_div_lt_one_div and div_lt_div_iff₀, followed by norm_num verification that 1/(1.62)^5 exceeds 0.088 while 1/(1.61)^5 falls below 0.093, then linarith closes the interval.
why it matters in Recognition Science
The declaration supplies the interval used verbatim by hbar_range in NumericalPredictions, which forms part of the structure NumericalPredictionsCert that certifies all numerical predictions including alpha inverse in (137.030, 137.039). It completes THEOREM C-004.5 of the constants sequence, linking the quantum scale to the phi fixed point of the forcing chain. The result closes the numerical anchor for the phi-ladder mass formulas without introducing open scaffolding.
scope and limits
- Does not compute an exact closed-form value for ħ.
- Does not prove the bounds on φ from first principles.
- Does not extend to other unit systems or relativistic corrections.
- Does not incorporate uncertainty from higher-tier effects in nucleosynthesis.
Lean usage
theorem hbar_range : (0.088 : ℝ) < hbar ∧ hbar < (0.093 : ℝ) := hbar_boundsformal statement (Lean)
354theorem hbar_bounds : (0.088 : ℝ) < hbar ∧ hbar < (0.093 : ℝ) := by
proof body
Tactic-mode proof.
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]
385 have h_numeric : 1 / ((1.62 : ℝ) ^ (5 : ℝ)) > (0.088 : ℝ) := by
386 rw [show (5 : ℝ) = (5 : ℕ) by norm_num, Real.rpow_natCast]
387 norm_num
388 linarith
389 have hbar_upper : phi ^ (-(5 : ℝ)) < (0.093 : ℝ) := by
390 have h_inv : phi ^ (-(5 : ℝ)) = 1 / (phi ^ (5 : ℝ)) := by
391 rw [show (-(5 : ℝ)) = - (5 : ℝ) by norm_num]
392 rw [Real.rpow_neg]
393 · ring
394 · exact le_of_lt phi_pos
395 rw [h_inv]
396 -- Since φ^5 > 1.61^5, we have 1/φ^5 < 1/1.61^5
397 -- Compute 1.61^5 = 10.817... and 1/10.817 ≈ 0.0924 < 0.093
398 have h_div : 1 / (phi ^ (5 : ℝ)) < 1 / ((1.61 : ℝ) ^ (5 : ℝ)) := by
399 apply (div_lt_div_iff₀ (by positivity) (by positivity)).mpr
400 linarith [h_phi5_lower]
401 have h_numeric : 1 / ((1.61 : ℝ) ^ (5 : ℝ)) < (0.093 : ℝ) := by
402 rw [show (5 : ℝ) = (5 : ℕ) by norm_num, Real.rpow_natCast]
403 norm_num
404 linarith
405 exact ⟨hbar_lower, hbar_upper⟩
406
407/-- The speed of light c in RS-native units (voxel/tick). -/