c_rs_eq_one

formal source

 102noncomputable def c_rs : ℝ := ℓ₀ / τ₀
 103
 104/-- c = 1 in RS-native units. -/
 105theorem c_rs_eq_one : c_rs = 1 := by
 106  unfold c_rs ℓ₀ τ₀
 107  norm_num
 108
 109/-- c > 0. -/
 110theorem c_pos : c_rs > 0 := by rw [c_rs_eq_one]; norm_num
 111
 112/-! ## Planck's Constant: ℏ = E_coh · τ₀ -/
 113
 114/-- **Planck's reduced constant** in RS-native units.
 115
 116    ℏ is the product of coherence energy and fundamental time.
 117    This sets the scale of the IR gate (minimum action for coherent state).
 118
 119    In RS-native units: ℏ = φ^(-5) · 1 = φ^(-5). -/
 120noncomputable def ℏ_rs : ℝ := E_coh * τ₀
 121
 122/-- ℏ = φ^(-5) in RS-native units. -/
 123theorem ℏ_rs_eq : ℏ_rs = φ_val^(-5 : ℤ) := by
 124  unfold ℏ_rs E_coh τ₀
 125  ring
 126
 127/-- ℏ > 0. -/
 128theorem ℏ_pos : ℏ_rs > 0 := by
 129  rw [ℏ_rs_eq]
 130  exact zpow_pos phi_pos (-5)
 131
 132/-- ℏ is algebraic in φ. -/
 133theorem ℏ_algebraic_in_φ : ∃ n : ℤ, ℏ_rs = φ_val^n := ⟨-5, ℏ_rs_eq⟩
 134
 135/-! ## Gravitational Constant: G -/