`mass_raw`

definition

show as: view math explainer →

module: IndisputableMonolith.Constants.RSNativeUnits
domain: Constants
line: 123 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.RSNativeUnits on GitHub at line 123.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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
 151/-- φ-ladder scaling: compute φⁿ for integer rung. -/
 152@[simp] noncomputable def phiRung (n : ℤ) : ℝ := phi ^ n
 153

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.