planckEnergy_rs

formal source

 255  Real.sqrt (hbarQuantum * c / Constants.G)
 256
 257/-- Planck energy in RS units: E_P = m_P · c² = m_P (since c = 1). -/
 258noncomputable def planckEnergy_rs : Energy := planckMass_rs
 259
 260/-! ## Dimensionless Ratios (Fixed by φ)
 261
 262These ratios are the same in any unit system - they are the "physics" of RS.
 263-/
 264
 265/-- Fine structure constant inverse: α⁻¹ ≈ 137.036. -/
 266noncomputable def alphaInv_rs : ℝ := Constants.alphaInv
 267
 268/-- The K-gate ratio: K = π/(4 ln φ). -/
 269noncomputable def K_rs : ℝ := Constants.RSUnits.K_gate_ratio
 270
 271/-- Coherence scaling: E_coh = φ⁻⁵. -/
 272noncomputable def E_coh_rs : ℝ := phiRung (-5)
 273
 274lemma E_coh_rs_eq_E_coh : E_coh_rs = E_coh := by
 275  simp only [E_coh_rs, phiRung, E_coh, cLagLock]
 276  -- Both are phi^(-5), but one uses zpow and the other uses rpow
 277  -- φ^(-5 : ℤ) = φ^(-5 : ℝ) for φ > 0
 278  have h : phi ^ (-5 : ℤ) = phi ^ ((-5 : ℤ) : ℝ) := by
 279    rw [← Real.rpow_intCast phi (-5)]
 280  rw [h]
 281  congr 1
 282  norm_cast
 283
 284/-! ## External Calibration (SI Bridge)
 285
 286If you want "seconds" and "meters", you must provide an explicit calibration
 287mapping RS primitives to an external unit system. This keeps the empirical
 288seam explicit and auditable.