sqrt5_pos

formal source

  59noncomputable def ψ : ℝ := (1 - Real.sqrt 5) / 2
  60
  61/-- √5 > 0 -/
  62theorem sqrt5_pos : 0 < Real.sqrt 5 := Real.sqrt_pos_of_pos (by norm_num : (5:ℝ) > 0)
  63
  64/-- φ > 0 -/
  65theorem phi_pos : 0 < φ := by
  66  unfold φ
  67  have h := sqrt5_pos
  68  linarith
  69
  70/-- φ > 1 -/
  71theorem phi_gt_one : 1 < φ := by
  72  unfold φ
  73  have h := sqrt5_pos
  74  have h2 : Real.sqrt 5 > 1 := by
  75    rw [show (1:ℝ) = Real.sqrt 1 from (Real.sqrt_one).symm]
  76    exact Real.sqrt_lt_sqrt (by norm_num) (by norm_num)
  77  linarith
  78
  79/-- **THEOREM: φ² = φ + 1** (the defining equation). -/
  80theorem phi_equation : φ ^ 2 = φ + 1 := by
  81  unfold φ
  82  have h5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (5:ℝ) ≥ 0)
  83  ring_nf
  84  nlinarith [h5]
  85
  86/-- **THEOREM: ψ² = ψ + 1** (conjugate satisfies the same equation). -/
  87theorem psi_equation : ψ ^ 2 = ψ + 1 := by
  88  unfold ψ
  89  have h5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt (by norm_num : (5:ℝ) ≥ 0)
  90  ring_nf
  91  nlinarith [h5]
  92