`phiRung_neg`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.RSNativeUnits on GitHub at line 172.

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

 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
 194/-! ## Gap-45 Synchronization
 195
 196The gap-45 rung (φ⁴⁵) provides critical phase synchronization:
 197- lcm(8, 45) = 360 synchronizes the octave and gap cycles
 198- This forces D = 3 as the unique dimension with this property
 199-/
 200
 201/-- The gap-45 rung: φ⁴⁵. -/
 202@[simp] noncomputable def gap45 : ℝ := phiRung 45

papers checked against this theorem

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