pi_computable
The real number π satisfies the computability condition that there exists an algorithm producing rational approximations q_n with |π - q_n| < 2^{-n} for every natural number n. Researchers verifying that Recognition Science constants remain algorithmically accessible despite classical proof steps would cite this result when chaining to expressions for the fine-structure constant. The proof is a one-line wrapper applying the infer_instance tactic to discharge the goal from the pre-existing instance of the Computable class.
claim$π$ is computable: there exists a function $f: ℕ → ℚ$ such that $|π - f(n)| < 2^{-n}$ for all natural numbers $n$.
background
The module Meta.ConstructiveNote resolves the objection that Recognition Science claims algorithmic foundations while employing classical logic in Lean. It separates proof machinery from output computability, noting that classical axioms do not prevent specific reals from admitting fast rational approximations. The local setting is Gap 2, where the derived constants of the framework (including those involving π) must remain computable reals regardless of the logic used to derive them.
proof idea
The proof is a one-line wrapper that applies the infer_instance tactic. This discharges the goal because the Computable class (defined in the same module as existence of an approximation function f with the 2^{-n} error bound) already carries an instance for Real.pi, drawn from standard algorithms such as the Bailey-Borwein-Plouffe series or Machin formula.
why it matters in Recognition Science
This declaration feeds the parent theorems alpha_seed_computable and curvature_computable, which establish that the geometric seed 4π·11 and the curvature term 103/(102 π^5) are computable, thereby confirming that the full expression for α^{-1} lies inside the Recognition Science band (137.030, 137.039). It directly addresses the classical-constructive gap in the framework while leaving open the question of extracting certified programs under fully constructive axioms.
scope and limits
- Does not exhibit or certify any particular algorithm for computing π.
- Does not claim that every real number is computable under constructive logic alone.
- Does not address convergence rates or computational complexity of the approximations.
- Does not discharge the noncomputable keyword on Real.pi itself.
Lean usage
have h_pi : Computable Real.pi := pi_computableformal statement (Lean)
71theorem pi_computable : Computable Real.pi := by infer_instance
proof body
Term-mode proof.
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. -/