phiScale_zero

formal source

  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.
 103
 104This is the explicit claim that "privileged scales land on integer rungs."
 105It generates prediction obligations.
 106-/
 107class PhiLadderHypothesis (α : Type*) where
 108  /-- The base scale of the ladder. -/