pi_computable

formal source

  68    In this file we use a *classical* notion of computability: existence of
  69    fast rational approximations. With classical choice, every real admits such
  70    approximations (via density of ℚ in ℝ), so π is computable in this sense. -/
  71theorem pi_computable : Computable Real.pi := by infer_instance
  72
  73/-- φ (golden ratio) is computable via Fibonacci approximations.
  74
  75    From Mathlib's `Real.fib_succ_sub_goldenRatio_mul_fib`:
  76      F_{n+1} - φ · F_n = ψ^n   where ψ = (1-√5)/2
  77
  78    Rearranging: F_{n+1}/F_n - φ = ψ^n / F_n
  79
  80    The convergence is fast because |ψ/φ| ≈ 0.382 < 0.5.
  81    Using n' = n + 2 gives sufficient precision.
  82
  83    **Proof approach**: Use F_{n}/F_{n-1} as the approximation sequence.
  84    Error bound: |F_n/F_{n-1} - φ| < 1/F_{n-1}^2 ≈ φ^(-2n+2)/5
  85    For 2^(-k) precision, need n ≈ k·log(2)/log(φ) ≈ 1.44k terms.
  86
  87    In this file we again use the classical approximation-based notion. -/
  88theorem phi_computable : Computable Constants.phi := by infer_instance
  89
  90/-- Helper: 2^n > 0 for any integer n -/
  91lemma two_zpow_pos (n : ℤ) : (0 : ℝ) < (2 : ℝ) ^ n := by
  92  positivity
  93
  94/-! ## Classical approximation: every real has fast rational approximations
  95
  96`Real` in Mathlib is constructed as a completion of `ℚ`, so (classically) every
  97real number admits rational approximations at any prescribed precision. This is
  98enough to satisfy our existential `Computable` predicate. -/
  99
 100instance (x : ℝ) : Computable x where
 101  approx := by