`octavePhase`

definition

show as: view math explainer →

module: IndisputableMonolith.Constants.RSNativeUnits
domain: Constants
line: 192 · 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 192.

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

used by

formal source

 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 :
 220    tau_rec = Constants.RSUnits.K_gate_ratio := by
 221  unfold tau_rec
 222  have hlog : Real.log phi ≠ 0 := ne_of_gt (Real.log_pos one_lt_phi)

papers checked against this theorem

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