pith. machine review for the scientific record. sign in
theorem

phi_equation

proved
show as:
view math explainer →
module
IndisputableMonolith.Foundation.PhiForcing
domain
Foundation
line
43 · github
papers citing
31 papers (below)

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Foundation.PhiForcing on GitHub at line 43.

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

  40noncomputable def φ : ℝ := (1 + Real.sqrt 5) / 2
  41
  42/-- φ satisfies the golden ratio equation: φ² = φ + 1. -/
  43theorem phi_equation : φ^2 = φ + 1 := by
  44  simp only [φ, sq]
  45  have h5 : (0 : ℝ) ≤ 5 := by norm_num
  46  have hsq5 : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt h5
  47  field_simp
  48  nlinarith [Real.sq_sqrt h5, sq_nonneg (Real.sqrt 5)]
  49
  50/-- φ is positive. -/
  51theorem phi_pos : 0 < φ := by
  52  simp only [φ]
  53  have h5 : Real.sqrt 5 > 2 := by
  54    have h4 : (4 : ℝ) < 5 := by norm_num
  55    have hsqrt4 : Real.sqrt 4 = 2 := by
  56      rw [show (4 : ℝ) = 2^2 by norm_num, Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2)]
  57    calc Real.sqrt 5 > Real.sqrt 4 := Real.sqrt_lt_sqrt (by norm_num) h4
  58      _ = 2 := hsqrt4
  59  linarith
  60
  61/-- φ > 1. -/
  62theorem phi_gt_one : φ > 1 := by
  63  simp only [φ]
  64  have h5 : Real.sqrt 5 > 2 := by
  65    have h4 : (4 : ℝ) < 5 := by norm_num
  66    have hsqrt4 : Real.sqrt 4 = 2 := by
  67      rw [show (4 : ℝ) = 2^2 by norm_num, Real.sqrt_sq (by norm_num : (0 : ℝ) ≤ 2)]
  68    calc Real.sqrt 5 > Real.sqrt 4 := Real.sqrt_lt_sqrt (by norm_num) h4
  69      _ = 2 := hsqrt4
  70  linarith
  71
  72/-- φ < 2. -/
  73theorem phi_lt_two : φ < 2 := by