`ticksToOctaves`

definition

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Constants.RSNativeUnits on GitHub at line 189.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 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
 203
 204/-- The synchronization period: lcm(8, 45) = 360. -/
 205@[simp] def syncPeriod : ℕ := 360
 206
 207lemma syncPeriod_eq_lcm : syncPeriod = Nat.lcm 8 45 := by native_decide
 208
 209/-! ## K-gate derived displays in RS-native units -/
 210
 211/-- Recognition time display: τ_rec = (2π)/(8 ln φ) · τ₀. -/
 212@[simp] noncomputable def tau_rec : Time :=
 213  Constants.RSUnits.tau_rec_display U
 214
 215/-- Kinematic wavelength display: λ_kin = (2π)/(8 ln φ) · ℓ₀. -/
 216@[simp] noncomputable def lambda_kin : Length :=
 217  Constants.RSUnits.lambda_kin_display U
 218
 219theorem tau_rec_eq_K_gate_ratio :

papers checked against this theorem

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