scaleByPhi

formal source

 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]
 159  exact zpow_pos phi_pos n
 160
 161lemma phiRung_zero : phiRung 0 = 1 := by simp [phiRung]
 162
 163lemma phiRung_one : phiRung 1 = phi := by simp [phiRung]
 164
 165lemma phiRung_neg_one : phiRung (-1) = 1 / phi := by
 166  simp only [phiRung, zpow_neg_one, one_div]
 167
 168lemma phiRung_add (m n : ℤ) : phiRung (m + n) = phiRung m * phiRung n := by
 169  simp only [phiRung]
 170  exact zpow_add₀ phi_ne_zero m n
 171
 172lemma phiRung_neg (n : ℤ) : phiRung (-n) = 1 / phiRung n := by
 173  simp only [phiRung, one_div]
 174  rw [zpow_neg]
 175
 176/-! ## The 8-Tick Cycle
 177
 178The fundamental ledger cycle has period 8 = 2³ (forced by D=3).
 179This defines the octave structure of RS.
 180-/
 181
 182/-- The octave period: 8 ticks. -/
 183@[simp] def octavePeriod : Time := 8 * tick
 184
 185/-- The breath cycle: 1024 ticks (8 × 128 = 8 × 2⁷). -/