`one_lt_phi`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.PhiSupport.Lemmas on GitHub at line 25.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  22lemma phi_def : Constants.phi = Real.goldenRatio := rfl
  23
  24/-- φ > 1. -/
  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

papers checked against this theorem

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