lemma
proved
phiRung_pos
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Constants.RSNativeUnits on GitHub at line 157.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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⁷). -/
186@[simp] def breathCycle : Time := 1024 * tick
187