phi_pos

formal source

  36noncomputable def phi : ℝ := (1 + Real.sqrt 5) / 2
  37
  38/-- φ is positive. -/
  39theorem phi_pos : 0 < phi := by
  40  unfold phi
  41  have h : 0 < Real.sqrt 5 := Real.sqrt_pos.mpr (by norm_num : (0:ℝ) < 5)
  42  linarith
  43
  44/-- φ > 1. (√5 > 1, so (1 + √5)/2 > 1) -/
  45theorem phi_gt_one : 1 < phi := by
  46  unfold phi
  47  -- We need: 1 < (1 + √5) / 2  ⟺  2 < 1 + √5  ⟺  1 < √5
  48  have h5pos : (0 : ℝ) < 5 := by norm_num
  49  have hsqrt5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (le_of_lt h5pos)
  50  have h1sq : (1 : ℝ) ^ 2 = 1 := by norm_num
  51  -- √5 > 1 because 5 > 1 and sqrt is monotone
  52  have h1 : (1 : ℝ) < Real.sqrt 5 := by
  53    have : Real.sqrt 1 = 1 := Real.sqrt_one
  54    rw [← this]
  55    exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num : (1:ℝ) < 5)
  56  linarith
  57
  58/-- φ² = φ + 1 (the defining property). -/
  59theorem phi_sq : phi ^ 2 = phi + 1 := by
  60  unfold phi
  61  have h5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (0:ℝ) ≤ 5)
  62  ring_nf
  63  rw [h5]
  64  ring
  65
  66/-! ## The φ-Scaling Action -/
  67
  68/-- Scale a value by φⁿ. -/
  69noncomputable def phiScale (n : ℤ) (x : ℝ) : ℝ := x * phi ^ n