`ticksToOctaves`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants.RSNativeUnits on GitHub at line 189.

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

 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.