IndisputableMonolith.PhiSupport.Lemmas

   1import Mathlib
   2import Mathlib.NumberTheory.Real.GoldenRatio
   3import IndisputableMonolith.Constants
   4
   5/-!
   6Module: IndisputableMonolith.PhiSupport.Lemmas
   7
   8Golden-ratio support lemmas used by certificates:
   9- `φ^2 = φ + 1` (from Mathlib's `Real.goldenRatio_sq`)
  10- fixed-point identity `φ = 1 + 1/φ`
  11- uniqueness of the positive root of `x^2 = x + 1`
  12
  13These depend only on elementary real algebra and Mathlib's goldenRatio facts.
  14-/
  15
  16namespace IndisputableMonolith
  17namespace PhiSupport
  18
  19open Real
  20
  21/-- Closed form for φ. -/
  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
  56    have hx2 : x ^ 2 = x + 1 := hx.left
  57    -- (2x−1)^2 = 5
  58    have hquad : (2 * x - 1) ^ 2 = 5 := by
  59      calc
  60        (2 * x - 1) ^ 2 = 4 * x ^ 2 - 4 * x + 1 := by ring
  61        _ = 4 * (x + 1) - 4 * x + 1 := by simpa [hx2]
  62        _ = 5 := by ring
  63    -- From x>0 and x(x−1)=1, get x>1 hence 2x−1>0
  64    have hx_nonzero : x ≠ 0 := ne_of_gt hx.right
  65    have hx_sub : x ^ 2 - x = 1 := by
  66      have := congrArg (fun t => t - x) hx.left
  67      simpa [sub_eq_add_neg] using this
  68    have hx_mul : x * (x - 1) = 1 := by
  69      have hfac : x ^ 2 - x = x * (x - 1) := by ring
  70      simpa [hfac] using hx_sub
  71    have hx1_pos : 0 < x - 1 := by
  72      -- divide by positive x
  73      have := congrArg (fun t : ℝ => t / x) hx_mul
  74      have hdiv : x - 1 = 1 / x := by
  75        simpa [div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc, hx_nonzero] using this
  76      simpa [hdiv] using (one_div_pos.mpr hx.right)
  77    have hx_pos : 0 < 2 * x - 1 := by linarith
  78    -- Take square root
  79    have hsqroot : Real.sqrt ((2 * x - 1) ^ 2) = Real.sqrt 5 := by
  80      simpa [hquad]
  81    have hsqabs : Real.sqrt ((2 * x - 1) ^ 2) = |2 * x - 1| := by
  82      exact Real.sqrt_sq_eq_abs (2 * x - 1)
  83    have habs : |2 * x - 1| = Real.sqrt 5 := by
  84      -- rewrite the left side of hsqroot via sqrt(sq)=|·|
  85      simpa [hsqabs] using hsqroot
  86    have hlin : 2 * x - 1 = Real.sqrt 5 := by
  87      have hnonneg : 0 ≤ 2 * x - 1 := le_of_lt hx_pos
  88      have hdrop : |2 * x - 1| = 2 * x - 1 := abs_of_nonneg hnonneg
  89      simpa [hdrop] using habs
  90    have h2x : 2 * x = 1 + Real.sqrt 5 := by linarith
  91    have hx_eq : x = (1 + Real.sqrt 5) / 2 := by
  92      have h2 : (2 : ℝ) ≠ 0 := by norm_num
  93      -- x = (1+√5)/2  ↔  2*x = 1+√5
  94      exact (eq_div_iff_mul_eq h2).2 (by simpa [mul_comm] using h2x)
  95    simpa [Constants.phi] using hx_eq
  96  · intro hx; subst hx
  97    exact And.intro phi_squared (lt_trans (by norm_num) one_lt_phi)
  98
  99/-- **Phase 3 Derivation**: Model-independent exclusivity of φ.
 100    The golden ratio is the unique positive solution to the self-similarity constraint. -/
 101theorem exclusivity_model_independent :
 102    ∀ x : ℝ, x > 0 → (x^2 = x + 1) → x = Constants.phi := by
 103  intro x hx h_eq
 104  have h_root := phi_unique_pos_root x
 105  exact h_root.mp ⟨h_eq, hx⟩
 106
 107end PhiSupport
 108end IndisputableMonolith
 109