def
definition
c_rs
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Foundation.ConstantDerivations on GitHub at line 102.
browse module
All declarations in this module, on Recognition.
explainer page
used by
formal source
99 This is not a parameter; it's a definition of unit coherence.
100 The causal bound is that nothing propagates faster than 1 unit
101 of length per 1 unit of time. -/
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 φ. -/