pi_computable
plain-language theorem explainer
The theorem shows that π meets the Computable predicate: an algorithm exists producing rationals q_n with |π - q_n| < 2^{-n}. Recognition Science authors cite it when separating proof machinery from output computability of derived constants. The proof is a one-line wrapper invoking the typeclass instance.
Claim. The real number π is computable: there exists a function f : ℕ → ℚ such that ∀ n ∈ ℕ, |π - f(n)| < 2^{-n}.
background
The Computable class states that a real x admits an algorithm returning rationals within 2^{-n} error. This module resolves the classical-versus-constructive gap by noting that classical proof steps do not alter whether outputs like π remain computable reals. The local setting distinguishes proof logic from the algorithmic character of RS constants such as φ and α^{-1}.
proof idea
One-line wrapper that applies infer_instance on the Computable Real.pi typeclass. The surrounding comment lists known algorithms (BBP formula, Machin formula) that witness the required rational approximations, but the Lean term relies on the pre-existing instance.
why it matters
It supplies the base fact used by alpha_seed_computable (4π·11) and curvature_computable (103/(102π^5)). These feed the claim that all RS-derived constants remain computable reals even when proofs employ classical logic. The result closes one objection listed in the module doc-comment without introducing new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.