`hbar_pos`

proved

show as: view math explainer →

module: IndisputableMonolith.Constants
domain: Constants
line: 308 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants on GitHub at line 308.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 305/-- Reduced Planck constant ħ in RS-native units: ħ = E_coh · τ₀ = φ⁻⁵ · 1. -/
 306noncomputable def hbar : ℝ := cLagLock * tau0
 307
 308lemma hbar_pos : 0 < hbar := mul_pos cLagLock_pos tau0_pos
 309
 310/-- **THEOREM C-004.1**: ℏ = φ⁻⁵ in RS-native units.
 311
 312    This is the fundamental identity: ℏ = E_coh · τ₀ = φ⁻⁵ · 1 = φ⁻⁵. -/
 313lemma hbar_eq_phi_inv_fifth : hbar = phi ^ (-(5 : ℝ)) := by
 314  unfold hbar cLagLock tau0 tick
 315  simp
 316
 317/-- **THEOREM C-004.2**: ℏ is positive (required for quantum dynamics). -/
 318theorem hbar_positive : hbar > 0 := hbar_pos
 319
 320/-- **THEOREM C-004.3**: ℏ < 1 (the action quantum is small compared to natural units).
 321
 322    Proof: φ > 1 ⟹ φ⁵ > 1 ⟹ φ⁻⁵ < 1. -/
 323theorem hbar_lt_one : hbar < 1 := by
 324  rw [hbar_eq_phi_inv_fifth]
 325  have h1 : phi ^ (5 : ℝ) > 1 := by
 326    have hphi : phi > 1 := one_lt_phi
 327    have hexp : (5 : ℝ) > 0 := by norm_num
 328    have h1_lt : (1 : ℝ) < phi ^ (5 : ℝ) := by
 329      rw [← Real.one_rpow (5 : ℝ)]
 330      apply Real.rpow_lt_rpow
 331      · norm_num
 332      · linarith
 333      · norm_num
 334    linarith
 335  have h2 : phi ^ (-(5 : ℝ)) = 1 / (phi ^ (5 : ℝ)) := by
 336    rw [show (-(5 : ℝ)) = - (5 : ℝ) by norm_num]
 337    rw [Real.rpow_neg]
 338    · ring

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.