def
definition
massQuantum
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Constants.RSNativeUnits on GitHub at line 120.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
117-/
118
119/-- Mass quantum: 1 coh/c² = 1 coh (since c = 1). -/
120@[simp] noncomputable def massQuantum : ℝ := cohQuantum
121
122/-- Convert mass count to raw RS scale. -/
123@[simp] noncomputable def mass_raw (m : Mass) : ℝ := m * massQuantum
124
125/-! ## Frequency and momentum quanta -/
126
127/-- Frequency quantum: 1/tick (inverse of fundamental time). -/
128@[simp] noncomputable def freqQuantum : Frequency := 1 / tick
129
130/-- Convert frequency to raw RS scale. -/
131@[simp] noncomputable def freq_raw (f : Frequency) : ℝ := f * freqQuantum
132
133/-- Momentum quantum: E_coh/c = E_coh (since c = 1). -/
134@[simp] noncomputable def momentumQuantum : ℝ := cohQuantum / c
135
136/-- Convert momentum to raw RS scale. -/
137@[simp] noncomputable def momentum_raw (p : Momentum) : ℝ := p * momentumQuantum
138
139@[simp] lemma momentumQuantum_eq_cohQuantum : momentumQuantum = cohQuantum := by
140 simp [momentumQuantum, c]
141
142/-! ## The φ-Ladder: Scaling in RS
143
144All RS quantities are organized on a φ-ladder. The ladder provides:
145- Mass rungs: m_n = m₀ · φⁿ
146- Time rungs: τ_n = τ₀ · φⁿ
147- Length rungs: ℓ_n = ℓ₀ · φⁿ
148- Energy rungs: E_n = E₀ · φⁿ
149-/
150