 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
 154/-- Scale any quantity by n rungs on the φ-ladder. -/
 155@[simp] noncomputable def scaleByPhi (x : ℝ) (n : ℤ) : ℝ := x * phiRung n
 156
 157lemma phiRung_pos (n : ℤ) : 0 < phiRung n := by
 158  simp [phiRung]

papers checked against this theorem

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