  95-/
  96
  97/-- Coherence energy quantum: φ⁻⁵ ≈ 0.0902. -/
  98@[simp] noncomputable def cohQuantum : ℝ := E_coh
  99
 100/-- Convert energy count (in coh) to raw RS scale. -/
 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

papers checked against this theorem

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