planckLength_rs

formal source

 246  tick * Real.sqrt (Constants.G / (c ^ 3))
 247
 248/-- Planck length in RS units: ℓ_P = c · τ_P. -/
 249noncomputable def planckLength_rs : Length :=
 250  c * planckTime_rs
 251
 252/-- Planck mass in RS units: m_P = √(ħc/G).
 253    This is the mass at which gravitational and quantum scales meet. -/
 254noncomputable def planckMass_rs : Mass :=
 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)]