`tick`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Constants on GitHub at line 8.

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

   5namespace Constants
   6
   7/-- The fundamental RS time quantum (RS-native). τ₀ = 1 tick. -/
   8@[simp] def tick : ℝ := 1
   9
  10/-- Notation for fundamental tick. -/
  11abbrev τ₀ : ℝ := tick
  12
  13/-- One octave = 8 ticks: the fundamental evolution period. -/
  14def octave : ℝ := 8 * tick
  15
  16/-- Golden ratio φ as a concrete real. -/
  17noncomputable def phi : ℝ := (1 + Real.sqrt 5) / 2
  18
  19lemma phi_pos : 0 < phi := by
  20  have htwo : 0 < (2 : ℝ) := by norm_num
  21  -- Use that √5 > 0
  22  have hroot_pos : 0 < Real.sqrt 5 := by
  23    have : (0 : ℝ) < 5 := by norm_num
  24    exact Real.sqrt_pos.mpr this
  25  have hnum_pos : 0 < 1 + Real.sqrt 5 := by exact add_pos_of_pos_of_nonneg (by norm_num) (le_of_lt hroot_pos)
  26  simpa [phi] using (div_pos hnum_pos htwo)
  27
  28lemma one_lt_phi : 1 < phi := by
  29  have htwo : 0 < (2 : ℝ) := by norm_num
  30  have hsqrt_gt : Real.sqrt 1 < Real.sqrt 5 := by
  31    simpa [Real.sqrt_one] using (Real.sqrt_lt_sqrt (by norm_num) (by norm_num : (1 : ℝ) < 5))
  32  have h2lt : (2 : ℝ) < 1 + Real.sqrt 5 := by
  33    have h1lt : (1 : ℝ) < Real.sqrt 5 := by simpa [Real.sqrt_one] using hsqrt_gt
  34    linarith
  35  have hdiv : (2 : ℝ) / 2 < (1 + Real.sqrt 5) / 2 := (div_lt_div_of_pos_right h2lt htwo)
  36  have hone_lt : 1 < (1 + Real.sqrt 5) / 2 := by simpa using hdiv
  37  simpa [phi] using hone_lt
  38

papers checked against this theorem

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