`phiRung_one`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.RSNativeUnits on GitHub at line 163.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

 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
 188/-- Convert tick count to octave count (integer division). -/
 189def ticksToOctaves (t : ℕ) : ℕ := t / 8
 190
 191/-- Phase within an octave (0..7). -/
 192def octavePhase (t : ℕ) : Fin 8 := ⟨t % 8, Nat.mod_lt t (by norm_num)⟩
 193

papers checked against this theorem

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