IndisputableMonolith.PhiSupport

   1import Mathlib
   2import IndisputableMonolith.Constants
   3
   4namespace IndisputableMonolith
   5namespace PhiSupport
   6
   7open Constants
   8
   9/-- φ² = φ + 1: The defining equation of the golden ratio.
  10
  11    Proof: φ = (1+√5)/2, so φ² = (1+√5)²/4 = (1 + 2√5 + 5)/4 = (6 + 2√5)/4 = (3 + √5)/2
  12    And φ + 1 = (1+√5)/2 + 1 = (3 + √5)/2 ✓ -/
  13theorem phi_squared : phi ^ 2 = phi + 1 := by
  14  unfold phi
  15  have h5 : (0 : ℝ) ≤ 5 := by norm_num
  16  have hsqrt : Real.sqrt 5 ^ 2 = 5 := Real.sq_sqrt h5
  17  field_simp
  18  ring_nf
  19  rw [hsqrt]
  20  ring
  21
  22/-- φ = 1 + 1/φ: The fixed-point equation.
  23
  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
  43