def
definition
hbarQuantum
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.RSNativeUnits on GitHub at line 104.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
101@[simp] noncomputable def energy_raw (E : Energy) : ℝ := E * cohQuantum
102
103/-- Action quantum: ħ = E_coh · τ₀ = E_coh in RS-native units. -/
104@[simp] noncomputable def hbarQuantum : ℝ := cohQuantum * tick
105
106/-- Convert action count (in act) to raw RS scale. -/
107@[simp] noncomputable def action_raw (A : Action) : ℝ := A * hbarQuantum
108
109@[simp] lemma hbarQuantum_eq_Ecoh : hbarQuantum = E_coh := by
110 simp [hbarQuantum, cohQuantum, tick]
111
112/-! ## Mass quantum (derived from E = mc²)
113
114In RS-native units with c = 1:
115- Mass = Energy (mass-energy equivalence)
116- 1 mass quantum = 1 coh (in c=1 units)
117-/
118
119/-- Mass quantum: 1 coh/c² = 1 coh (since c = 1). -/
120@[simp] noncomputable def massQuantum : ℝ := cohQuantum
121
122/-- Convert mass count to raw RS scale. -/
123@[simp] noncomputable def mass_raw (m : Mass) : ℝ := m * massQuantum
124
125/-! ## Frequency and momentum quanta -/
126
127/-- Frequency quantum: 1/tick (inverse of fundamental time). -/
128@[simp] noncomputable def freqQuantum : Frequency := 1 / tick
129
130/-- Convert frequency to raw RS scale. -/
131@[simp] noncomputable def freq_raw (f : Frequency) : ℝ := f * freqQuantum
132
133/-- Momentum quantum: E_coh/c = E_coh (since c = 1). -/
134@[simp] noncomputable def momentumQuantum : ℝ := cohQuantum / c