U_c

formal source

  84
  85@[simp] lemma U_tau0 : U.tau0 = 1 := rfl
  86@[simp] lemma U_ell0 : U.ell0 = 1 := rfl
  87@[simp] lemma U_c : U.c = 1 := rfl
  88
  89/-! ## Coherence and action quanta
  90
  91`Constants.E_coh = φ⁻⁵` is a **dimensionless** RS-derived number.
  92In the RS-native system:
  93- **1 coh** (energy quantum) := E_coh
  94- **1 act** (action quantum) := ħ = E_coh · τ₀ = E_coh (since τ₀ = 1)
  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-/