phiScale_add

formal source

  69noncomputable def phiScale (n : ℤ) (x : ℝ) : ℝ := x * phi ^ n
  70
  71/-- φ-scaling is a group action. -/
  72theorem phiScale_add (m n : ℤ) (x : ℝ) :
  73    phiScale m (phiScale n x) = phiScale (m + n) x := by
  74  simp only [phiScale, mul_assoc]
  75  congr 1
  76  rw [zpow_add₀ (ne_of_gt phi_pos), mul_comm]
  77
  78theorem phiScale_zero (x : ℝ) : phiScale 0 x = x := by
  79  simp [phiScale]
  80
  81theorem phiScale_neg (n : ℤ) (x : ℝ) :
  82    phiScale (-n) (phiScale n x) = x := by
  83  rw [phiScale_add, neg_add_cancel, phiScale_zero]
  84
  85/-! ## The φ-Ladder Hypothesis Class -/
  86
  87/-- A value is on the φ-ladder if it equals X₀ · φⁿ for some base X₀ and integer n. -/
  88structure OnPhiLadder (x : ℝ) (base : ℝ) where
  89  rung : ℤ
  90  eq : x = base * phi ^ rung
  91
  92/-- The rung of a value relative to a base (computed via logarithm). -/
  93noncomputable def computeRung (x : ℝ) (base : ℝ) : ℝ :=
  94  Real.log (x / base) / Real.log phi
  95
  96/-- A value is "near" a φ-rung if its computed rung is close to an integer. -/
  97def nearPhiRung (x : ℝ) (base : ℝ) (tolerance : ℝ) : Prop :=
  98  ∃ n : ℤ, |computeRung x base - n| ≤ tolerance
  99
 100/-! ## The φ-Ladder Hypothesis (Explicit) -/
 101
 102/-- The φ-ladder hypothesis for a collection of scales.