`phi_fixed_point'`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.PhiSupport on GitHub at line 27.

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

formal source

  24    Proof: From φ² = φ + 1, divide by φ (which is positive) to get φ = 1 + 1/φ
  25    NOTE: Also defined in PhiSupport/Lemmas.lean for use by that module.
  26    Renamed here to avoid conflict. -/
  27theorem phi_fixed_point' : phi = 1 + phi⁻¹ := by
  28  have hphi_pos : phi > 0 := phi_pos
  29  have hphi_ne : phi ≠ 0 := ne_of_gt hphi_pos
  30  -- From phi_squared: φ² = φ + 1
  31  -- Divide both sides by φ: φ = 1 + 1/φ
  32  have h := phi_squared
  33  field_simp at h ⊢
  34  linarith
  35
  36/-- φ > 1: The golden ratio is strictly greater than 1.
  37
  38    This is already proven in Constants.lean -/
  39theorem one_lt_phi : (1 : ℝ) < phi := Constants.one_lt_phi
  40
  41end PhiSupport
  42end IndisputableMonolith

papers checked against this theorem

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