`phi_ne_zero`

proved

show as: view math explainer →

module: IndisputableMonolith.PhiSupport.Lemmas
domain: PhiSupport
line: 28 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.PhiSupport.Lemmas on GitHub at line 28.

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

  25lemma one_lt_phi : 1 < Constants.phi := by simp [phi_def, Real.one_lt_goldenRatio]
  26
  27/-- φ ≠ 0. -/
  28lemma phi_ne_zero : Constants.phi ≠ 0 := by
  29  -- goldenRatio = (1+√5)/2 ≠ 0
  30  have : Real.goldenRatio ≠ 0 := by
  31    have hpos : 0 < Real.goldenRatio := Real.goldenRatio_pos
  32    exact ne_of_gt hpos
  33  simpa [phi_def] using this
  34
  35/-- φ^2 = φ + 1 using the closed form. -/
  36@[simp] theorem phi_squared : Constants.phi ^ 2 = Constants.phi + 1 := by
  37  simp [phi_def, Real.goldenRatio_sq]
  38
  39/-- φ = 1 + 1/φ as an algebraic corollary. -/
  40theorem phi_fixed_point : Constants.phi = 1 + 1 / Constants.phi := by
  41  have h_sq : Constants.phi ^ 2 = Constants.phi + 1 := phi_squared
  42  have h_ne_zero : Constants.phi ≠ 0 := phi_ne_zero
  43  calc
  44    Constants.phi = (Constants.phi ^ 2) / Constants.phi := by
  45      rw [pow_two, mul_div_cancel_left₀ _ h_ne_zero]
  46    _ = (Constants.phi + 1) / Constants.phi := by rw [h_sq]
  47    _ = Constants.phi / Constants.phi + 1 / Constants.phi := by rw [add_div]
  48    _ = 1 + 1 / Constants.phi := by
  49      have : Constants.phi / Constants.phi = 1 := div_self h_ne_zero
  50      rw [this]
  51
  52/-- Uniqueness: if x > 0 and x² = x + 1, then x = φ. -/
  53 theorem phi_unique_pos_root (x : ℝ) : (x ^ 2 = x + 1 ∧ 0 < x) ↔ x = Constants.phi := by
  54  constructor
  55  · intro hx
  56    have hx2 : x ^ 2 = x + 1 := hx.left
  57    -- (2x−1)^2 = 5
  58    have hquad : (2 * x - 1) ^ 2 = 5 := by

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.